Re: type safety

• To: Jon.Fairbairn@cl.cam.ac.uk
• Subject: Re: type safety
• From: Matthias Felleisen <matthias@cs.rice.edu>
• Date: Wed, 29 Dec 1999 23:59:42 -0600 (CST)
• CC: types@cis.upenn.edu
• In-reply-to: <199912292250.RAA07235@localhost.localdomain> (message from Jon Fairbairn on Wed, 29 Dec 1999 20:45:14 +0000)
• References: <199912292250.RAA07235@localhost.localdomain>
• Reply-to: matthias@rice.edu

[I understand that there are more powerful type theories than ML's and that
 we can built a much richer hierarchy of numeric types.]

Jon writes: 

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

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? By pushing
tests and error/exception signals into programs, you don't get any more
program safety than we had. 

-- Matthias

• Re: type safety
• From: Jon Fairbairn <Jon.Fairbairn@cl.cam.ac.uk>

• Prev: Re: type safety
• Next: Re: type safety
• Index(es):
  • Main
  • Thread