Encoding Lists with Lengths by Type Family
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
I've typechecked this by hand, and indeed it looks to me as if it should work. (Admittedly, your inAssocL function is making an unsubstantiated claim (since you define it as 'undefined'), but that is still sound since any attempt to run the program will diverge. But it should tpyecheck.) Here is my calculation, for the Cons case of | > 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)) y :: List a n x :: List a k, where m ~ Suc k Cons a y : List a Suc n revcat x (Cons a y) :: List a (Plus k (Suc n)) subst inAssocL (revcat x (Cons a y)) :: List a (Plus (Suc k) n) So to make the result type match up with the type of the RHS we need m ~ Suc k => List a (Plus m n) ~ List a (Plus (Suc k) n) which is of course the case. Manuel has made some recent changes -- I have not seen if they fix this. Simon
participants (2)
-
Shin-Cheng Mu -
Simon Peyton-Jones