kinds.txt

So we have all these types like Int, Float, String, Map String Int, [Maybe String], etc. What do all these types have in common? Well, essentially, they're "normal" types where we can make a value for them. Just as values have types, types have "kinds". In this case, just as `4 : Int`, `Int : *`, and just as `"Hello" : String`, `String : *`. That is to say, all these normal types (the types of plain old values) have kind `*`.

Now, in OCaml, you have type parametricity, but only over types of kind `*`. Let's give an example of a type that's *not* of kind `*`.

`Map : * -> * -> *`

We apply this "type constructor" (which is a kind of "type function", just like constructors are a kind of function) to the type `Int : *`.

`Map Int : * -> *`

Apply this to `String : *`.

`Map Int String : *`

And, as we know, we can create values of type `Map Int String`, so it makes sense that it has kind `*`!

Now, in Haskell, you can actually have things that are parametric not just on types of kind `*`, but types of different kinds. So I can have

`data WrapperWrapper wrapperType innerType = WW (wrapperType innerType)`

Notice that `wrapperType` must have kind `* -> *`. For example,

`WW (Just "hello") : WrapperWrapper Maybe [Char]`

And `Maybe : * -> *`.

In OCaml, you can't do that sort of thing. You can only have things be parametrized by types of kind `*`. Turns out this isn't enough for a lot of useful things like Monads!

Haskell also supports other kinds besides `*` and `* -> ...`. For example, Haskell has a kind `#`, which is just like `*` except that the types with kind `#` aren't behind a pointer.

As with many high-level languages (Python, JavaScript, etc.) most values are somewhat complex in structure, so they live behind a pointer. Unfortunately, this isn't great for performance. Languages like OCaml, which only have one kind, have no way of knowing statically if an object is behind a pointer or if it's a raw, unboxed object (like an `Integer` vs an `int` in Java). Therefore, it has to make this determination at runtime, so every value has a bit set to one or zero to say "I'm a pointer" or "I'm not a pointer". This is pretty bad, because it means an extra check every time you use an object, and `int`s are only 31 or 63 bits in OCaml.

Haskell, on the other hand, knows statically, because unboxed types have kind `#`, so the compiler knows how to statically treat them differently. So you can get really good performance by making the distinction between boxed and unboxed values. Note that normally, you would never need to deal with unboxed values yourself. The compiler usually figures out automatically where it can unbox values for you to minimize heap usage.

Haskell also supports (through the use of some extensions) converting arbitrary types to kinds. So if I had

`data Foo = FooA | FooB | FooC`

I could actually "promote" `Foo` to its own kind, and now `FooA`, `FooB`, and `FooC` are types. Note that you can't construct a value of type `FooA`, because `FooA : Foo`, but it would have to be `FooA : *` or `FooA : #` for us to be able to construct a value of that type.

However, if I have something like this:

`data Wrapper dummyType innerType = Wrapper innerType`

I can create a value

`Wrapper 5 : Wrapper FooA Int`

This is really useful for statically keeping track of things that have the same structure, but you don't want to accidentally confuse them. You can just add a "tag" type that indicates what the value is used for.

You can even promote `Int` to a kind, and now all the numbers are types. Haskell has some libraries like Dimensional that do this sort of thing, so you can actually have types for physical dimensions. It could look something like

`data Dimension (length : Int) (time : Int) = Dimension Double`

`foot : Dimension 1 0`

`second : Dimension 0 1`

`(/) : Dimension a b -> Dimension c d -> Dimension (a-c) (b-d)`

`foot / second : Dimension 1 -1`

This is super great for physical simulation stuff, because it lets you know you got your units right.