Parametric polymorphism

a : type ⊢ f : type \over ∀a. f : type

Consider that you have a function that’s fairly simple, for example the identity function λx. x. Since this function does not use specific eliminators or constructors for the x -variable, that variable can be of any type and this function would work like it’s supposed to.

So you just assume there’s some type that’s filled in.

a : type \over λx. x : a → a

In this book we denote this use with the ∀ -symbol. Eg. we write:

id : ∀a. a → a
id = λx. x

const : ∀a b. a → b → a
const = λx.λy. x

Note that these parameters do not have visible constructors or eliminators. This is something I’m still wondering about. Should I do something about that?

Haskell notation

Haskell treats types and terms as separate entities. This allows it to identify any lower-case term that appears in a type as a type parameter.

id :: a -> a
id x = x

If you want to, you can add “forall” -clause to identify type parameters.

const :: forall a b. a -> b -> a
const x _ = x