[Prev][Next][Index][Thread]
Un/typed lambda calculus
Date: Mon, 10 Oct 88 14:29:33 BST
To: types@theory.LCS.MIT.EDU
I'd like to make a few remarks in reply to John's outline and, in particular,
to the responses of Garrel Pottinger and Matthias Felleisen.
Whether or not the type-free lambda calculus is the ``substrate'' of all type
systems depends on your point of view. Garrel seems to emphasize the
Curry-Hindley program of studying type assignment for untyped lambda terms,
whereas John's proposal emphasizes the use of so-called explicitly-typed
function calculi. Taken at face value, the latter approach does not rely on
the untyped lambda calculus at all, and can be understood in isolation from
it. But the deeper issue, one that is raised by Matthias's remarks, is the
relation of typing assertions to the semantics of programs.
In an explicitly-typed approach, types are just annotations that are used in
two ways. First, they are used in the inductive definition of the well-formed
expressions (and are attached to terms primarily to achieve decidability of
type checking). Second, they are used to index an equivalence relation
representing equality for terms of that type. It is to be emphasized that in
this approach the triple A |- M : tau has no semantic content: it is merely a
notation for expressing the well-formedness of M in a given context.
In a type assignment system types HAVE semantic content: A |- M : tau means
that in all untyped lambda models, the denotation of M lies within the set
determined by tau (and the set determined by tau is determined in a uniform
way for all models, up to choice of base types.) This view justifies taking
the rule of subject conversion in type assignment systems. Here typing is an
assertion about the behavior of M under application (although, as Garrel
points out, this is not the only possibility).
With regard to Matthias's question, it seems to me that the role of types in
explicitly-typed function calculi is exactly analogous to dimensional analysis
in the physical sciences. But their role in systems of type assignment is
quite different: they are used to express properties of terms under conversion
(as Garrel emphasized). In this way type assignment systems are just a form
of programming logic for functional programs, with typing playing the role of
predication.
But there's something not quite right about the type assignment view with
respect to programming: programming languages are defined by an operational
semantics, and programs are to be understood with respect to this operational
semantics. In systems of type assignment the principles of reasoning are
limited by the fact that the assertions are about conversion classes of terms,
in other words about programs with respect to an arbitrary, unspecified
operational semantics. This is not an accurate view of programming, and does
not lead, it seems to me, to an appropriate logic of programs. The third way,
introduced by Martin-Lof and promoted by Constable's group at Cornell, is to
take the semantic view of types characteristic of systems of type assignment,
but to take the meaning of A |- M : tau to be relative to a FIXED
operational intepretation. In this way one obtains a proper programming logic
for functional programs that can be used to reason about a specific
programming language and to state precise properties about the execution
(evaluation) of such terms. Types in this setting are used to express
properties that go far beyond mere dimensional analysis.
John remarked that explicitly-typed systems enjoy various technical properties
that are useful in the development of the theory. In reply, it seems
worthwhile to point out that this third approach completely avoids questions
related to conversion and reduction since these relations never enter into the
story. Universality is not an issue here, for the underlying programming
language can always be taken to be Turing universal.
Furthermore, the approach is compatible with both a total (as in Martin-Lof)
or partial correctness approach to programming logic (although the latter is
incompatible with the straightforward application of props-as-types to reduce
all logical reasoning to typing assertions). It is also compatible with
Garrel's view that the untyped lambda calculus underlies the typed systems in
the sense that the programs M are usually taken as untyped terms in some
lambda-calculus-like language. It remains to be seen whether the approach can
be extended to the case of imperative and control features such as those
considered by Matthias, Mitch Wand, and the Indiana school in connection with
Scheme.
Bob Harper
LFCS, Edinburgh
(soon to be CMU-CS).