Let-polymorphism is Fundamentally Flawed

On Oct 19, 2012, I gave a talk on type systems at Indiana Universitys Programming Languages Group. Based on my research and experience of implementing type systems, I briefly described my understanding of the Hindley-Milner type system and its various enhancements. I described an observation of let-polymorphism (an important feature in the HM system) that it is the analogy to dynamic scoping, but reincarnated in a type-level language. The forall quantifiers in the types are put in random and unprincipled places which is causing undesirable interferences with many other language features (such as side-effects and first-class continuations).

Because let-polymorphism has been deeply rooted in the very beginning of the HM system, it is very unlikely that any enhancement can get over it without changing the fundamental properties of the system (such as being able to infer parameter types without any annotations). Thus I think the various enhancements to the HM system, such as value restriction, MLF etc cant really get the system both correct and general.