[Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.

[Tillmann Rendel]

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