[Haskell-cafe] Learning GADT types to simulate dependent types

[Daniel Fischer]

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