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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
