optional types, predicate types

[Matthias Felleisen <address@hidden>]

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
 program runs. 

 [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
 this case.]

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. 




-- Matthias