On 10/4/07, Pasqualino 'Titto' Assini <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
