On 10/7/07, Ryan Ingram <[EMAIL PROTECTED]> wrote: > On 10/4/07, Pasqualino 'Titto' Assini <[EMAIL PROTECTED]> wrote: > > My mental typechecker seems to diverge on the "data EQ a b where Refl :: > > EQ > > a a" bit so I am now reading the "typing dynamic typing" paper, hoping for > > further enlightment. > > Basically, if you have "Refl :: Eq a b", it provides a witness that > the types a and b are really the same type.
Also, something that might make it simpler to understand is that the "a" and "b" in the initial GADT declaration are irrelevant (and totally ignored). Here is an equivalent definition: data EQ :: * -> * -> * where Refl :: EQ a a -- ryan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe