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

[Ryan Ingram]

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.

Consider this function definition:
 typechecka' :: Maybe (EQ ta t2) -> Typ tb -> Term (ta->tb) -> Term t2 ->
                Either String MostlyStatic
 typechecka' (Just Refl) tb e1 e2 = Right $ MostlyStatic (tb,App e1 e2)

On the RHS of the =, ta and t2 are unified to the same type (because
of the pattern-match on the GADT "Refl").  Without that, "App e1 e2"
won't typecheck, because e1 :: Term (ta -> tb) and e2 :: Term t2.
Once you have a witness that those are the same type, however, the
typechecker will unify ta and t2 and App can typecheck.

   -- ryan