[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