Re: type safety

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

> 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)

I didn't say that it was practical.

> and throw an exception when the check fails.

Only if there is nothing better to do.

> 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).

I didn't say it was practical.

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

That argument covers the whole of any notion of static typing. One
could always put a type like:

data Untype = I Integer | U (Untype -> Untype) | ...

at the beginning of a programme and then programme in an essentially
untyped manner. That doesn't mean that the static type system is

> 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?

I didn't say it was practical.

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

I have (not in ML, though). It's clumsy, but I wouldn't agree that in
the case of lists it really is impractical -- if you write a
list-processing programme that makes extensive use of fold, map and so
on, occurrences of head are fairly rare, so replacing them with
explicit case-analyses is less of a burden than one might expect.

> The domain checking approach that you advocate 

I wouldn't say that I advocate that approach.  I suppose that having
said "a failure of will on the part of programming language designers"
it might sound that way, but that was merely a rhetorical phrase.

Jón Fairbairn                                 Jon.Fairbairn@cl.cam.ac.uk
18 Kimberley Road                                        jf@cl.cam.ac.uk
Cambridge CB4 1HH                      +44 1223 570179 (pm only, please)