Comment Comment by benbataille > Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1.This equivalence does not hold in the HM formalisation. It's well explained in the Wikipedia article : http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism[Abs] is monomorphic while [Let] is polymorphic. Using the Wikipedia article exemple : \f.(f true, f 0) will not be typed while let f = \x.x in (f true, f 0) will be reduced to (bool, int). parent benbataille 13 years ago
This equivalence does not hold in the HM formalisation. It's well explained in the Wikipedia article : http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism
[Abs] is monomorphic while [Let] is polymorphic. Using the Wikipedia article exemple : \f.(f true, f 0) will not be typed while let f = \x.x in (f true, f 0) will be reduced to (bool, int).