An algebraic semantics of higher-order types with subtypes

Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. They did not, however, give a semantics of contracts. The lack of a semantics makes it impossible to define and prove soundness and completeness of the checking algorithm. (Given a semantics, a sound checker never reports violations that do not exist under that semantics; a complete checker is – in principle – able to find violations when violations exist.) Ideally, a semantics should capture what programmers intuitively feel is the meaning of a contract or otherwise clearly point out where intuition does not match reality. In this paper we give an interpretation of contracts for which we prove the Findler-Felleisen algorithm sound and (under reasonable assumptions) complete. While our semantics mostly matches intuition, it also exposes a problem with predicate contracts where an arguably more intuitive interpretation than ours would render the checking algorithm unsound. In our semantics we have to make use of a notion of safety (which we define in the paper) to avoid unsoundness. We are able to eliminate the “leakage” of safety into the semantics by changing the language, replacing the original version of unrestricted predicate contracts with a restricted form. The corresponding loss in expressive power can be recovered by making safety explicit as a contract. This can be done either in ad-hoc fashion or by including general recursive contracts. The addition of recursive contracts has far-reaching implications, deeply affecting the formulation of our model and requiring different techniques for proving soundness.

Download Full-text

The complexity of type inference for higher-order typed lambda calculi

Journal of Functional Programming ◽

10.1017/s0956796800001143 ◽

1994 ◽

Vol 4 (4) ◽

pp. 435-477 ◽

Cited By ~ 9

Author(s):

Fritz Henglein ◽

Harry G. Mairson

Keyword(s):

Lower Bounds ◽

Higher Order ◽

Type Inference ◽

Boolean Logic ◽

Turing Machines ◽

Technical Tool ◽

Inference Problem ◽

Exponential Time ◽

First Order ◽

Order Types

AbstractWe analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus (F2) invented by Girard and Reynolds, as well as higher-order extensions F3, F4, …, Fω proposed by Girard. We prove that recognising the F2-typable terms requires exponential time, and for Fω the problem is non-elementary. We show as well a sequence of lower bounds on recognising the Fk-typable terms, where the bound for Fk+1 is exponentially larger than that for Fk.The lower bounds are based on generic simulation of Turing Machines, where computation is simulated at the expression and type level simultaneously. Non-accepting computations are mapped to non-normalising reduction sequences, and hence non-typable terms. The accepting computations are mapped to typable terms, where higher-order types encode reduction sequences, and first-order types encode the entire computation as a circuit, based on a unification simulation of Boolean logic. A primary technical tool in this reduction is the composition of polymorphic functions having different domains and ranges.These results are the first nontrivial lower bounds on type inference for the Girard/Reynolds system as well as its higher-order extensions. We hope that the analysis provides important combinatorial insights which will prove useful in the ultimate resolution of the complexity of the type inference problem.

Download Full-text

Categorical semantics for higher order polymorphic lambda calculus

Journal of Symbolic Logic ◽

10.2307/2273831 ◽

1987 ◽

Vol 52 (4) ◽

pp. 969-989 ◽

Cited By ~ 77

Author(s):

R. A. G. Seely

Keyword(s):

Lambda Calculus ◽

Higher Order ◽

Algebraic Semantics ◽

Categorical Structure ◽

Categorical Semantics ◽

Definitional Extension

AbstractA categorical structure suitable for interpreting polymorphic lambda calculus (PLC) is defined, providing an algebraic semantics for PLC which is sound and complete. In fact, there is an equivalence between the theories and the categories. Also presented is a definitional extension of PLC including “subtypes”, for example, equality subtypes, together with a construction providing models of the extended language, and a context for Girard's extension of the Dialectica interpretation.

Download Full-text

A denotational semantics for the symmetric interaction combinators

Mathematical Structures in Computer Science ◽

10.1017/s0960129507006135 ◽

2007 ◽

Vol 17 (3) ◽

pp. 527-562 ◽

Cited By ~ 4

Author(s):

DAMIANO MAZZA

Keyword(s):

Linear Logic ◽

Denotational Semantics ◽

Distributed Computation ◽

Higher Order ◽

Parallel Execution ◽

Turing Machines ◽

Algebraic Semantics ◽

Relational Semantics ◽

Completeness Result ◽

Higher Order Functions

The symmetric interaction combinators are a variant of Lafont's interaction combinators. They enjoy a weaker universality property with respect to interaction nets, but are equally expressive. They are a model of deterministic distributed computation and share the good properties of Turing machines (elementary reductions) and of the λ-calculus (higher-order functions and parallel execution). We introduce a denotational semantics for this system, which is inspired by the relational semantics for linear logic, and prove an injectivity and full completeness result for it. We also consider the algebraic semantics defined by Lafont, and prove that the two are strongly related.

Download Full-text