The F-semantics of types for the &lgr;-calculus assigns to a functional type an element of F, the subdomain of a &lgr;-calculus model that contains canonical representations of functions. This paper studies the completeness ( F-completeness ) of the intersection type discipline for Curry’s typing scheme (i.e., in which a universal type &ohgr; and an intersection operator ∧ for type formation are introduced) with respect to the F-semantics. The main theorem states that a type assignment induced by a type theory is F-complete iff (1) the rule of invariance of types under &bgr;-conversion and (2) Hindley’s Rule ( &psgr; ∧ &ohgr; ⁿ → &ohgr; M ⊧ &psgr; ( &lgr; y ₁ ... y _n. M y ₁ ... y _n ) ) can be derived from the type theory. The rest of the paper gives an approximation theorem for such theories and discusses four type theory examples related to those ideas. In particular, a restricted type assignment is introduced that is both F-complete and F-sound (sound with relation to the F-semantics).

This theoretical paper is, in fact, a progress report on “results and ideas which have been discussed at length by Coppo and Hindley with the authors.” So few motivational remarks and explanations are provided, and some proofs are just indicated by references to other publications. This should limit its audience to theoreticians and logicians working on semantic models of &lgr;-calculus.