Enforce lists to be monotonic at compile time
I’ve been learning lately about typelevel programming in haskell and now that I feel that some ideas have clicked it’s time to write down some potential applications. You’re probably not going to need this in particular, but I wanted to show up to what extent the typesystem can enforce properties of your program that you wouldn’t even dream of in other languages.
In this post I’ll show you briefly how we can enforce monotonic behaviour in fixed constant lists defined at compile time. As I said, I’ll use some common typelevel programming tricks for achieving this goal.
Typelevel nats
These are the usual Peano naturals:
data Nat = Z  Succ Nat
zero :: Nat
zero = Z
one :: Nat
one = Succ Z
two :: Nat
two = Succ One
Using the DataKinds
language extension we can promote those
values to types, and the Nat
type to a kind. That would allow
us to have types like these:
type Zero = Z
type One = Succ Z
type Two = Succ One
Typelevel functions
The same way we can define the usual sum and order for values of
type Nat
:
sum :: Nat > Nat > Nat
sum Z a = a
sum (Succ a) b = Succ (sum a b)
lessThanOrEqualTo :: Nat > Nat > Bool
lessThanOrEqualTo Z a = True
lessThanOrEqualTo a Z = False
lessThanOrEqualTo (Succ n) (Succ m) = lessThanOrEqualTo n m
we can make functions that operate on the type level using
the TypeFamilies
language extension:
type family Sum (a :: Nat) (b :: Nat) :: Nat where
Sum Z a = a
Sum (Succ a) b = Succ (Sum a b)
type familiy LessThanOrEqualTo (a :: Nat) (b :: Nat) :: Bool where
LessThanOrEqualTo Z b = True
LessThanOrEqualTo a Z = False
LessThanOrEqualTo (Succ n) (Succ m) = LessThanOrEqualTo n m
Note that in this example Bool
is the kind Bool
(thanks to
DataKinds
) and True
and False
are both types of kind Bool
.
With those type families we could have things like:
data Proxy a = Proxy  Data.Proxy
proof :: Proxy True
proof = (Proxy :: Proxy (LessThan One Two))  compiles
fakeProof :: Proxy True
fakeProof = (Proxy :: Proxy (LessThan Two One))  compile time error
What’s more, using the TypeOperators
language extension we can
change the above type families to:
type family (a :: Nat) + (b :: Nat) :: Nat where
Z + a = a
Succ a + b = Succ (a + b)
type familiy (a :: Nat) <= (b :: Nat) :: Bool where
Z <= b = True
a <= Z = False
(Succ n) <= (Succ m) = n <= m
proof :: Proxy True
proof = (Proxy :: Proxy (One <= True))
Turn typelevel naturals into values
We want a function that turns any type of kind Nat
into an
integer. You can’t have a function from a type to a value in haskell
but we can model that with the Proxy
typeconstructor.
class ToInt (a :: Nat) where
toInt :: Proxy a > Int
instance ToInt Z where
toInt _ = 0
instance ToInt a => ToInt (Succ a) where
toInt (_ :: Proxy (Succ a)) = 1 + toInt (Proxy :: Proxy a)
In order to make this piece of code work we’ll need
FlexibleInstances
, UndecidableInstances
and ScopedTypeVariables
.
FlexibleInstances
is a harmless extension (meaning nothing’s gonna
hurt you), ScopedTypeVariables
makes GHC understand that the
a
type variable we use in the Proxy (Succ a)
is the same
variable we are refering to later with Proxy a
. UndecidableInstances
could make type checking your code undecidable, but we are safe for now.
Increasing
typefamily
Taking advantage of the fact that the list type constructor is promoted
by DataKinds
to a kind constructor we can define the following
type family:
type family Increasing (nats :: [Nat]) where
Increasing '[] = True
Increasing '[a] = True
Increasing (a:(b:others)) = (a <= b) && Increasing (b:others)
Increasing _ = False
That given a typelevel list of typelevel nats evaluates to the
type True
if the nats
are monotonically increasing.
Get list of increasing integers
In the same vein we obtained an integer for every typelevel nat,
we now want to get a list of integers for every typelevel list
of types of kind Nat
, but, we’ll only do so for monotonically
increasing lists.
class (Increasing nats ~ True) => ToIncreasing (nats :: [Nat]) where
toIncreasing :: Proxy nats > [Int]
instance ToIncreasing '[] where
toIncreasing _ = []
instances (ToInt a, ToIncreasing others, Increasing (a:others) ~ True) => ToIncreasing (a:others) where
toIncreasing (_ :: Proxy (a:others)) =
toInt (Proxy :: Proxy a) : toIncreasing (Proxy :: Proxy others)
toIncreasing (Proxy :: Proxy '[Zero, One, Two])  [0,1,2]
toIncreasing (Proxy :: Proxy '[Two, Zero, One])  compiletime error
Observations

Interestingly enough we need more constraints in the last instance definition that would be provably needed. We know that every
a
is aNat
and that everyNat
is aToInt
but we have to have that as a constraint anyway. Moreover, ifIncreasing (a:others) ~ True
then necessarilyToIncreasing others
is satisfied, but once again we need it as a constraint. 
This approach can be easily extended to other invariants that can be defined inductively on lists. How much more extendable is this technique?

Nobody wants to define lists of numbers like
[ThreehundredThirtyTwo, Fifteen]
and that’s ok. Typeliterals would allow us to provide an ergonomic API. 
Some potentially useful typelevel combinators arise from this code. There probably are libraries of typelevel combinators out there. Have to take a look.

This post talks about some of the things I talk in here too and was quite didactic.