[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
optional types, predicate types
Academics have dealt with both optional types and predicate types for much
longer than the conversation on this list indicates.
Optional types: ML is a statically typed language that allows you to omit
all type declarations. The PE (front end) restores the types for most ML
compilers and produces an explicitly typed intermediate language. Take a
look at the efforts that have gone on in this area, starting with Milner's
original papers, Leroy's first paper on using typed intermediate forms for
parameteric polymorphism (POPL 91 or 92), and the whole series of TIC
workshops. Most papers show how to use the types that the front end
restores in the compilation process.
Don't forget to read the papers by Boehm (yes, the one who wrote the GC)
on when type reconstruction is impossible in these cases. Indeed, there
are a whole series of such papers. With optional types you don't
necessarily get all the types back.
And then don't forget to think what these types mean. Unless you want them
to mean what they mean in C. Nothing but the number of bits you allocate.
Predicate types: As ML shows, optional types are not necessarily associated
with predicate types. In contrast to partition types as in ML, predicate
types are descriptions of sets of values that actually flow when the
[Note: Type theoretician object to the use of the word type for such
things, and in a way they are correct. We should use some other word for
MIT's Mike Ernst didn't invent predicate types. (Sorry, Greg, if I am
bursting a bubble here :). Predicate have a history going back to the
60s. There is a pretty solid Vaughn Pratt paper (who may have been at MIT
at the time) on this stuff. POPL in the 70's.
If you want to take a look at a static debugger based on predicate type
reconstruction, read PLT's papers on soft types. We studied this thing
starting with Fagan, followed by Wright, Flanagan, and Meunier
now. Meunier's screen dump give you an idea of how powerful the debugger
is and how graphical it is. Also see Flanagan's screen dumps. Warning: PLT
Scheme will no longer support MrSpidey as of v200; we will publish its
successor when it's ready.
(see http://www.ccs.neu.edu/scheme/, follow the links to papers)
For the use of predicate types in compilation, see the papers on Self,
Scheme, and Common Lisp, esp the CMU edition. Note though, that many of
these papers do not pay attention to soundness.