Python from Wise Guy's Viewpoint

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Matthias Blume wrote:
[color=blue]
> PS: When I say "untyped" I mean it as in "the _untyped_ lambda
> calculus".[/color]

What terms would you use to describe the difference between dynamically
and weakly typed languages, then?

For example, Smalltalk is clearly "more" typed than C is. Describing
both as "untyped" seems a little bit unfair to me.

Pascal

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

[Remi Vanicat]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue]
> Remi Vanicat wrote:[color=green]
>> Pascal Costanza <costanza@web.d e> writes:[/color]
>[color=green][color=darkred]
>>>In a statically typed language, when I write a test case that calls a
>>>specific method, I need to write at least one class that implements at
>>>least that method, otherwise the code won't compile.[/color]
>> Not in ocaml.
>> ocaml is statically typed.[/color]
>
> How does ocaml make sure that you don't get a message-not-understood
> exception at runtime then?[/color]

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.

By the way, It might give you some headache when you have made a
spelling error to a method name (because the error is not seen by the
compiler where it happen, but latter, where the function using the
wrong method is used).



--
Rémi Vanicat

[Matthias Blume]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue]
> Matthias Blume wrote:
>[color=green]
> > PS: When I say "untyped" I mean it as in "the _untyped_ lambda
> > calculus".[/color]
>
> What terms would you use to describe the difference between
> dynamically and weakly typed languages, then?
>
>
> For example, Smalltalk is clearly "more" typed than C is. Describing
> both as "untyped" seems a little bit unfair to me.[/color]

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

Matthias

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Matthias Blume wrote:[color=blue]
> Pascal Costanza <costanza@web.d e> writes:
>
>[color=green]
>>Fergus Henderson wrote:
>>
>>[color=darkred]
>>>In my experience, people who have difficulties in getting their programs
>>>to typecheck usually have an inconsistent design, not a design which is
>>>consistent but which the type checker is too restrictive to support.[/color]
>>
>>Have you made sure that this is not a circular argument?[/color]
>
> Sure. What he says is that the problems with those programs are
> usually still there even after you erase types and, thus, arrive at an
> untyped program.[/color]

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.


Pascal

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

[Matthias Blume]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue][color=green]
> > There are also programs which I cannot express at all in a purely[/color]
>[color=green]
> > 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.[/color]
>
> This is a circular argument. You are already suggesting the solution
> in your problem description.[/color]

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.
[color=blue]
> ...and BTW, please let me keep up using dynamically typed languages,
> because this works well for me![/color]

Since I have no power over what you do, I am forced to grant you this
wish. (Lucky you!)
[color=blue]
> See the example of downcasts in Java.[/color]

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!
[color=blue][color=green]
> > 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.[/color]
>
> 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.[/color]

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

[Matthias Blume]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue]
> 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.[/color]

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

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Matthias Blume wrote:[color=blue]
> Pascal Costanza <costanza@web.d e> writes:
>
>[color=green]
>>Matthias Blume wrote:
>>
>>[color=darkred]
>>>PS: When I say "untyped" I mean it as in "the _untyped_ lambda
>>>calculus".[/color]
>>
>>What terms would you use to describe the difference between
>>dynamically and weakly typed languages, then?
>>
>>
>>For example, Smalltalk is clearly "more" typed than C is. Describing
>>both as "untyped" seems a little bit unfair to me.[/color]
>
>
> 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).[/color]

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

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

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Remi Vanicat wrote:[color=blue]
> Pascal Costanza <costanza@web.d e> writes:
>
>[color=green]
>>Remi Vanicat wrote:
>>[color=darkred]
>>>Pascal Costanza <costanza@web.d e> writes:[/color]
>>[color=darkred]
>>>>In a statically typed language, when I write a test case that calls a
>>>>specific method, I need to write at least one class that implements at
>>>>least that method, otherwise the code won't compile.
>>>
>>>Not in ocaml.
>>>ocaml is statically typed.[/color]
>>
>>How does ocaml make sure that you don't get a message-not-understood
>>exception at runtime then?[/color]
>
>
> 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.[/color]

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

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

[Ken Rose]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza wrote:[color=blue]
> Joachim Durchholz wrote:
>[color=green]
>> Pascal Costanza wrote:
>>[color=darkred]
>>> For example, static type systems are incompatible with dynamic
>>> metaprogramming . This is objectively a reduction of expressive power,
>>> because programs that don't allow for dynamic metaprogramming can't
>>> be extended in certain ways at runtime, by definition.[/color]
>>
>>
>> What is dynamic metaprogramming ?[/color]
>
>
> Writing programs that inspect and change themselves at runtime.[/color]

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

[Simon Helsen]

Re: Python from Wise Guy's Viewpoint

On Thu, 23 Oct 2003, Remi Vanicat wrote:
[color=blue][color=green]
>> How does ocaml make sure that you don't get a message-not-understood
>> exception at runtime then?[/color]
>
>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.[/color]

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.small talk 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

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Matthias Blume wrote:[color=blue]
> Pascal Costanza <costanza@web.d e> writes:
>
>[color=green][color=darkred]
>>>There are also programs which I cannot express at all in a purely[/color]
>>[color=darkred]
>>>dynamicall y 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 .[/color]
>>
>>This is a circular argument. You are already suggesting the solution
>>in your problem description.[/color]
>
>
> 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?[/color]

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.
[color=blue]
> 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.
>
>[color=green]
>>...and BTW, please let me keep up using dynamically typed languages,
>>because this works well for me![/color]
>
>
> Since I have no power over what you do, I am forced to grant you this
> wish. (Lucky you!)[/color]

:-)
[color=blue][color=green]
>>See the example of downcasts in Java.[/color]
>
>
> 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![/color]

OK, sorry, this was my mistake. I have picked this example because it
has been mentioned in another branch of this thread.
[color=blue][color=green][color=darkred]
>>>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.[/color]
>>
>>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.[/color]
>
>
> 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.[/color]

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 @web.de Institute of Computer Science III
http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Matthias Blume wrote:[color=blue]
> Pascal Costanza <costanza@web.d e> writes:
>
>[color=green]
>>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.[/color]
>
>
> Care to give an example? How you you know that the design is
> consistent?[/color]

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

No. Design consistency is an aesthetical category.
[color=blue]
> :-)
>
> Matthias[/color]

Pascal

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

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Ken Rose wrote:[color=blue]
> Pascal Costanza wrote:
>[color=green]
>> Joachim Durchholz wrote:
>>[color=darkred]
>>> Pascal Costanza wrote:
>>>
>>>> For example, static type systems are incompatible with dynamic
>>>> metaprogramming . This is objectively a reduction of expressive
>>>> power, because programs that don't allow for dynamic metaprogramming
>>>> can't be extended in certain ways at runtime, by definition.
>>>
>>> What is dynamic metaprogramming ?[/color]
>>
>> Writing programs that inspect and change themselves at runtime.[/color]
>
> 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?[/color]

I think this was in the late 70's.


Pascal

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

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Simon Helsen wrote:[color=blue]
> On Thu, 23 Oct 2003, Remi Vanicat wrote:
>
>[color=green][color=darkred]
>>>How does ocaml make sure that you don't get a message-not-understood
>>>exception at runtime then?[/color]
>>
>>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.[/color]
>
>
> 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.[/color]

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.
[color=blue]
> One more thing I remembered from a heavy cross-group fight between
> comp.lang.small talk 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.[/color]

Sometimes the ill-typed program is all I need because it helps me to
solve a problem that is covered by that program nonetheless.
[color=blue]
> 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.[/color]

Exactly. Very well put!

Thanks,
Pascal

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

[Andreas Rossberg]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza wrote:[color=blue][color=green]
>>
>> But only at runtime, where a logic flaw may or may not trigger the
>> assertion.[/color]
>
> 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.
>[color=green]
>> (Assertions are still useful: if they are active, they prove that the
>> errors checked by them didn't occur in a given program run. This can
>> still be useful. But then, production code usually runs with assertion
>> checking off - which is exactly the point where knowing that some bug
>> occurred would be more important...)[/color]
>
> Don't let your production code run with assertion checking off then.[/color]

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.
[color=blue]
> 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.[/color]

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

--
Andreas Rossberg, rossberg@ps.uni-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.