Day 11: Key — Typesafe Dynamic Typing

I saw mention of this at Haskell eXchange 2016. I haven’t done anything with it, but it intrigued me so I decided to include a post in this series.

Advertised as type-safe dynamic typing without needing Typeable class constraints, Key sits somewhere between the unique supply and the ST state monads.

Unique supply

The point of a unique supply monad is to give a supply of unique names/identifiers that are different to the all of the identifiers previously supplied — for example, if you’re outputting a structured document that needs identifiers for each section.

ST state

This monad lets you create STRefs which are typed mutable variables that you can read or write from within that stateful computaton, but that do not leak out of that computation. By storing state in STRefs rather than a single global environment, there is no need to declare the entire environment in one place.

newSTRef :: a -> ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s ()

Key

As I said before, Key sits between the two: it gives you keys which are distinct from other keys, and each key has a type associated with it (as with STRefs) but nothing more: no mutable storage.

So what does is type associated with each key for, if it isn’t being used to type a storage location? You get a new equality test testEquality, instead of ==, that gives more information at compile time than the simple True / False values returned by ==.

newKey :: KeyM s (Key s a)
testEquality :: Key s a -> Key s b -> Maybe (a :~: b)
data a :~: b where
  Refl :: a :~: a

newKey gets a new key, with a type attacked to it. testEquality compares two keys for equality returning either Nothing or Just Refl.

What that type :~: represents is a compile time proof that its two type parameters are identical: testEquality will return a “proof” that the types of two keys are equal, if the two keys are actually the same key; or Nothing if they are not the same key.

That information can be used at compile time (even though the comparison doesn’t happen until run time) with a case statement:

case testEquality k1 k2 of
  Just Refl -> xxxx

In the case of Just Refl, in xxxx, we know that k1 and k2 are the same keys, but also the compiler now knows, at compile time, that k1 and k2 have the same types.

If you (for example) used Typeable to get the types of k1 and k2, and compared those, you as programmer might convince yourself that in some code path the types are equal, but you aren’t in a position to convince the compiler — what you would get out of the comparison operation is True without any futher type information made available to the compiler.

What can you build?

The Key paper starts by defining boxes, which store a single value and need a key to unlock them. Boxes aren’t parameterised by their type — instead the type comes from the key that is used to successfully unlock the box.

From that, you can build up STRefs — because boxes all have the same type, you can stick them in a list, and try unlocking all of them with a key.

Typed names also have use when writing arrow based code, where although you can name “things” and attach a type, you can’t (in pure Haskell) inspect those “things” — that is the big difference between arrows and monads.

What this isn’t

Key doesn’t give you the ability to identify types separately from keys. It doesn’t let you take two arbitrary values and compare their types, nor get the type of a value as a value itself. You only get two compare two keys for key equality, resulting in a type equality proof if they are the same key. So it doesn’t replace Typeable, but it turns out you don’t always need to generally represent types as values.

See Also

The Key monad paper