Python from Wise Guy's Viewpoint

[Matthew Danish]

On Mon, Oct 27, 2003 at 10:08:15PM +0100, Joachim Durchholz wrote:
> Matthew Danish wrote:
> 
> >On Mon, Oct 27, 2003 at 07:00:01PM +0100, Andreas Rossberg wrote:
> >
> >>Pascal Costanza wrote:
> >>
> >>>Can you show me an example of a program that does't make sense anymore 
> >>>when you strip off the static type information?
> >>
> >>Here is a very trivial example, in SML:
> >>
> >>	20 * 30
> >>
> >>Multiplication, as well as literals, are overloaded. Depending on 
> >>whether you type this expression as Int8.int (8-bit integers) or 
> >>IntInf.int (infinite precision integer) the result is either 600 or an 
> >>overflow exception.
> >
> >May I point out that the correct answer is 600, not overflow?
> 
> No, the correct answer isn't 600 in all cases.
> If it's infinite-precision arithmetic, the correct answer is indeed 600.
> If it's 8-bit arithmetic with overflow, there is no correct answer.
> If it's 8-bit arithmetic with wrap-around, the correct answer is 88.
> If it's 8-bit arithmetic with saturation, the correct answer is 255.
> (The result happens to be independent of whether the arithmetic is 
> signed or unsigned.)

What is this stuff?  I am talking about integers here!  You know, the
infinite set with the same cardinality as natural numbers.  Why can't
the implementation figure out how to represent them most efficiently?

> Using infinite-precision internally for all calculations isn't always 
> practicable, and in some algorithms, this will give you even wrong 
> results (e.g. when multiplying or dividing using negative numbers, or 
> with saturating arithmetic).

If it gives you the wrong results, I'm not interested.  How hard is it
to get the arithmetically correct result of 20 * 30?  Surely 20 * -30 is
not that difficult either.  It is a pet peeve I have with many
programming languages, especially the ones that are so big on proofs and
correctness.

Arithmetic as it exists in ML is a good example of the difference
between correctness and type-safety.  It is also a good example of the
difference between correctness and proof.

Of course, you may claim, that the definition of div, or / or whatever
it is called, is "correct" in that it conforms to the specification.
All that says to me is that the specification is wrong.  Garbage can be
proven, in some system.  Doesn't mean I'm interested.

> Of course, this doesn't say much about the distinction between static 
> and dynamic typing, actually the issues and unlucky fringe cases seem 
> very similar to me. (In particular, overloading and type inference don't 
> tell us whether the multiplication should be done in 8-bit, 16-bit, 
> machine-precision, infinite-precision, wrap-around, or saturated 
> arithmetic, and run-time types don't give us any useful answer either.)

Lisp gets exact rational arithmetic right, why don't ML or Haskell?
Clever compilers like CMUCL can even emit efficient code when it can
figure out the specific types.  Surely a statically typed language would
find this even easier!

-- 
; Matthew Danish <mdanish at andrew.cmu.edu>
; OpenPGP public key: C24B6010 on keyring.debian.org
; Signed or encrypted mail welcome.
; "There is no dark side of the moon really; matter of fact, it's all dark."