[Prev][Next][Index][Thread]
Re: type safety
> Right: if the original program looked like this:
>
> (lambda (n : Integer)
> (/ 1 n))
>
> yours will be
>
> (lambda (n : Integer-Abstract-Type)
> (if (instanceof n Zero)
> (error 'division-by-zero)
> (/ 1 (cast-to-NZInteger n))))
>
> or something like this. And how is your type system going to prove to me
> that (error 'division-by-zero) is never going to be called?
It isn't. But your claim was that Milner's claim was
incorrect. He claimed that the type system could ensure that
programmes do not "crash" (I don't remember the precise term
used). Your example was that it couldn't prevent division by
zero, but my example counters that: in a language with this
restriction on the type of (/), (/) never gets zero as a
second argument. Perhaps the number of errors in the
programme remains the same, but their _kind_ is different.
> By pushing
> tests and error/exception signals into programs, you don't get any more
> program safety than we had.
Perhaps not, but we were talking about the definition of
type safety.
As I mentioned in my first message, this approach is
probably (almost certainly) impractical.
* * *
I'll add (apropos your later message) that we differ on the
meaning of type. My appreciation of the term is closer to
that mentioned elsewhere in the thread (apologies to whoever
mentioned it, but I deleted that message) of Reynolds:
typing is static information that helps the compiler (or
read phase of the interpreter, if you prefer) reject a class
of programmes (before executing them) so that certain
classes of error never occur.
I don't have a word for what you mean by typing, and I think
it would save a whole lot of futile arguments if the terms
'static type' and 'dynamic type' didn't both include the
word type.
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)
Follow-Ups:
References: