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