Encoding Lists with Lengths by Type Family

[Shin-Cheng Mu]

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
for Haskell:

 > 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