[Prev][Next][Index][Thread]

RE: type safety


Greg,

>> ... For "partial" primitive
>> operations like division, you can define the domain of the operation
>> as a type in a suffciently expressive type system.  In fact, the same
>> "trick" can be used to eliminate array bounds checking by introducing
>> subrange types as in Pascal.  But what have you gained?  The
>> programmer must now insert an explicit case check for nearly every
>> application of the primitive operation (e.g., array access) and throw
>> an exception when the check fails.  

>This is only true in very simple systems.  Xi and Pfenning's
>proposal for DML provides enough support that the check can
>be moved to the caller instead of the callee -- hence the
>requirement becomes part of the (documented) interface, 
>no runtime test is necessary in simple cases, and we have
>a way to communicate invariants.  A similar approach is used
>in TALx86 and Touchstone.  I expect to see nice treatments
>of array bounds checks folded into next generation languages.

Either Xi and Pfenning only handle trivial cases or their type system
must set a new record for complexity.  A sophisticated approach to
eliminating array bounds checks involves solving integer linear
programming problems.  Are you stating that all type systems
that do not incorporate integer programming solvers are "very simple"?

On a more serious note, what you are proposing is to replace
conventional static type systems generated by simple syntactic rules
with much more complex static analyses akin to what Matthias and I
call "soft type systems".  We developed soft type systems to support
"static debugging", which is really a restricted form of program
verification.  What I fail to see is why these analyses (which can be
very expensive computationally) should be incorporated in the language
syntax.  

You could easily take one of the soft typers Matthias and I have built
for Scheme and adopt it as a type system.  The programmer would write
a conventional Scheme program, run it through the soft typer to find
which run-time checks (as performed by a conventional "dynamically
typed" version of Scheme) are not provably unnecessary, and insert
explicit casts at these sites.  For that matter, you could add an
option to the soft typer that would automatically produce a
"corrected" source program including the requisite casts.  But what is
the point in making such a complex analysis part of the language syntax?

Keep the language definition simple and embed the complexity in
the verification tools used to analyze the language.

-- Corky