Investigations in intersection types : confluence, and semantics of expansion in the -calculus, and a type error slicing method
Abstract
Type systems were invented in the early 1900s to provide foundations for Mathematics
where types were used to avoid paradoxes. Type systems have then been
developed and extended throughout the years to serve different purposes such as efficiency
or expressiveness. The λ-calculus is used in programming languages, logic,
mathematics, and linguistics. Intersection types are a kind of types used for building
semantic models of the λ-calculus and for static analysis of computer programs.
The confluence property was used to prove the λ-calculus’ consistency and the
uniqueness of normal forms. Confluence is useful to show that logics are sensibly
designed, and to make equality decision procedures for use in theorem provers.
Some proofs of the λ-calculus’ confluence are based on syntactic concepts (reduction
relations and λ-term sets) and some on semantic concepts (type interpretations).
Part I of this thesis presents an original syntactic proof that is a simplification of
a semantic proof based on a sound type interpretation w.r.t. an intersection type
system. Our proof can be seen as bridging some semantic and syntactic proofs.
Expansion is an operation on typings (pairs of type environments and result
types) in type systems for the λ-calculus. It was introduced to prove that the principal
typing property (i.e., that every typable term has a strongest typing) holds
in intersection type systems. Expansion variables were introduced to simplify the
expansion mechanism. Part II of this thesis presents a complete realisability semantics
w.r.t. an intersection type system with infinitely many expansion variables.
This represents the first study on semantics of expansion. Providing sound (and
complete) realisability semantics allows one to study the algorithmic behaviour of
typed λ-terms through their types w.r.t. a type system. We believe such semantics
will cast some light on the not yet well understood expansion operation.
Intersection types were used in a type error slicer for the SML programming
language. Existing compilers for many languages have confusing type error messages.
Type error slicing (TES) helps the programmer by isolating the part of a program
contributing to a type error (a slice). TES was initially done for a tiny toy language
(the λ-calculus with polymorphic let-expressions). Extending TES to a full language
is extremely challenging, and for SML we needed a number of innovations. Some
issues would be faced for any language, and some are SML-specific but representative
of the complexity of language-specific issues likely to be faced for other languages.
Part III of this thesis solves both kinds of issues and presents an original, simple,
and general constraint system for providing type error slices for ill-typed programs.
We believe TES helps demystify language features known to confuse users.