Skip to content

Instantly share code, notes, and snippets.

@5310
Forked from anonymous/kinds.txt
Created August 3, 2016 05:01
Show Gist options
  • Save 5310/cbf5a3693bfe94ca3fbc762da2dbafd6 to your computer and use it in GitHub Desktop.
Save 5310/cbf5a3693bfe94ca3fbc762da2dbafd6 to your computer and use it in GitHub Desktop.
Kind Polymorphism in Haskell #article

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 ints 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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment