The Sky was the Limit

Everyone remembers Tom Petty's song 'Into the Great Wide Open' with it's famous refrain

The sky was the limit

I was thinking about limits (the category theory ones) for many years now, but could never really visualize the concept. (I should really start reading Awodey's 'Category Theory' which will be my present to self at Xmas.) I tried to get hold of the related problems with a mental construction of a lazy, self-building thrist. It was clear that each element should increase the type, Z, (S Z), (S (S Z)), etc. ad infinitum, so the start type would be clear: Thrist Up Z ?. But the ?, let's call it the limit, is not clear at all. Anyway it would be an infinite type, not like in the simple analogy of let count = 0 : count in count, where count :: [Int] holds. As we know type checkers do not like infinite types, as it would take forever and two days to check them :-)

Fortunately the sky is not a limit anymore and I came up with a solution that is nice and short even in Ωmega, which is a strict language (albeit with a lazy construct). Since it is only a few lines I can effortlessly reproduce it here.

data Count :: Nat ~> Nat ~> * where

  Incr :: Nat' n -> Count n (1+n)t

The Incr constructor states the typing rule, namely one higher to the right than to the left. We can try it out:

prompt> [Incr 0v, Incr 1v, Incr 2v]l

[(Incr 0v),(Incr 1v),(Incr 2v)]l : Thrist Count 0t 3t

Not surprisingly, this is the only value of type Thrist Count 0t 3t. We follow the example of count above and write:

a = [Incr 0v; lazy (shift a)]l

Naturally shift will shift a Count thrist to the right, thus satisfying the type constraint of thrists, that at each joining point the left and right types must match up. The lazy keyword is needed here to delay the evaluation, it is however pointless in Haskell.

All that remains is to write the shift function which will create the ominous limit type:

shift :: Thrist Count n a -> Thrist Count (1+n)t a

shift [Incr n; r]l = [Incr (1+n)v; lazy (shift r)]l

It is probably not a surprise that the limit value is ⊥ (i.e. nonexistent), so any type will do (along the constraints of the kind in question). I settled with a universal type.

Now we can pattern match on a to see that it really grows into the sky:

case a of {[a,aa,aaa,aaaa; b]l -> show b}

prints "[(Incr 4v) ; ...]l" thanks to show's magic. The ... corresponds to the suspended computation.

Hey, it wasn't that hard at all! Where is the infinite type? It is hidden behind the existential barrier that is formed at each thrist joining point, and since it cannot escape we do not have to worry it...

Good night!