Putting together a talk on parametric polymorphism. While I it doesn't capture all nuances is type-level lambdas a good springboard?
Conversation
I suspect that's going to be a very bad idea. Foralls and type-level lambdas are different things and the difference can be _extremely_
2
4
confusing to someone who isn't already familiar with these things (so, as far as I can tell approximately everyone at some point or another)
3
Had to reteach this to myself more than once - indeed, it can be confusing:
fn foo<T>(x: T) -> T { x } ≡ foo : ∀(α:★). α→α = Λα:★. λx:α. x
1
1
Also confusing: in dependent types t1→t2 becomes a special case of ∀(α:t1).t2, when t2 does not depend on α.
So I'm guessing you were thinking of explaining it somewhere along the lines of this?
type Id<T> = T ≡ Id : Type → Type = Λα:Type.α