Python from Wise Guy's Viewpoint

[Dirk Thierbach]

Pascal Costanza <costanza at web.de> wrote:
> Dirk Thierbach wrote:

>> Yep. It turns out that you take away lots of bogus programs, and the
>> sane programs that are taken away are in most cases at least questionable
>> (they will be mostly of the sort: There is a type error in some execution
>> branch, but this branch will never be reached)
> 
> No. Maybe you believe me when I quote Ralf Hinze, one of the designers 
> of Haskell:
> 
> "However, type systems are always conservative: they must necessarily 
> reject programs that behave well at run time."

I don't see any contradiction. It's true that type systems must necessarily
reject programs that behave well at run time, nobody is disputing that.
These are the programs that were "taken away". Now why does a type
system reject a program? Because there's a type mismatch in some branch
if the program. Why is the program still well behaved? Very probably 
because this branch never gets executed, or it only executes with 
values where the type mismatch for some reason doesn't matter. There
may be other reasons, but at the moment I cannot think of any.

I don't have statistically evidence, but it would be easy to 
enumerate all terms of a simple language (say, simply typed lambda
calculus with a few constants and ground types) up to a certain length,
and then pick out those that are not well typed but still well behaved.

My guess is that most will be of the type

  (if true then 42 else "abc") + 1

It may not be decidable whether such a condition in an if-statement
is always true, but in this case I would consider such a program also
pretty bogus :-)

If you have an example that is not if this type, I would be interested
to see it.

> Could you _please_ just accept that statement? That's all I am
> asking for!

I have no trouble accepting that statement. As I have said, nobody is
disputing it. What I don't accept is your conclusion that because
one has to reject certain programs, one looses "expressive power".

- Dirk