Learning GADT types to simulate dependent types
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.
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
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
Daniel Fischer wrote:
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.
Thanks, and also thanks to Dan Doel who showed how to do it with the new type families. I'll stick with the Fundeps solution here for the moment until type families settle down, but that method is cleaner. I was also able to write this: class Concat p1 p2 p3 | p1 p2 -> p3, p1 p3 -> p2 where pConcat :: p1 a -> p2 a -> p3 a pBogus :: p1 a -> p2 a -> p3 a instance Concat (Plist Zero) (Plist n) (Plist n) where pConcat _ ys = ys pBogus _ 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 pBogus xs ys = ys And indeed the second definition of pBogus gave me a compile-time type error because the length of the result didn't agree with the type length. I'm going to be doing a presentation on Haskell for my boss soon, and this should definitely impress (he has a solid coding background). Thanks again, Paul.
participants (3)
-
Dan Doel -
Daniel Fischer -
Paul Johnson