Under 'What is Hindley Milner' it states:
Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.
My question is, What is an example of a type available in System F, that is not available in Hindley Milner (type inference)?
(The assumption being that the inference of System F types has been proven undecideable)
Hindley/Milner does not support higher-rank polymorphic types, i.e., types where the universal quantifier is nested into some larger type (i.e., any notion of first-class polymorphism).
One of the simplest example would be e.g.:
f : (∀α. α → α) → int × string
f id = (id 4, id "boo")
Inferring higher-rank polymorphism is known to be undecidable in general. Similar limitations apply to recursion: a recursive definition cannot have polymorphic recursive uses. For a contrived example:
g : ∀α. int × α → int
g (n,x) = if n = 0 then 0 else if odd n then g (n-1, 3) else g (n-1, "boo")
This is kind of unsurprising given the above, and the fact that a recursive definition like the above is just a shorthand for applying the higher-order Y combinator at a polymorphic type, which would again require (impredicative) first-class polymorphism.
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句