On Saturday 28 June 2008, Paul Johnson wrote:
I'm trying to understand how to use GADT types to simulate dependent types. I'm trying to write a version of list that uses Peano numbers in the types to keep track of how many elements are in the list. Like this:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Plist where
infixr 3 :|
data Zero
data S a
class Add n1 n2 t | n1 n2 -> t, n1 t -> n2
instance Add Zero n n instance Add (S n1) n2 (S t)
data Plist n a where Nil :: Plist Zero a (:|) :: a -> Plist n a -> Plist (S n) a
instance (Show a) => Show (Plist n a) where show Nil = "Nil" show (x :| xs) = show x ++ " :| " ++ show xs
pHead :: Plist (S n) a -> a pHead (x :| _) = x
pTail :: Plist (S n) a -> Plist n a pTail (_ :| xs) = xs
pConcat Nil ys = ys pConcat (x :| xs) ys = x :| pConcat xs ys
Everything works except the last function (pConcat). I figured that it should add the lengths of its arguments together, so I created a class Add as shown in the Haskell Wiki at http://www.haskell.org/haskellwiki/Type_arithmetic. But now I'm stuck. When I try to load this module I get:
Plist.hs:32:8: GADT pattern match in non-rigid context for `Nil' Tell GHC HQ if you'd like this to unify the context In the pattern: Nil In the definition of `pConcat': pConcat Nil ys = ys Failed, modules loaded: none.
(Line 32 is "pConcat Nil ys = ys")
So how do I do this? Am I on the right track? Can someone help improve my Oleg rating?
There are a couple issues that jump out at me. First, your second instance for Add is a bit off. It should be more like: instance (Add n1 n2 t) => Add (S n1) n2 (S t) Second, the reason you're getting that particular error with pConcat is that it doesn't have a type signature. Matching on GADTs requires one. However, fixing those here, I still got errors, and I'm not enough of a type class/fundep wizard to know what the problem is. Instead, I might suggest using type families for the type-level arithmetic: type family Add n1 n2 :: * type instance Add Zero n2 = n2 type instance Add (S n1) n2 = S (Add n1 n2) Then the signature of pConcat becomes: pConcat :: Plist m a -> Plist n a -> Plist (Add m n) a Which works fine. As an added bonus, the type family doesn't require undecidable instances like the type class does. Type families are a bit iffy in 6.8.*, but they'll work all right for simple stuff like this, at least. Cheers, -- Dan