Python from Wise Guy's Viewpoint

M

Matthias Blume

Pascal Costanza said:
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?
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!
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.

Matthias
 
M

Matthias Blume

Pascal Costanza said:
Well, to say this once more, there are programs out there that have a
consistent design, that don't have "problems", and that cannot be
statically checked.

Care to give an example? How you you know that the design is
consistent? Do you have a proof for that claim? Can you write that
proof down for me, please?

:)

Matthias
 
P

Pascal Costanza

Matthias said:
Safe and unsafe.

BTW, C is typed, Smalltalk is untyped. C's type system just happens
to be unsound (in the sense that, as you observed, well-typed programs
can still be unsafe).

Can you give me a reference to a paper, or some other literature, that
defines the terminology that you use?

I have tried to find a consistent set of terms for this topic, and have
only found the paper "Type Systems" by Luca Cardelli
(http://www.luca.demon.co.uk/Bibliography.htm#Type systems )

He uses the terms of static vs. dynamic typing and strong vs. weak
typing, and these are described as orthogonal classifications. I find
this terminology very clear, consistent and useful. But I am open to a
different terminology.

Pascal
 
P

Pascal Costanza

Remi said:
It make the verification when you call the test. I explain :

you could define :

let f x = x #foo

which is a function taking an object x and calling its method
foo, even if there is no class having such a method.

When sometime latter you do a :

f bar

then, and only then the compiler verify that the bar object have a foo
method.

Doesn't this mean that the occurence of such compile-time errors is only
delayed, in the sense that when the test suite grows the compiler starts
to issue type errors?

Anyway, that's an interesting case that I haven't known about before.
Thanks.


Pascal
 
K

Ken Rose

Pascal said:
Writing programs that inspect and change themselves at runtime.

Ah. I used to do that in assembler. I always felt like I was aiming a
shotgun between my toes.

When did self-modifying code get rehabilitated?

- ken
 
E

Erann Gat

Let me put it like this. Say I have a statically, expressively, strongly
typed language L. And I have another language L' that is identical to
L except it lacks the type system. Now, any program in L that has the
type declarations removed is also a program in L'. The difference is
that a program P rejected by the compiler for L can be converted to a
program P' in L' which *may even appear to run fine for most cases*.
However, and this is the really important point, P' is *still* a
*broken* program. Simply ignoring the type problems does not make
them go away: P' still contains all the bugs that program P did.

No. The fallacy in this reasoning is that you assume that "type error"
and "bug" are the same thing. They are not. Some bugs are not type
errors, and some type errors are not bugs. In the latter circumstance
simply ignoring them can be exactly the right thing to do.

(On the other hand, many, perhaps most, type errors are bugs, and so
having a type system provide warnings can be a very useful thing IMO.)

E.
 
S

Simon Helsen

It make the verification when you call the test. I explain :

you could define :

let f x = x #foo

which is a function taking an object x and calling its method
foo, even if there is no class having such a method.

When sometime latter you do a :

f bar

then, and only then the compiler verify that the bar object have a foo
method.

you might want to mention that this is possible because of 'extensible
record types'. Well, there is a good chance the pyhton/lisp community will
not understand this, but it illustrates that a lot of the arguments
(probably on both sides in fact) are based on ignorance.

One more thing I remembered from a heavy cross-group fight between
comp.lang.smalltalk and c.l.f. quite a while ago, is that so-called
'dynamically typed' languages are useful because they allow you to
incrementally develop ill-typed programs into better-typed programs (the
XP-way), where the ill-typed programs already (partially) work. OTOH, with
a static type system, you have to think more in advance to get the types
right. XP-people consider this a hindrance and that is what people mean
with 'the type system getting the way'. With a Haskell-style or even
Ocaml-style type system, you cannot seriously argue that you can write a
program which cannot be easily(!) converted into one that fits such type
systems. By program, I mean 'a finished production-reade piece of
software', not a 'snapshot' in the development cycle.

The arguments from the smalltalk people are arguably defendable and this
is why this kind of discussion will pop up again and again. Using either
static or dynamic (Blume: untyped) type systems is not the point at all.
What actually matters is your development style/phylosophy and this is
more an issue of software engineering really.

Ok, I am phasing out again.

Regards,

Simon
 
P

Pascal Costanza

Matthias said:
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.




Since I have no power over what you do, I am forced to grant you this
wish. (Lucky you!)
:)



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

Pascal Costanza

Matthias said:
Care to give an example? How you you know that the design is
consistent?

Squeak, probably. Lisp development environments. Probably almost any
development environment with a good debugger that allows for changing
code on the fly.
Do you have a proof for that claim? Can you write that
proof down for me, please?

No. Design consistency is an aesthetical category.

Pascal
 
P

Pascal Costanza

Ken said:
Ah. I used to do that in assembler. I always felt like I was aiming a
shotgun between my toes.

When did self-modifying code get rehabilitated?

I think this was in the late 70's.


Pascal
 
P

Pascal Costanza

Simon said:
you might want to mention that this is possible because of 'extensible
record types'. Well, there is a good chance the pyhton/lisp community will
not understand this, but it illustrates that a lot of the arguments
(probably on both sides in fact) are based on ignorance.

Do you have a reference for extensible record types. Google comes up,
among other things, with Modula-3, and I am pretty sure that's not what
you mean.
One more thing I remembered from a heavy cross-group fight between
comp.lang.smalltalk and c.l.f. quite a while ago, is that so-called
'dynamically typed' languages are useful because they allow you to
incrementally develop ill-typed programs into better-typed programs (the
XP-way), where the ill-typed programs already (partially) work.

Sometimes the ill-typed program is all I need because it helps me to
solve a problem that is covered by that program nonetheless.
OTOH, with
a static type system, you have to think more in advance to get the types
right. XP-people consider this a hindrance and that is what people mean
with 'the type system getting the way'. With a Haskell-style or even
Ocaml-style type system, you cannot seriously argue that you can write a
program which cannot be easily(!) converted into one that fits such type
systems. By program, I mean 'a finished production-reade piece of
software', not a 'snapshot' in the development cycle.

The arguments from the smalltalk people are arguably defendable and this
is why this kind of discussion will pop up again and again. Using either
static or dynamic (Blume: untyped) type systems is not the point at all.
What actually matters is your development style/phylosophy and this is
more an issue of software engineering really.

Exactly. Very well put!

Thanks,
Pascal
 
A

Andreas Rossberg

Pascal said:
I don't care about that difference. My development environment is
flexible enough to make execution of test suites a breeze. I don't need
a separate compilation and linking stage to make this work.


Don't let your production code run with assertion checking off then.

You don't seem to see the fundamental difference, which has been stated
as "Static typing shows the absence of [certain classes of] errors,
while testing [with assertions] can only show the presence of errors."
When you actively use a type system as a tool and turn it to your
advantage that "certain class" can be pretty large, btw.
I hear that in the worst case scenarios, static type checking in modern
type systems needs exponential time, but for most practical cases this
doesn't matter. Maybe it also doesn't matter for most practical cases
that you can't check all permutations of data in a test suite.

Come on, you're comparing apples and wieners. The implications are
completely different.

--
Andreas Rossberg, (e-mail address removed)-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc.
 
A

Andreas Rossberg

Pascal said:
Can you give me a reference to a paper, or some other literature, that
defines the terminology that you use?

I have tried to find a consistent set of terms for this topic, and have
only found the paper "Type Systems" by Luca Cardelli
(http://www.luca.demon.co.uk/Bibliography.htm#Type systems )

He uses the terms of static vs. dynamic typing and strong vs. weak
typing, and these are described as orthogonal classifications. I find
this terminology very clear, consistent and useful. But I am open to a
different terminology.

My copy,

http://research.microsoft.com/Users/luca/Papers/TypeSystems.A4.pdf

on page 3 defines safety as orthogonal to typing in the way Matthias
suggested.

--
Andreas Rossberg, (e-mail address removed)-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc.
 
A

Andreas Rossberg

Pascal said:
Yes, but it says dynamically typed vs statically typed where Matthias
says untyped vs typed.

Huh? On page 2 Cardelli defines typed vs. untyped. Table 1 on page 5
clearly identifies Lisp as an untyped (but safe) language. He also
speaks of statical vs. dynamical _checking_ wrt safety, but where do you
find a definition of dynamic typing?

- Andreas

--
Andreas Rossberg, (e-mail address removed)-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc.
 
P

Pascal Bourguignon

Matthias Blume said:
A 100,000 line program in an untyped language is useless to me if I am
trying to make modifications -- unless it is written in a highly
stylized way which is extensively documented (and which usually means
that you could have captured this style in static types).

The only untyped languages I know are assemblers. (ISTR that even
intercal can't be labelled "untyped" per se).

Are we speaking about assembler here?
 
M

Matthias Blume

Pascal Bourguignon said:
The only untyped languages I know are assemblers. (ISTR that even
intercal can't be labelled "untyped" per se).

Are we speaking about assembler here?

No, we are speaking different definitions of "typed" and "untyped"
here. Even assembler is typed if you look at it the right way.

As I said before, I mean "untyped" as in "The Untyped Lambda
Calculus" which is a well-established term.

Matthias
 
A

Andrew Dalke

Joachim Durchholz
Not quite - that was a loss of 500 million dollars. I don't know what
the software development costs were, so I'm just guessing here, but I
think it's relatively safe to assume a doubly redundant system would
already have paid off if it had caught the problem.

Since the Mars rover mission a few years ago cost only about $250million,
I'm going to assume that you included payload cost. Here's some
relevant references I found [after sig], which suggests a price per rocket
of well under $100 million and the cost of the "four uninsured scientific
satellites" made it be about $500 million.

It used to be that rockets needed a lot of real-world tests before
people would stick expensive payloads on them. For a while, dead
weight was used, but people like amateur hams got permission to
put "cheap" satellites in its place, and as the reliability increased,
more and more people were willing to take chances with unproven
rockets.

So there's an interesting tradeoff here between time spent on live
testing and the chance it will blow up. Suppose Ariane decided
to launch with just bricks as a payload. Then they would have
been out ~$75 million. But suppose they could convince someone
to take a 10% chance of failure to launch a $100 million satellite
for half price, at $40 million. Statistically speaking, that's a good
deal. As long as it really is a 10% chance.

(The satellites were uninsured, which suggests that this was
indeed the case.)

However, it seems that 4 of the first 14 missions failed, making
about a 30% failure rate. It also doesn't appear that all of those
were caused by software failures; the 4th was in a "cooling
circuit."
The point is that no amount of software technology would have caught the
problem if the specifications are wrong.

I agree.

Andrew
(e-mail address removed)


http://www.namibian.com.na/2002/june/techtalk/02651A180A.html
] The Ariane 44L rocket equipped with four liquid strap-on boosters --
] the most powerful in the Ariane-4 series --
...
] Specialists estimated the cost of the satellite, launch and insurance at
] more than $250 million.


http://www.cnn.com/2000/TECH/space/12/20/rocket.ariane.reut/
] Western Europe's new generation Ariane-5 rocket has placed three
] satellites into space
...
] Experts have estimated the cost of the [ASTRA 2D] satellite,
] launch and insurance at over $85 million
...
] The estimated cost of the GE-8 satellite, launch and insurance is
] over $125 million.

] But Ariane-5's career began with a spectacular failure during its
] maiden test launch in June 1996, exploding 37 seconds after
] lift-off and sending four uninsured scientific satellites worth $500
] million plunging into mangrove swamps on French Guiana's coast.

http://www.centennialofflight.gov/essay/SPACEFLIGHT/ariane/SP42.htm
] After Arianespace engineers rewrote the rocket's control software,
] the second Ariane-5 launch successfully took place on October 30,
] 1997. More launches followed and the rocket soon entered full commercial
] service, although it suffered another failure on its tenth launch in July
2001.
] Ariane-5 joined the Russian Proton, American Titan IV and Japanese
] H-IIA as the most powerful rockets in service. Ariane-5 initially had a
very
] high vehicle cost, but Arianespace mounted an aggressive campaign to
] significantly reduce this cost and make the rocket more cost-effective.
The
] company also planned further upgrades to the Ariane-5 to enable it to
remain
] competitive against a growing number of competitors.

http://www.chron.com/cgi-bin/auth/story.mpl/content/interactive/space/news/9
9/990824.html
] Each launch of Japan's flagship H-2 rocket to place a satellite into
] geostationary orbit costs close to 19 billion yen, about double the cost
] of competitors such as the European Space Agency's Ariane rocket.
(19 billion yen ~ $190 million => ~$100million for geostationary orbit on
Ariane)

] Part of the six-billion European-Currency-Unit ($6.28 billion U.S.) cost
of
] the Ariane 5 project went toward construction of new facilities at ESA's
Kourou,
] French Guiana launch complex

http://www.rte.ie/news/2002/1212/satellite.html
] It is the fourth failure of an Ariane-5 in its 14-mission history, and is
] being seen as a major setback for the European space programme.
See also
http://www.dw-world.de/english/0,3367,1446_A_713425,00.html
] the problem occurred in the cooling circuit of one of the rocket's main
] engines. A change in engine speed around 180 seconds after take-off
] caused the launcher to "demonstrate erratic behaviour".
 

Ask a Question

Want to reply to this thread or ask your own question?

You'll need to choose a username for the site, which only take a couple of moments. After that, you can post your question and our members will help you out.

Ask a Question

Members online

Forum statistics

Threads
474,173
Messages
2,570,937
Members
47,481
Latest member
ElviraDoug

Latest Threads

Top