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

Re: type safety


>Even with a limited type system, you can make Integer an 
>abstract type uniting NZInteger and Zero

>divide then gets the type Integer -> NZInteger -> Integer.
>Of course, this requires the programme to be peppered with
>tests, and that's why language designers don't do it, but
>your argument seems to be about what a type system _can_ do,
>not what people _do_ do.

This claim is extremely misleading.  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.  Moreover, the programmer must
continually apply appropriate injection operations to convert values
of the component types (e.g., NZInteger) back to the aggregate type
(e.g., Integer).  Aborting errors have been conveniently moved outside
the type system, but they have not gone away.  Type checking does not
exclude the possibility of run-time failures any more effectively than
before--except for the few primitive applications where the type
system assures that no case check is required.

If this approach is such a good idea, then why does't ML follow it in
conjunction with lists (empty vs. non-empty) where it is less clumsy
than it is for integers?  You can easily define your own list type in
ML so that none of the usual primitive operations (including first and
rest) are partial.  Try rewriting a non-trivial ML application
involving lists in this way and you will see why no language designer
has gone down this road.  Explicit case checking for domain errors
imposes a huge clerical burden on the programmer and obfuscates code.

The domain checking approach that you advocate becomes even less
tenable when it is applied to non-primitive operations that impose
complex invariants on their inputs.  What about an operation that
requires an argument that is a prime number?  Or the abstract syntax
for a type correct ML program?  These domains cannot be defined by
simple tree grammars.  A syntactic type system that accommodates them
will be truly unwieldy.

-- Corky Cartwright
Follow-Ups: