Python from Wise Guy's Viewpoint

[Pascal Costanza]

Dirk Thierbach wrote:
> Pascal Costanza <costanza at web.de> wrote:
> 
>>Dirk Thierbach wrote:
> 
> 
>>>Maybe. It sure would help if you'd tell me your view instead of having
>>>me guess :-) For me, a type is a certain class of values, and a static
>>>type is given by a limited language describing such classes. A
>>>dynamic type is a tag that is associated with a value. Arbitrary
>>>classes of values (like "all reals less than 200") are not a type.
>>
>>What are "non-arbitrary classes of values"?
> 
> Those that can be described by the language available for static types
> e.g. in Haskell or OCaml.

This sounds like a circular definiton.

>>According to your criteria, (real * 200) is
>>- a certain class of values
>>- given in a limited language describing that class
> 
> Yes, but you will have a hard time developing a static type checker
> that will work with such a language.

I am not asking for a definition of the term "static type", but for a 
definition of the term "type".

>>I would be interesting to see a convincing definition of the term "type" 
>>that precludes (real * 200), and similar type specifications.
> 
> Look at the definition for type in Haskell or OCaml, for example.

Haskell: "An expression evaluates to a value and has a static type." 
(http://www.haskell.org/onlinereport/intro.html#sect1.3 )

Where is the definiton for "type"? (without "static"?)

I haven't found a definiton in http://caml.inria.fr/ocaml/htmlman/index.html

>>(Maybe it helps to explain that CHECK-TYPE doesn't check a value per se. 
>>(check-type 5 (real * 200)) doesn't work. CHECK-TYPE checks a property 
>>of the variable it is being passed.)
> 
> Yes, I know. What does that explain?

Let's first get our terminology right.

>>The only claim I make is that static type systems need to reject 
>>well-behaved programs. That's an objective truth.
> 
> This depends on the definition of "well-behaved". The claim I make is
> that for a suitable definition of "well-behaved", it is not an
> objective truth. And even if you stick to your definition of
> "well-behaved", it doesn't really matter in practice.

"well-behaved" means "doesn't show malformed behavior at runtime", i.e. 
especially "doesn't core dump".

"Behavior" is a term that describes dynamic processes. I am only 
interested in dynamic behavior here.

I don't mind if you want to change that terminology. Let's just rephrase 
it: Static type systems need to reject programs that wouldn't 
necessarily fail in serious ways at runtime.

>>All I hear is that you (and many others) say that the disadvantages
>>of static typing are negligible. However, I haven't found any
>>convincing arguments for that claim.
> 
> What kind of arguments would you like to have? I have tried to
> show with a few examples that even programs that you think should
> be rejected with static typing will be accepted (if you allow for
> the fact that they are written in a different language).

Yes, for some of them.

>>But I am interested in the question why you (or others) think that 
>>almost all software should be developed like that. 
> 
> I didn't say that. Please do not put up a strawman. In fact, I 
> explicitely said "you use whatever tool you like best".

But that was the original question that initiated this thread. If we 
have an agreement here, that's perfect!

>>I have chosen to illustrate examples in which a dynamic approach might 
>>be considerably better. 
> 
> And you didn't convince me; all your examples can be statically
> typed.

What about the example in 
http://groups.google.com/groups?selm=bnf688%24esd%241%40newsreader2.netcologne.de 
?

I don't think this can be done without a serious rewrite.

>>Again, to make this absolutely clear, it is my personal experience
>>that dynamic type checking is in many situations superior to static
>>type checking.
> 
> That's maybe the important point. HOW DO YOU KNOW IF YOU HAVE NEVER
> TRIED IT? (In a language with good static typing, not in a language
> with lousy static typing). And obviously you haven't tried it,
> otherwise you wouldn't give examples that can be easily statically
> typed, or confuse exceptions or dynamic checks with static type checks.
> So it cannot come from your personal experience.

Right, it comes from a more principled consideration: You can't have 
metacircularity in a statically type language. You might be able to have 
metacircularity if you strictly separate the stages, but as soon as you 
want to be able to at least occasionally call base code from meta code 
and vice versa, then you lose.

Metacircularity gives me the guaranntee that I can always code around 
any unforeseeable limitations that might come up, without having to 
start from scratch.

So, yes, I am interested in having the opportunity to change invariants 
during the runtime of a program. This might sound self-contradictory, 
but in practice it isn't. Remember, "One man's constant is another man's 
variable." (see http://www-2.cs.cmu.edu/afs/cs.cmu.edu/Web/csd/perlis.html )

>>But I don't ask anyone to unconditionally use dynamically typed
>>languages.
> 
> But you insist that dynamically typed languages are "better" or
> "superior to" statically typed, because you claim you cannot do things
> in a statically typed language that you can do in a dynamically typed
> one. That's the point where I disagree. I don't ask you to use a
> statically typed language, I just want you to give admit that both
> are equally good in this respect, or at least you should sit down and
> verify that yourself before saying it.

I haven't said that I can do more things in a dynamically typed 
language. I have said that statically typed languages need to reject 
well-behaved programs. That's a different claim. We are not talking 
about Turing equivalence.

If a base program calls its meta program and changes types, you can't 
type check such a program by definition.

For example:

(defun check (x)
   (integerp x))

(defun example-1 ()
   (let ((x 5))
     (assert (check x))
     (print 'succeeded)
     (eval '(defun check (x)
              (stringp x)))))

Now, this might seem nonsensical, but consider this:

(defun example-2 ()
   (eval '(defun check (x)
            (realp x)))
   (example-1))



Pascal

-- 
Pascal Costanza               University of Bonn
mailto:costanza at web.de        Institute of Computer Science III
http://www.pascalcostanza.de  Römerstr. 164, D-53117 Bonn (Germany)