Re: Optional types

[address@hidden (Gregory T. Sullivan)]

>>>>> "Ken" == Ken Anderson <kanderson@bbn.com> writes:

 Ken> So, what if the compiler could take those examples and use them
 Ken> to generate efficient code, the would certainly help type
 Ken> inference.  The resulting code might not be as efficient as
 Ken> having a type declaration language as Dan was talking about (i
 Ken> guess Common Lisp has something like this), but it could be fast
 Ken> and light.

There are reasons that the languages used to express types are much
more restricted than full-blown Turing-complete programming
languages.  The major tension in type system design is finding type
languages that are as expressive as possible (allowing as many correct
programs as possible to be proven type correct) while still being
sound (types correspond to runtime values), decidable (type checking
will terminate), etc.  

If you are aiming for static type correctness (i.e. no "message not
understood" errors at runtime), you clearly need a type language you
can effectively reason about.  One example of expressive but complex
type systems is the Flint project at Yale[1].

Even for dynamically typed languages, where the legality of method
calls is checked at call time, you still want a type language you can
reason about, in order to have any hope of optimizing away a
significant portion of the type checks.

My current favorite is to have a rich set of concrete types (integers,
records, etc.), a simple type algebra (and, or, not, ==) for
constructing more complex types, and a bail out of "predicate
types"[2] that you use when all else fails.  Predicate types give you
the full power of the host programming language when you need it, but
foil analysis.

Two more related comments:

  * The "write your tests before your code" approach of the Extreme
    Programming crowd is a great idea.  It forces you to be precise
    about what you intend to code, and the general purpose programming
    language allows you to specify all the tests not expressible in
    the type language.

  * Writing test _harnesses_ (as opposed to the tests themselves) is
    much easier in a higher order (where methods are first class),
    dynamically typed language such as Smalltalk than a statically
    typed language such as Java (though Java's reflection api helps). 

[1] http://flint.cs.yale.edu/
[2] http://sdg.lcs.mit.edu/~mernst/pubs/gud-ecoop98-abstract.html

-- 
Greg      gregs@ai.mit.edu (617)253-5807
Sullivan  http://www.ai.mit.edu/~gregs/