I just wanted to mention that John's idea
of two different forms of binding, a polymorphic one
with repeated evaluation and a monomorphic one with single evaluation, is not new.
It is also in Xavier Leroy's PhD thesis "Polymorphic Typing of an Algorithmic
Language",
where he suggests two different let's.
The context there was an ML dialect with references.
So, strict evaluation + side-effects. In this system
polymorphic references were possible, because the polymorphism
required a re-evaluation of the reference.
Another way to look at it is by making type abstractions
explicit and thinking of a type abstraction as a specific form of closure.
At every type application we evaluate the body of this closure.
Stefan Kahrs
