Lambda the Ultimate

Propositions as [Types], Steve Awodey and Adrej Bauer.

Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family.

We give rules for bracket types in dependent type theory and provide complete semantics using regular categories. We show that dependent type theory with the unit type, strong extensional equality types, strong dependent sums, and bracket types is the internal type theory of regular categories, in the same way that the usual dependent type theory with dependent sums and products is the internal type theory of locally cartesian closed categories.

We also show how to interpret first-order logic in type theory with brackets, and we make use of the translation to compare type theory with logic. Specifically, we show that the propositions-as-types interpretation is complete with respect to a certain fragment of intuitionistic first-order logic. As a consequence, a modified double-negation translation into type theory (without bracket types) is complete for all of classical first-order logic.

I figure I should say a few words about why proof irrelevance is an interesting idea. In math, you often want to consider elements of a certain type that have certain properties -- for example, you might want the set of satisfiable boolean formulas as part of a proof as a hypothesis of a theorem.

The way you might represent this in dependent type theory is by giving a pair, consisting of a formula and a satisfying assignment. You might write this as sigma f:Formula. assignment(f). The trouble is that the elements of this type really have more information than the subset contains; in addition to having formulas, you also have the assignments. So if you wanted to write a function that took values of this type computed satisfying assignments, then you could do it in constant time by just returning the second component of the pair, the evidence that it was satisfiable. This is not what you want, if your goal was to show that you could compute the satisfying assignment to a satisfiable formula.

One way of addressing this problem is to treat the second component of the pair as a proof irrelevant type. The basic idea is that for each type A, you make up a new type [A] which has either zero or one inhabitants, depending on whether A has any inhabitants or not. This means that you cannot make any computational use of data of type [A], because it doesn't have any structure to it. So if your solver receives a value of type sigma f:Formula. [assignment(f)], then you know that the formula is satisfiable, but you don't know what it is, because the second component is a bracket type. This means that your function will actually have to do the real work you intended.

I should also add that this is an old idea in type theory; this is the paper that made it clear to me.

(Thanks to Bob Harper for suggesting clarifications to my comments.)

Gradual Typing for Objects. Jeremy Siek and Walid Taha.

Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed a gradual type system for a functional calculus named [...]. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops [another calculus], a gradual type system for object-based languages, extending the [...] calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.

The authors' previous work on gradual typing was discussed here. This brings it to an object-oriented setting which is (as the abstract points out) very directly applicable to mainstream scripting languages, at least in principle.

[Edit: This is from the types list, where the authors also added: "We will present the paper at ECOOP 2007 and would be especially interested in any feedback on the paper before the final submission is due on April 25."]

The Missing Link - Dynamic Components for ML, Andreas Rossberg. ICFP 2006.

Despite its powerful module system, ML has not yet evolved for the modern world of dynamic and open modular programming, to which more primitive languages have adapted better so far. We present the design and semantics of a simple yet expressive first-class component system for ML. It provides dynamic linking in a type-safe and type-flexible manner, and allows selective execution in sandboxes. The system is defined solely by reduction to higher-order modules plus an extension with simple module-level dynamics, which we call packages. To represent components outside processes we employ generic pickling. We give a module calculus formalising the semantics of packages and pickling.

This is a very nice paper showing how to integrate dynamic loading into the ML module system. Er, I guess I'm repeating the abstract. I thought this paper, in addition to the feature it gave, was also a good demonstration of how to put the Dreyer-Crary-Harper account of ML modules to work.

Haven't seen this paper by Tim Sheard mentioned on Ltu before. As in previous papers Sheard tries to put Howard Curry to work in terms that are understandable for those that don't have a Phd in type theory.

Abstract:
Omega is an experimental system that combines features of both a programming language and a logical reasoning system. Omega is a language with an infinite hierarchy of computational levels. Terms at one level are classified (or typed) by terms at the next higher level. In this paper we report on using two different computational mechanisms. At the value level, computation is performed by reduction, and is largely unconstrained. At all higher levels, computation is performed by narrowing.

Termination Checking with Types, Andreas Abel. 2004.

The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces lambda+mu, a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

Recently on LtU, there has been a good deal of discussion about total functional programming, so I thought I'd link to an article that shows how to use typing to enforce termination. The main advantage of type-based approaches (as compared to analyzing the program text directly) is that the termination check is not as sensitive to the precise shape of the program; for example, you can beta-reduce a term and not alter whether the system thinks the program will terminate or not.

This paper is also nice because it provides a relatively simple example of bidirectional type checking, which is an important idea both practically (it reduces spurious type annotations and helps produce better error messages) and theoretically (it is intimately related to cut elimination).

State of the Union: Type Inference via Craig Interpolation, by Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu

The ad-hoc use of unions to encode disjoint sum types in C programs and the inability of C's type system to check the safe use of these unions is a long standing source of subtle bugs. We present a dependent type system that rigorously captures the ad-hoc protocols that programmers use to encode disjoint sums, and introduce a novel technique for automatically inferring, via Craig Interpolation, those dependent types and thus those protocols. In addition to checking the safe use of unions, the dependent type information inferred by interpolation gives programmers looking to modify or extend legacy code a precise understanding of the conditions under which some fields may be safely accessed. We present an empirical evaluation of our technique on 350KLOC of open source C code. In 80 out of 90 predicated edges (corresponding to 1472 out of 1684 union accesses), our type system is able to infer the correct dependent types. This demonstrates that our type system captures and explicates programmers' informal reasoning about unions, without requiring manual annotation or rewriting.

RZ for Constructive Mathematics in Programming by Chris Stone and Andrej Bauer.

Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

I haven't read the paper yet, but the abstract reminded me of PADS.

On Decidability of Nominal Subtyping with Variance. Andrew J. Kennedy, Benjamin C. Pierce. FOOL'07. January 2007

We investigate the algorithmics of subtyping in the presence of nominal inheritance and variance for generic types, as found in Java 5, Scala 2.0, and the .NET 2.0 Intermediate Language. We prove that the general problem is undecidable and characterize three different decidable fragments. From the latter, we conjecture that undecidability critically depends on the combination of three features that are not found together in any of these languages: contravariant type constructors, class hierarchies in which the set of types reachable from a given type by inheritance and decomposition is not always finite, and class hierarchies in which a type may have multiple supertypes with the same head constructor. These results settle one case of practical interest: subtyping between ground types in the .NET intermediate language is decidable; we conjecture that our proof can also be extended to show full decidability of subtyping in .NET. For Java and Scala, the decidability questions remain open; however, the proofs of our preliminary results introduce a number of novel techniques that we hope may be useful in further attacks on these questions.

The undecidability of subtyping is proved by reduction from the Post Correspondence Problem. Section 5 presents several decidable fragments.

Hot stuff!

Ott—a tool for writing definitions of programming languages and calculi.

Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms. For a simple example, here is an Ott source file for an untyped call-by-value lambda calculus (test10.ott), and the generated LaTeX (compiled to pdf) and (compiled to ps), Coq, Isabelle, and HOL definitions.

Most simply, the tool can be used to aid completely informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates good-quality typeset output. By parsing (and so sort-checking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.

That same input can be used to generate formal definitions, for Coq, HOL, and Isabelle. It should thereby enable a smooth transition between use of informal and formal mathematics. Additionally, the tool can automatically generate definitions of functions for free variables, single and multiple substitutions, subgrammar checks (e.g. for value subgrammars), and binding auxiliary functions. (At present only a fully concrete representation of binding is supported, without quotienting by alpha equivalence.)

The distribution includes several examples, in varying levels of completeness: untyped and simply typed lambda-calculus, a calculus with ML polymorphism, the POPLmark Fsub with and without records, an ML module system taken from (Leroy, JFP 1996) and equipped with an operational semantics, and LJ, a lightweight Java fragment.

Peter Sewell and his team continue to bridge the gap between the informal and formal worlds of programming language semantics.

We provide a functional specification of three central components of Simon Peyton Jones’s awkward squad: teletype I/O, mutable state and concurrency. By constructing an internal model of such concepts within our programming language, we can reason about programs that perform I/O as if they were pure functions. One important application of our approach is accommodating I/O in a dependently typed programming language.