Hi Tillmann,
On Wed, Apr 3, 2013 at 11:59 PM, Tillmann Rendel
From the type-theoretic point of view, I guess this is related to your view of what a polymorphic function is.
Do you have a reference to the previous conversation?
but we moved further and further towards the System-F-ish view that polymorphism is an explicit, computational thing.
While that may be true, I read the original email as merely referring to the explicit annotation of types (where they are customarily neither seen nor written) as a particular pedagogical approach for new students, something which has much to recommend for. 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. -- Kim-Ee