Encoding Lists with Lengths by Type Family

8 Dec 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
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

Encoding Lists with Lengths by Type Family

Shin-Cheng Mu