Re: [Haskell-cafe] Re: Typechecker to GADT: the full implementation of a typed DSL

On 10/7/07, Ryan Ingram wrote:

On 10/4/07, Pasqualino 'Titto' Assini 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