[Haskell-cafe] Re: Typechecker to GADT: the full implementation
of a typed DSL
ryani.spam at gmail.com
Mon Oct 8 02:58:11 EDT 2007
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.
More information about the Haskell-Cafe