I have often been careless about the conventions regarding use of the terms rank, order, and degree: I apologise for any confusion that might result.Įither way, the apply function does not have higher rank, it's perfectly rank 1. But that is meta notation, and A and B are meta-level variables standing for an arbitrary simple type.īoth Church-style and Curry-style formalisms use schemes. It's true that when people talk about STLC types they often write down type 'schemes' like A->B->B. So ML-style polymorphism, and system F, don't have much to do with the point I was making.

Whereas terms with ML-style let statements cannot be translated into the STLC without blowing up the size of the term. Hindley-Milner-style STLC are exactly equivalent in terms of the lambda terms they define. Note that this is a more sophisticated form of polymorphism. I should have made this clear.Ī lambda calculus with H-M-style implicit let polymorphism is typically just called ML in the PL literature I invented the term, because I thought Hindley-Milner polymorphism would be more immediately comprehensible than the explanation I gave above about Church-style and Curry-style typing. There is no such thing as a 'Hindley-Milner STLC' either. The original reference for the simply-typed lambda calculus is Curry & Feys (1958), which used Curry-style typing - this was natural since they wanted to model Hilbert-style proof theory, which uses a precisely analogous form of formula scheme. With the benefit of the Hindley-Milner algorithm, we see that there is a principal type, and this is the type obtained from algorithm W. Whereas Curry-style typing does not provide type information to lambda terms, being in a sense underspecified, which means that typable terms may admit many possible type assignments.

Church-style typing decorates lambda terms with enough type annotations so that each typable term has exactly one non-schematic type. I don't think this assertion is defensible. So his proof implies PTIME-completeness of simple type inference even when restricted to affine/linear lambda terms.The very meaning of 'simply typed' is no polymorphism Moreover, Mairson's encoding of the circuit value problem has the property that the terms representing boolean circuits are affine (variables used at most once), and in Section 2 of the paper he gives another encoding that produces linear terms (variables used exactly once). This implies PTIME-completeness, since simple type inference can be performed efficiently using first-order unification. This is strictly speaking a functional problem ('Given a term $t$, compute its principal type'), but Mairson shows that the corresponding decision problem ('Given a term $t$ and type $A$, is $A$ the principal type of $t$?') is PTIME-hard, by reduction from the circuit value problem.

To be a bit more precise, here 'type inference' is taken to mean the problem of computing the principal simple type of an untyped lambda term. Type inference for simply typed lambda calculus is complete for polynomial time, as elegantly explained in section 1 of Harry Mairson's Linear lambda calculus and PTIME-completeness.

Typed lambda calculus