# Encoding Lists with Lengths by Type Family

Shin-Cheng Mu scm at iis.sinica.edu.tw
Sat Dec 8 21:50:40 EST 2007

```Hi,

I understand that the type family is still an experimental feature
in GHC. This is just a confirmation whether it is a bug, or is
what the designers intended.

I am curious how much "dependent type" programming I can
emulate using GADT and type family. Therefore I started with
the typical "list with length" example. List a n is a list
of elements a and length n encoded by singleton types Zero
and Suc, as was done in the paper Towards Open Type Functions

> data Zero = Zero
> data Suc a = Suc a

> data List a n where
>   Nil :: List a Zero
>   Cons :: a -> List a n -> List a (Suc n)

Concatenation effortlessly type checks!

> cat :: List a m -> List a n -> List a (Plus m n)
> cat Nil y = y
> cat (Cons a x) y = Cons a (cat x y)

However, I was not able to convince GHC that the following
function revcat, list reversal using an accumulating parameter,
is type correct:

> revcat :: List a m -> List a n -> List a (Plus m n)
> revcat Nil y = y
> revcat (Cons a x) y =
>    subst incAssocL (revcat x (Cons a y))

In the recursive case, (Cons a x) has type List a (Suc m)
and y has type List a n. The recursive call to revcat is
supposed to yield a list of type:

List a (Plus m (Suc n))

while we want the return type to be

List a (Plus (Suc m) n)

Therefore I shall provide a conversion proving that they
are actually the same thing. Currently I give the types
only and will think about how to implement them later:

> subst :: (m -> n) -> List a m -> List a n
> subst = undefined

> incAssocL :: Plus m (Suc n) -> Plus (Suc m) n
> incAssocL = undefined

However, GHCi (run with options -XTypeFamilies -XGADTs)
gave me the following error message:

Couldn't match expected type `Plus n3 n2'
against inferred type `Plus m n1'
Expected type: Plus m (Suc n1) -> Plus (Suc n3) n2
Inferred type: Plus m (Suc n1) -> Plus (Suc m) n1
In the first argument of `subst', namely `incAssocL'
In the expression: subst incAssocL (revcat x (Cons a y))

For some reason GHC wanted me to return the more general
type Plus (Suc n3) n2 where n2 and n3 are fresh, rather
than unifying n2 with m and n2 with n.

Why is that?

sincerely,
Shin

```