Monty Thibault
Monty Thibault

Reputation: 51

Haskell Polymorphism With Kinds and Type Variables

In Haskell I have learnt that there are type variables (ex. id :: a -> a), applied to type signatures, and kinds (ex. Maybe :: * -> *), applied to type constructors and type classes. A type must have kind * (be a concrete type) in order to hold values.

We use type variables to enable polymorphism: Nothing :: Maybe a means that the constant Nothing can belong to a family of possible types. This leads me to believe that kinding and type variables serve the same purpose; wouldn't the last code sample work as simply Nothing :: Maybe, where type class Maybe remains with the kind * -> * to signify that the type belongs to generic family?

What it seems we are doing is taking an empty parameter (* -> *) and filling it in with a type variable (a) that represents the same level of variance.

We see this behavior in another example:

>>> :k Either
Either :: * -> * -> *
>>> :t Left ()
Left () :: Either () b
>>> :t Right ()
Right () :: Either a ()

Why is it theoretically necessary to make the distinction between kinds and type variables?

Upvotes: 4

Views: 207

Answers (1)

Alexey Romanov
Alexey Romanov

Reputation: 170713

They are distinct just like typing and usual (value-level) variables are distinct. Variables have types, but they aren't types. So also, type variables have kinds. Type variables are the primary notion: without them you don't have parametric polymorphism, and they exist also in many other languages like Java, C#, etc. But Haskell goes further in allowing types-which-take-parameters ([], Maybe, ->, etc.) to exist on their own and to have type variables which represent such non-concrete types. And this means it needs a kind system to disallow things like Maybe Int Int.

From the example, it seems that you suggest that you can write a signature without type variables and restore it to the signature with them. But then how could you distinguish a -> b -> a and a -> b -> b?

Upvotes: 5

Related Questions