Is Milner let polymorphism a rank 2 feature?

Question

let a = b in c can be thought as a syntactic sugar for (\a -> c) b, but in a typed setting in general it's not the case. For example, in the Milner calculus let a = \x -> x in (a True, a 1) is typable, but seemingly equivalent (\a -> (a True, a 1)) (\x -> x) is not.

However, the latter is typable in System F with a rank 2 type for the first lambda.

My questions are:

• Is let polymorphism a rank 2 feature that sneaked secretly in the otherwise rank 1 world of Milner calculus?

• The purpose of having of separate let construct seems to specify which types should be generalized by type checker, and which are not. Does it serve any other purposes? Are there any reasons to extend more powerful systems e.g. System F with separate let which is not sugar? Are there any papers on the rationale behind the design of the Milner calculus which no longer seems obvious to me?

• Is there the most general type for \a -> (a True, a 1) in System F?

• Are there type systems closed under beta expansion? I.e. if P is typable and M N = P then M is typable?

Some clarifications:

• By equivalence I mean equivalence modulo type annotations. Is 'System F a la Church' the correct term for that?

• I know that in general the principal typing property doesn't hold in F, but a principal type could exist for my particular term.

• By let I mean the non-recursive flavour of let. Extension of system F with recursive let is obviously useful as it allows for non-termination.

Answer 1

W.r.t. to the four questions asked:

• A key insight in this matter is that rather than just typing a lambda-abstraction with a potentially polymorphic argument type, we are typing a (sugared) abstraction that is (1) applied exactly once and, moreover, that is (2) applied to a statically known argument. That is, we can first subject the "argument" (i.e. the definiens of the local definition) to type reconstruction to find its (polymorphic) type; then assign the found type to the "parameter" (the definiendum); and then, finally, type the body in the extended type context.

  Note that that is considerably more easy than general rank-2 type inference.

• Note that, strictly speaking, let .. = .. in .. is only syntactic sugar in System F if you demand that the definiendum carries a type annotation: let .. : .. = .. in .. .

• Here are two solutions for T in (\a :: T -> (a True, a 1)) in System F: forall b. (forall a. a -> b) -> (b, b) and forall c d. (forall a b. a -> b) -> (c, d). Note that neither one of them is more general than the other. In general, System F does not admit principal types.

• I suppose this holds for the simply typed lambda-calculus?

Answer 2

Types are not preserved under beta-expansion in any calculus that can express the concept of "dead code". You can probably figure out how to write something similar to this in any usable language:

if True then something typable else utter nonsense

For example, let M = (\x y -> x) (something typable) and N = (utter nonsense) and P = (something typable), so that M N = P, and P is typable, but M N isn't.

...rereading your question, I see that you only demand that M be typable, but that seems like a very strange meaning to give to "preserved under beta-expansion" to me. Anyway, I don't see why some argument like the above couldn't apply: simply let M have some untypable dead code in it.