Search code examples
haskellhigher-kinded-typesunificationhigher-order-types

Why can I pass partially applied type constructors only in type parameter position?

This is probably a silly question but I cannot figure out the underlying rules for the following behavior:

foo :: t (f a) -> f a b -- accepted
foo = undefined

bar :: t [f a] -> f a b -- rejected
bar = undefined

It makes perfect sense that f applied to a and a b respectively in bar leads to a kind error and is thus rejected. But why is foo accepted?

Solution

  • It's the kind of f.

    Since the return type is f a b - i.e. f applied to two parameters, - it means that f :: Type -> Type -> Type.

    But then f a is used as a list element - [f a] - and list elements must be Type, which means that f a :: Type, which means that f :: Type -> Type.

    Mismatch.

    foo works because types can be partially applied. That is, if f :: Type -> Type -> Type, then f a :: Type -> Type. And then, type t is allowed to have a parameter of kind Type -> Type, so everything matches.

    To reiterate the above:

    • foo works because type t may have a parameter of kind Type -> Type.
    • bar doesn't work, because type [] (aka "list") must have a parameter of kind Type.