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

Re: type safety

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



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