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

Ryan Ingram 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

  -- ryan

More information about the Haskell-Cafe mailing list