If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a version of propositional logic where universal quantification over variables is allowed. But as polymorphism in HM is only allowed at the top level of types (as in forall a, b : a -> (b -> (a, b)) but not something like Int -> (forall a : a -> b).

Is this correct? And how is this system more powerful thatln simply typed lambda calculus?

  • $\begingroup$ Top level quantifications are also seen in logic in various circumstances. But I'm not sure this particular case has a name. $\endgroup$
    – Trebor
    Dec 20, 2023 at 3:26
  • $\begingroup$ @Trebor would you say that what I said is correct? $\endgroup$
    – pgmcr
    Dec 21, 2023 at 4:15


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.