Reputation: 51
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
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