title: Is Milner let polymorphism a rank 2 feature?
body: <p><code>let a = b in c</code> can be thought as a syntactic sugar for <code>(\a -&gt; c) b</code>, but in a typed setting in general it's not the case. For example, in the Milner calculus <code>let a = \x -&gt; x in (a True, a 1)</code> is typable, but seemingly equivalent <code>(\a -&gt; (a True, a 1)) (\x -&gt; x)</code> is not.</p>
  
  <p>However, the latter is typable in System F with a rank 2 type for the first lambda.</p>
  
  <p>My questions are:</p>
  
  <ul>
  <li><p>Is let polymorphism a rank 2 feature that sneaked secretly in the otherwise rank 1 world of Milner calculus?</p></li>
  <li><p>The purpose of having of separate <code>let</code> 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 <code>let</code> 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?</p></li>
  <li><p>Is there the most general type for <code>\a -&gt; (a True, a 1)</code> in System F?</p></li>
  <li><p>Are there type systems closed under beta expansion? I.e. if P is typable and M N = P then M is typable?</p></li>
  </ul>
  
  <p>Some clarifications:</p>
  
  <ul>
  <li><p>By equivalence I mean equivalence modulo type annotations. Is 'System F a la Church' the correct term for that?</p></li>
  <li><p>I know that in general the principal typing property doesn't hold in F, but a principal type could exist for my particular term.</p></li>
  <li><p>By <code>let</code> I mean the non-recursive flavour of <code>let</code>. Extension of system F with recursive let is obviously useful as it allows for non-termination.</p></li>
  </ul>