I can undestand some evidences that Hindley-Milner(HM) is a subsystem of System-F. HM only allows $\forall$ in the left of a monotype (or other $\forall$). System-F allows $\forall$ anywhere in the type and allows to pass polymorphic terms uninstantiated to functions (say $\lambda f.(f\: True, f\: 1)$).

But, how every well-typed term in HM is well a well-typed term in System-F?

First, we should make every term in HM be a term in System-F.

So the crutial step is to convert $let$ terms in HM to some $\lambda$-term in System-F. Would the naive interpretation

$let\: x\: =\: e_1\: in\: e_2 \equiv (\lambda x.e_2)e_1$

be enough?


Also observed that both systems don't have the same deductive rules.

  • $\begingroup$ What reference are you using for the system you call $HM$? Depending on how you set things up, "let" can introduce problems in polymorphic formulations of simple type theory. $\endgroup$
    – Rob Arthan
    Feb 16, 2017 at 0:28
  • $\begingroup$ @RobArthan Principal type-schemes for functional programs, by Damas and Milner. $\endgroup$ Feb 16, 2017 at 0:29


You must log in to answer this question.

Browse other questions tagged .