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

[Dan Doel]

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