Python from Wise Guy's Viewpoint

[Pascal Costanza]

Matthias Blume wrote:
> Pascal Costanza <costanza at web.de> writes:
> 
> 
>>>There are also programs which I cannot express at all in a purely
>>
>>>dynamically typed language.  (By "program" I mean not only the executable
>>>code itself but also the things that I know about this code.)
>>>Those are the programs which are protected against certain bad things
>>>from happening without having to do dynamic tests to that effect
>>>themselves.
>>
>>This is a circular argument. You are already suggesting the solution
>>in your problem description.
> 
> 
> Is it?  Am I?  Is it too much to ask to know that the invariants that
> my code relies on will, in fact, hold when it gets to execute?

Yes, because the need might arise to change the invariants at runtime, 
and you might not want to stop the program and restart it in order just 
to change it.

> Actually, if you think that this problem description already contains
> the solution which is static typing, then we are basically on the same
> page here.
> 
> 
>>...and BTW, please let me keep up using dynamically typed languages,
>>because this works well for me!
> 
> 
> Since I have no power over what you do, I am forced to grant you this
> wish.  (Lucky you!)

:-)

>>See the example of downcasts in Java.
> 
> 
> You had to dig out the poorest example you could think of, didn't you?
> Make a note of it: When I talk about the power of static typing, I am
> *not* thinking of Java!

OK, sorry, this was my mistake. I have picked this example because it 
has been mentioned in another branch of this thread.

>>>To make a (not so far-fetched, btw :) analogy: Consider logical
>>>statements and formal proofs. Making a logical statement is easy and
>>>can be very short.  It is also easy to make mistakes without noticing;
>>>after all saying something that is false while still believing it to
>>>be true is extremely easy.  Just by looking at the statement it is
>>>also often hard to tell whether the statement is right.  In fact,
>>>computers have a hard time with this task, too.  Theorem-proving is
>>>hard.
>>>On the other hand, writing down the statement with a formal proof is
>>>impossible to get wrong without anyone noticing because checking the
>>>proof for validity is trivial compared to coming up with it in the
>>>first place.  So even though writing the statement with a proof seems
>>>harder, once you have done it and it passes the proof checker you can
>>>rest assured that you got it right.  The longer "program" will have fewer
>>>"bugs" on average.
>>
>>Yes, but then you have a proof that is tailored to the statement you
>>have made. The claim of people who favor static type systems is that
>>static type systems are _generally_ helpful.
> 
> 
> I am not sure you "got" it: Yes, the proof is tailored to the
> statement (how else could it be?!), but the axioms and rules of its
> underlying proof system are not.  Just like not every program has the
> same type even though the type system is fixed.

Yes, but you have much more freedom when you write an arbitrary proof 
than when you need to make a type system happy.


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)