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