scholarly journals Operations with Higher-Order Types of Asymptotic Variation: Filling Some Gaps

2021 ◽  
Vol 11 (08) ◽  
pp. 687-716
Author(s):  
Antonio Granata
Keyword(s):  
Higher Order ◽  
Order Types

Sound and complete models of contracts

2006 ◽  
Vol 16 (4-5) ◽  
pp. 375-414 ◽  
Author(s):  
MATTHIAS BLUME ◽  
DAVID McALLESTER
Keyword(s):  
Ad Hoc ◽  
Expressive Power ◽  
Higher Order ◽  
Original Version ◽  
Order Types ◽  
Restricted Form ◽  
Soundness And Completeness ◽  
Recursive Contracts ◽  
Intuitive Interpretation ◽  
Typed Languages

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.

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

1994 ◽  
Vol 4 (4) ◽  
pp. 435-477 ◽  
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.

Using Quantification at Higher-Order Types

2012 ◽  
pp. 118-149
Author(s):  
Dale Miller ◽  
Gopalan Nadathur
Keyword(s):  
Higher Order ◽  
Order Types

scholarly journals Towards Higher-Order Types

1998 ◽  
Vol 14 ◽  
pp. 38-51
Author(s):  
Carlos Camarão ◽  
Lucília Figueiredo
Keyword(s):  
Higher Order ◽  
Order Types

scholarly journals Constructive natural deduction and its ‘ω-set’ interpretation

1991 ◽  
Vol 1 (2) ◽  
pp. 215-254 ◽  
Author(s):  
Giuseppe Longo ◽  
Eugenio Moggi
Keyword(s):  
Type Theory ◽  
Natural Deduction ◽  
Expressive Power ◽  
Higher Order ◽  
Second Order ◽  
Deduction Theorem ◽  
Natural Numbers ◽  
Experienced Reader ◽  
Order Types ◽  
The Universe

Various Theories of Types are introduced, by stressing the analogy ‘propositions-as-types’: from propositional to higher order types (and Logic). In accordance with this, proofs are described as terms of various calculi, in particular of polymorphic (second order) λ-calculus. A semantic explanation is then given by interpreting individual types and the collection of all types in two simple categories built out of the natural numbers (the modest sets and the universe of ω-sets). The first part of this paper (syntax) may be viewed as a short tutorial with a constructive understanding of the deduction theorem and some work on the expressive power of first and second order quantification. Also in the second part (semantics, §§6–7) the presentation is meant to be elementary, even though we introduce some new facts on types as quotient sets in order to interpret ‘explicit polymorphism’. (The experienced reader in Type Theory may directly go, at first reading, to §§6–8).

Sign in / Sign up

Export Citation Format

Share Document