Python from Wise Guy's Viewpoint

[Neelakantan Krishnaswami]

In article <bnjavv$v4c$2 at f1node01.rhrz.uni-bonn.de>, Pascal Costanza wrote:
> Matthias Blume wrote:
>> 
>> Nitpick: Neither syntactic nor statically checked type errors make
>> programs fail. Instead, their presence simply implies the absence of a
>> program.
> 
> Yes, the absence of a program that might not fail if it wouldn't have 
> been rejected by the static type system.

That sentence reflects a misunderstanding of what something like ML's
type system *means*. You're trying to hammer ML into the Lisp mold,
which is leading you to incorrect conclusions.

A value in any programming language is some pattern of bits
interpreted under a type. In Scheme or Lisp, there is a single
universe (a single type) that that all values belong to, which is why
it's legal to pass any value to a function. But in ML, there are
multiple universes of values, one for each type.

This means that the same bit pattern can represent different values,
which is not true in a dynamically typed language. To make this
concrete, consider the following Ocaml code:

  type foo = A | B
  
  type baz = C | D
  
  let f1 x = 
    match x with
    | A -> C    
    | B -> D
  
  let f2 x = 
    match x with
    | C -> 0 
    | D -> 1

Some apparently-similar Scheme code would look like:

  (define (f1 x)
     (case x
       ((A) 0)
       ((B) 1)))

  (define (f2 x)
     (case x
        ((C) 0) 
        ((D) 1)))

The difference between these two programs gets revealed when you look
at the assembly code that the Ocaml compiler produces for f1 and f2,
side by side[*]:

f1:                             f2:                      
.L101:                          .L103:                   
        cmpl    $1, %eax                cmpl    $1, %eax 
        je      .L100                   je      .L102    
        movl    $3, %eax                movl    $3, %eax 
        ret                             ret              
.L100:                          .L102:                   
        movl    $1, %eax                movl    $1, %eax 
        ret                             ret              

The code generated for each function is identical, modulo label names.
This means that the bit patterns for the data constructors A/C and B/D
are identical, and the the program only makes sense because A and C,
and B and D are interpreted at different types. (In fact, notice that
the bit-representation of the integer zero and and the constructors A
and C are the same, too.) In contrast, this would not be a valid
compilation of the Scheme program, because A, B, C, and D would all
have to have distinct bit patterns.

So eliminating the types from an ML program means you no longer have a
program, because you can no longer consistently interpret bit patterns
as ML values -- there *isn't* any universal domain that all ML values
really belong to, as you are supposing.

[*] I cleaned up some extraneous alignment stuff, to make what's going
on clearer. But all that was identical too.

-- 
Neel Krishnaswami
neelk at cs.cmu.edu