[Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.
rendel at informatik.uni-marburg.de
Wed Apr 3 20:04:29 CEST 2013
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.
More information about the Haskell-Cafe