Hi Kim-Ee,
Kim-Ee Yeoh wrote:
[...] I guess this is related to your view of [...]
Do you have a reference to the previous conversation?
Sorry, I mean "related to one's view of", not "related to Johannes
Waldmanns' view of".
Which seems miles away from what you're alluding to. Full-blown
type-level programming? Operational semantics at the type-level? I'm
not sure.
That's not what I tried to allude to. I mean the operational semantics
of instantiation and generalization *at the term level*. In System F,
there are two contraction rules: The usual β rule
(λx : τ . e1) e2 ~> subst e2 for x in e1
and an additional β-like rule for type application and abstraction:
(Λα . e) [τ] ~> subst τ for α in e
So in System F, type application and type abstraction have computational
content. I think this can become visible in GHC Haskell as well, but I
cannot find an example without type classes. Maybe I'm wrong.
Tillmann
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
