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

Paul Johnson paul at cogito.org.uk
Sat Jun 28 16:28:40 EDT 2008


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.


More information about the Haskell-Cafe mailing list