Am Samstag, 28. Juni 2008 19:51 schrieb Paul Johnson: > 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? > > Thanks, > > Paul. >
My Oleg rating isn't high either, and certainly you can do it more elegant, but class Concat l1 l2 l3 | l1 l2 -> l3, l1 l3 -> l2 where pConcat :: l1 a -> l2 a -> l3 a instance Concat (Plist Zero) (Plist n) (Plist n) where pConcat _ ys = ys instance Concat (Plist n1) (Plist n2) (Plist t) => Concat (Plist (S n1)) (Plist n2) (Plist (S t)) where pConcat (x :| xs) ys = x :| pConcat xs ys works, you don't even need the Add class then - btw, you'd want instance Add n1 n2 t => Add (S n1) n2 (S t) anyway. Cheers, Daniel _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe