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.
Thanks!
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$