Using Type Nats to create a type level list (having problems adding numbers on the type level)

Question

Just for fun, I wanted to create a Type level list that knows how long it is. Something like this:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

data family TypeList a (n::Nat)

data instance TypeList a (0) = EmptyList
data instance TypeList a (1) = TL1 a (TypeList a (0))
data instance TypeList a (2) = TL2 a (TypeList a (1))
data instance TypeList a (3) = TL3 a (TypeList a (2))

But, of course I'd like to generalize this to something like:

data instance TypeList a (n)   = TL3 a (TypeList a (n-1))

But this generates an error:

    TypeList.hs:15:53: parse error on input `-'
    Failed, modules loaded: none.

Another attempt:

data instance TypeList a (n+1) = TL3 a (TypeList a (n))

Also generates an error:

    Illegal type synonym family application in instance: n + 1
    In the data instance declaration for `TypeList'

I assume something like this must be possible. It's definitely possible using the notation:

data Zero
data Succ a

But I can't figure it out with the nicer looking version.

Answer 1

The type-level Nat improvements have landed in GHC 7.8 and this is now possible!

{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}

import GHC.TypeLits

data family List (n :: Nat) a
data instance List 0 a = Nil
data instance List n a = a ::: List (n - 1) a

infixr 8 :::

using List is just as natural as any []-like data structure you'd write yourself:

λ. :t 'a' ::: 'b' ::: 'c' ::: Nil
'a' ::: 'b' ::: 'c' ::: Nil :: List 3 Char