Encoding Lists with Lengths by Type Family
scm at iis.sinica.edu.tw
Sat Dec 8 21:50:40 EST 2007
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?
More information about the Glasgow-haskell-users