Please forgive me if this question is dumb.

While reading about Haskell kinds, I notice a theme:

*
* -> *
* -> * -> *

I get the impression that kinds in Haskell ultimately boil down to how many asterisks there are. You might say that the kind of a type is really just the number of types you need to apply to it before it becomes *. In other words, you could count all *'s but the last one, and define a type's kind by an integer. Say 0, 1, 2, etc.

Here's my question:

Is this a correct observation about Haskell's type system? Or does it allow something other than *'s to go where you typically see *'s? For example:

* -> a -> *

I imagine someone might want to do this to constrain type variables to have an instance of a type class, for example.

Functor a, Applicative b => * -> a -> b -> *

Is that a thing?

CodePudding user response：

The most basic form of the kind language contains only * (or Type in more modern Haskell; I suspect we'll eventually move away from *) and ->.

But there are more things you can build with that language than you can express by just "counting the number of *s". It's not just the number of * or -> that matter, but how they are nested. For example * -> * -> * is the kind of things that take two type arguments to produce a type, but (* -> *) -> * is the kind of things that take a single argumemt to produce a type where that argument itself must be a thing that takes a type argument to produce a type. data ThreeStars a b = Cons a b makes a type constructor with kind * -> * -> *, while data AlsoThreeStars f = AlsoCons (f Integer) makes a type constructor with kind (* -> *) -> *.

There are several language extensions that add more features to the kind language.

PolyKinds adds kind variables that work exactly the same way type variables work. Now we can have kinds like forall k. (* -> k) -> k.

ConstraintKinds makes constraints (the stuff to the left of the => in type signatures, like Eq a) become ordinary type-level entities in a new kind: Constraint. Rather than the stuff left of the => being special purpose syntax fairly disconnected from the rest of the language, now what is acceptable there is anything with kind Constraint. Classes like Eq become type constructors with kind * -> Constraint; you apply it to a type like Eq Bool to produce a Constraint. The advantage is now we can use all of the language features for manipulating type-level entities to manipulate constraints (including PolyKinds!).

DataKinds adds the ability to create new user-defined kinds containing new type-level things, in exactly the same way that in vanilla Haskell we can create new user-defined types containing new term-level things. (Exactly the same way; the way DataKinds actually works is that it lets you use a data declaration as normal and then you can use the resulting type constructor at either the type or the kind level)

There are probably some others I'm forgetting. But certainly the kind language is richer than the OP is imagining just with the basic Haskell features, and there is much more to it once you turn on a few (quite widely used) extensions.