Re: type safety
Subject: Re: type safety
From: Jon Fairbairn <Jon.Fairbairn@cl.cam.ac.uk>
Date: Wed, 29 Dec 1999 20:45:14 +0000
In-reply-to: Your message of "Wed, 29 Dec 1999 10:12:24 CST." <199912291950.OAA06972@localhost.localdomain>
While I agree with most of what you say, I don't follow
your argument 4:
> 4. Types can never prove that all safety restrictions will be respected.
I don't beleive this to be true; For most type systems you
cannot guard against non-termination, but I don't think
anyone has ever claimed otherwise. For type-theory based
languages, even that can be avoided.
> Take LC + numbers plus division. [...]
> * division, which may only consume numbers in both positions [B]
> and which may not consume a 0 in the second position [C]
> Your standard simple type system can eliminate the restrictions labeled
> A and B, but not C.
I aver that the standard simple type system _can_ eliminate
[C], although most language designs don't do this -- this
is a failure of will on the part of programming language
designers, not the type system
> So, a program in this language may still signal an
> error: attempt to divide by 0. Call this an exception or whatever you
> will, it is a behavior that you don't want.
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.
Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk
18 Kimberley Road email@example.com
Cambridge CB4 1HH +44 1223 570179 (pm only, please)