[Haskell-cafe] Re: Typechecker to GADT: the full implementation
of a typed DSL
ryani.spam at gmail.com
Mon Oct 8 02:59:54 EDT 2007
On 10/7/07, Ryan Ingram <ryani.spam at gmail.com> wrote:
> On 10/4/07, Pasqualino 'Titto' Assini <tittoassini at gmail.com> 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
More information about the Haskell-Cafe