I'm on the Wikipedia page for Hindley-Milner type systems, on the section about "let polymorphism": https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Let-polymorphism

I'm a bit confused on this sentence:

Ideally, this would be allowed with any use of a bound variable

What does that mean exactly? I'm not following the syntax in this section.


  • 3
    $\begingroup$ As far as I can tell that section is just poorly written. What you should get out of it is that HM can only generalize let bound functions, and that this change (or some change) is necessary because type inference (and type checking) are undecidable in the polymorphic lambda calculus. If you've understood that, I wouldn't put any more effort into deciphering what the author of that section intended. $\endgroup$ Jan 23, 2019 at 22:24


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.