Python from Wise Guy's Viewpoint

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

"Marshall Spight" <mspight@dnai.c om> writes:
[color=blue]
> It would be really interesting to see a small but useful example
> of a program that will not pass a statically typed language.
> It seems to me that how easy it is to generate such programs
> will be an interesting metric.[/color]

Would this count?

(defun noisy-apply (f arglist)
(format t "I am now about to apply ~s to ~s" f arglist)
(apply f arglist))

[Marshall Spight]

Re: Python from Wise Guy's Viewpoint

"Pascal Costanza" <costanza@web.d e> wrote in message news:bnc8rk$pvk $1@f1node01.rhr z.uni-bonn.de...[color=blue]
> Marshall Spight wrote:
>[color=green][color=darkred]
> >>>It would be really interesting to see a small but useful example
> >>>of a program that will not pass a statically typed language.
> >>>It seems to me that how easy it is to generate such programs
> >>>will be an interesting metric.
> >>>
> >>>Anyone? (Sorry, I'm a static typing guy, so my brain is
> >>>warped away from such programs. :-)
> >>
> >>Have you ever used a program that has required you to enter a number?
> >>
> >>The check whether you have really typed a number is a dynamic check, right?[/color]
> >
> >
> > This is not an example of what I requested. I can easily write
> > a statically typed program that inputs a string, and converts
> > it to a number, possibly failing if the string does not parse to a number.[/color]
>
> ...and what does it do when it fails?[/color]

What it does when it fails is irrelevant to my request
for someone to come up with a small, useful program
that cannot be written in a statically typed language,
since the program you describe can easily be written
in any statically typed language I'm aware of.

I'm perfectly aware of the fact that statically typed languages
have some runtime checks. This is a feature that static
and dynamic languages have in common, so I don't
see what you might be trying to get at.

[color=blue][color=green]
> > I was asking for a small, useful program that *cannot* be written
> > in a statically compiled language (i.e., that cannot statically
> > be proven type-correct.) I'd be very interested to see such
> > a thing.[/color]
>
> I have given this example in another post.[/color]

I'm very sorry, but I didn't see it. Could you help me find it?

[color=blue]
> Please bear in mind that
> expressive power is not the same thing as Turing equivalence.[/color]

No prob.

[color=blue]
> I have given an example of a program that behaves well and cannot be
> statically typechecked. I don't need any more evidence than that for my
> point. If you ask for more then you haven't gotten my point.[/color]

I'm not asking for more; I'm asking to see the program you're referring to.

Also, I was under the impression that this subthread is about
*my* point, which was a request for a small, useful program
that cannot be written in a statically typed language.


Marshall

[Erann Gat]

Re: Python from Wise Guy's Viewpoint

In article <bnc4bg$r6s$1@f 1node01.rhrz.un i-bonn.de>, Pascal Costanza
<costanza@web.d e> wrote:
[color=blue]
> Marshall Spight wrote:[color=green]
> > "Pascal Costanza" <costanza@web.d e> wrote in message[/color][/color]
news:bn8nhq$l04 $1@f1node01.rhr z.uni-bonn.de...[color=blue][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.
> >>
> >>In a dynamically typed language I can concentrate on writing the test
> >>cases first and don't need to write dummy code to make some arbitrary
> >>static checker happy.[/color]
> >
> >
> > This is a non-issue. In both cases, you need the implementing code
> > if you want to be able to run the testcase, and you don't need the
> > implementing code if you don't.[/color]
>
> No, in a dynamically typed language, I don't need the implementation to
> be able to run the testcase.
>
> Among other things:
>
> - the test cases can serve as a kind of todo-list. I run the testsuite,
> and it gives me an exception. This shows what portion of code I can work
> on next.
>
> - when a test case gives me an exception, I can inspect the runtime
> environment and analyze how far the test case got, what it already
> successfully did, what is missing, and maybe even why it is missing.
> With a statically typed language, I wouldn't be able to get that far.[/color]

To be fair, you can do both of those things in statically typed langauges
too, except that you get the error at compile time rather than run time.
[color=blue]
> Furthermore, when I am still in the exceptional situation, I can change
> variable settings, define a function on the fly, return some value from
> a yet undefined method by hand to see if it can make the rest of the
> code work, and so on.[/color]

This is a good point.

E.

[Brian McNamara!]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> once said:[color=blue]
>Brian McNamara! wrote:[color=green]
>> I can imagine Haskell code like
>>
>> y = do x <- myread "34"
>> return x * 2
>> z = do x <- myread "foo"
>> return x * 2
>>
>> where
>>
>> myread :: String -> Maybe a
>> y, z :: Maybe Int
>>
>> and "y" ends up with the value "Just 68" whereas "z" is "Nothing".[/color]
>
>The code you have given above doesn't give the user any feedback, right?
>Do you really think that this is useful?[/color]

It is certainly useful if the strings are coming from a file read over
the network by a batch process that runs nightly on a machine sitting in
a closet.

But I suppose you really want this example
[color=blue][color=green]
>>(defun f (x)
>> (unless (< x 200)
>> (cerror "Type another number"
>> "You have typed a wrong number")
>> (f (read)))
>> (* x 2))[/color][/color]

statically typed, huh? Ok, I'll try. If I come up short, I expect it's
because I'm fluent in neither Haskell nor Lisp, not because it can't be
done.

readInt :: IO Maybe Int

cerror :: String -> String -> IO Maybe a -> IO Maybe a
cerror optmsg errmsg v =
do print errmsg
print ("1: " ++ optmsg)
print "2: Fail"
mx <- readInt
r <- if (maybe False (=1) mx)
then v
else return Nothing
return r

f :: Int -> IO Maybe Int
f x = do x' <- if x < 200
then cerror "Type another number"
"You have typed a wrong number"
(do mx <- readInt
do x <- mx
return f x)
else return (return (x * 2))
return x'

I think that maybe works. Perhaps someone who really knows Haskell and
has a Haskell compiler can check it and/or tidy it up a little if
necessary.

--
Brian M. McNamara lorgon@acm.org : I am a parsing fool!
** Reduce - Reuse - Recycle ** : (Where's my medication? ;) )

[Henrik Motakef]

Re: Test cases and static typing

Dirk Thierbach <dthierbach@gmx .de> writes:
[color=blue]
> OTOH, Lisp certainly doesn't check types,[/color]

Ho hum. I realize that this is probably not what you meant, but given
the existence of usenet archives, I have to oppose this statement
anyway ;-)

Lisp implementations are not /required/ to check types at compile time
(they are at run time, when they encounter a CHECK-TYPE form), but
that doesn't neccessarily mean they don't.

Even if the CL type system isn't as friendly for such things as the
ones of Ocaml or Haskell may be (try proving whether a value is of
type (satisfies (lambda (x) (= x (get-universal-time))))[1] for a
start), some implementations really do honor you optional type
declarations, and even do some significant type inferencing. They
won't just abort compilation if they think you program could be
improved type-wise, but they will issue a warning, which is just as
good IMHO.
[color=blue]
> OTOH, this example is tied to a specific Lisp debugger feature.[/color]

The Lisp debugger is a standardized part of the language, just like
the type system is.


[1] Yes, yes, you'll have to create a named function for that lambda
expression in reality scince SATISFIES doesn't actually accept
lambdas for some reason, but you get the point.

[John Atwood]

Re: Static typing

Pascal Costanza <costanza@web.d e> wrote:
[color=blue]
>Mastering a programming language is a very long process.
>[color=green]
>> So you see that with different tools, you cannot do
>> it in exactly the same way as with the old tools, and immediately you
>> start complaining that the new tools have "less expressive power",
>> just because you don't see that you have to use them in a different
>> way. The "I can do lot of things with macros in Lisp that are
>> impossible to do in other languages" claim seems to have a similar
>> background.[/color]
>
>No, you definitely can do a lot of things with macros in Lisp that are
>impossible to do in other languages. There are papers that show this
>convincingly . Try
>ftp://publications.ai.mit.edu/ai-pub...df/AIM-453.pdf for a
>start. Then continue, for example, with some articles on Paul Graham's
>website, or download and read his book "On Lisp".[/color]

That's a great paper; however, see Steele's later work:

http://citeseer.nj.nec.com/steele94building.html

John

[Dirk Thierbach]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> wrote:[color=blue]
> Dirk Thierbach wrote:[/color]
[color=blue][color=green]
>> 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)[/color]
>
> 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."[/color]

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.
[color=blue]
> Could you _please_ just accept that statement? That's all I am
> asking for![/color]

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

[Dirk Thierbach]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> wrote:[color=blue]
> Brian McNamara! wrote:[/color]
[color=blue][color=green][color=darkred]
>>> Have you ever used a program that has required you to enter a
>>> number? The check whether you have really typed a number is a
>>> dynamic check, right?[/color][/color][/color]

This dynamic check doesn't necessarily translate to a type check.
Not everything boils down to types just because you're using "numbers".
As Brian has shown, you can use a type that says "maybe it is a
number, maybe it isn't". And that is statically safe, even if we
cannot decide at compile-time if it will be a number of not.
[color=blue][color=green]
>> Yes, but this doesn't imply we can't write a statically-typed program to
>> handle the situation...[/color][/color]
[color=blue]
> The code you have given above doesn't give the user any feedback, right?
> Do you really think that this is useful?[/color]

There's no problem with adding feedback, other than you have now to
package up the whole thing into the IO monad, because you have side
effects. The important point is the "Maybe" type. With a function like

multiread :: IO (Maybe Int)

you can write code as in

f = do z <- multiread
let y = do x <- z
return (x * 2)
return y

The outer "do" handles the IO monad, the inner "do" will ignore the
calculation if there is no value available. Here's a (very quickly
written, and very bad; I am sure it can be done with more elegance)
implementation of multiread:

myread :: String -> IO (Maybe Int) -> IO (Maybe Int)
myread "" _ = return Nothing
myread s failcont = result (reads s) where
result [(x, "")] = return (Just x)
result _ = failcont

multiread :: IO (Maybe Int)
multiread = do
s <- getLine
myread s (print "Reenter number, or press Enter to abort" >> multiread)


- Dirk

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Dirk Thierbach <dthierbach@gmx .de> writes:
[color=blue]
> 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.[/color]

*or* because the type system was unable to prove that there *isn't* a
type mismatch in *all* branches.

[Dirk Thierbach]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net wrote:[color=blue]
> I don't understand why you think that most of them will be `dead code'.[/color]

Because otherwise the code will be executed, and this will result
in a crash -- there must be a reason why the type checker complains.
[color=blue]
> I don't understand why a smart type checker would complain about dead
> code.[/color]

Because in general, it is not decidable if some part of the code will
be executed or not (halting problem).

- Dirk

[Dirk Thierbach]

Re: Test cases and static typing

Pascal Costanza <costanza@web.d e> wrote:
[color=blue]
> A flexible and useful IDE must treat static type checking as a separate
> tool. It needs to be able to do useful things with code that isn't
> correct yet.[/color]

I don't agree with the "must", but type checking is a seperate phase
in the compiler. It should be possible to make an IDE that treats
it that way. But I doubt that particular point is high on the priority
list of any potential programmer of an IDE.
[color=blue]
> And that's all I wanted from the very beginning - static typing as an
> additional tool, not as one that I don't have any other choice than use
> by default.[/color]

And that's fine, but it is not an issue of static typing.
[color=blue][color=green][color=darkred]
>>>>>The type system might test too many cases.[/color][/color][/color]
[color=blue]
> No, it's not better to give an example in a different language. The
> whole point of my argument is that the code above cannot be statically
> type-checked.[/color]

You can look now at two examples of code like this that can be
statically type-checked.

And I had the impression that you wanted to explain why a "type system
might test too many cases". I still don't understand this argument. I
don't see any "case" that the type system will test in the above
program, let alone "too many".
[color=blue][color=green]
>> I could probably rewrite the code with an approximation to cerror
>> (with the restriction that non-local control structures don't
>> translate one to one), but even then I don't see why the type system
>> would test too many cases for this example.[/color][/color]
[color=blue]
> I don't want an "approximat ion of cerror". I want cerror![/color]

Then use Lisp and cerror. Nobody forces you to use anything else. The
problem is again that you want to do it only in exactly the same way
as you are used to doing it. You don't see how to do it in another
language, and then you say "it cannot be done". And that's just wrong.

So can we settle on "you like to do it your way, but it is possible
to do everything you want in a statically typed language if
you're a little bit more flexible"? (That means of course that if
you refuse to be a bit more flexible, it cannot be done in exactly
the same way -- after all, they are different languages.)

As long as you say "this cannot be done" you'll get answers showing
you that it can indeed be done, only in a way that is a little bit
different. Then you say "yes, but that's not how I want it. You're
trying to force to use me something I don't want!".

It gets a bit silly after some iterations. Let's stop it.

- Dirk

[Andreas Rossberg]

Re: Python from Wise Guy's Viewpoint

"Pascal Costanza" <costanza@web.d e> wrote:[color=blue]
>[color=green]
> > But you completely ignore the fact that it also adds expressive power at
> > another end! For one thing, by allowing you to encode certain invariants
> > in the types that you cannot express in another way. Furthermore, by
> > giving more knowledge to the compiler and hence allow the language to
> > automatize certain tedious things.[/color]
>
> I think you are confusing things here. It gets much clearer when you
> separate compilation/interpretation from type checking, and see a static
> type checker as a distinct tool.
>
> The invariants that you write, or that are inferred by the type checker,
> are expressions in a domain-specific language for static program
> analysis. You can only increase the expressive power of that
> domain-specific language by adding a more elaborate static type system.
> You cannot increase the expressive power of the language that it reasons
> about.[/color]

Sorry, but that reply of yours somewhat indicates that you haven't really
used modern type systems seriously.

All decent type systems allow you to define your own types. You can express
any domain-specific abstraction you want in types. Hence the type language
gives you additional expressive power wrt the problem domain.
[color=blue]
> An increase of expressive power of the static type checker decreases the
> expressive power of the target language, and vice versa.[/color]

That's a contradiction, because the type system is part of the "target"
language. You cannot separate them, because the type system is more then
just a static analysis phase - you can program it.
[color=blue]
> As a sidenote, here is where Lisp comes into the game: Since Lisp
> programs can easily reason about other Lisp programs, because there is
> no distinction between programs and data in Lisp, it should be pretty
> straightforward to write a static type checker for Lisp programs, and
> include them in your toolset.[/color]

It is not, because Lisp hasn't been designed with types in mind. It is
pretty much folklore that retrofitting a type system onto an arbitrary
language will not work properly. For example, Lisp makes no distinction
between tuples and lists, which is crucial for type inference.
[color=blue]
> It should also be relatively straightforward to make this a relatively
> flexible type checker for which you can increase/decrease the level of
> required conformance to the (a?) type system.
>
> This would mean that you could have the benefits of both worlds: when
> you need static type checking, you can add it. You can even enforce it
> in a project, if the requirements are strict in this regard in a certain
> setting. If the requirements are not so strict, you can relax the static
> type soundness requirements, or maybe even go back to dynamic type[/color]
checking.

I don't believe in soft typing, since it cannot give you the same guarantees
as strong typing. If you want to mix static and dynamic typing, having
static typing as the default and *explicit* escapes to dynamic typing is the
only sensible route, IMNSHO. Otherwise, all the invariants and guarantees
typing gives you are lost.
[color=blue][color=green]
> > Overloading is one obvious example
> > that increases expressive power in certain ways and crucially relies on
> > static typing.[/color]
>
> Overloading relies on static typing? This is news to me. What do you mean?[/color]

If you want to have extensible overloading then static types are the only
way I know for resolving it. Witness Haskell for example. It has a very
powerful overloading mechanism (for which the term 'overloading' actually is
an understatement) . It could not possibly work without static typing, which
is obvious from the fact that Haskell does not even have an untyped
semantics.
[color=blue][color=green]
> > So there is no inclusion, the "expressiveness " relation is unordered wrt
> > static vs dynamic typing.[/color]
>
> No, I don't think so.[/color]

Erasing type information from a program that uses type abstraction to
guarantee certain post conditions will invalidate those post conditions. So
you get a program with a different meaning. It expresses something
different, so the types it contained obviously had some expressive power.

Erasing type information from a program that uses overloading simply makes
it ambiguous, i.e. takes away any meaning at all. So the types definitely
expressed something relevant.

- Andreas

[Adrian Hey]

Re: Python from Wise Guy's Viewpoint

ketil+news@ii.u ib.no wrote:[color=blue]
> While Mr. Martin probably should get out more, I must admit that I
> have a nagging feeling about typing and object orientation. Somebody
> else correlated typing with imperativity, and I suspect dynamic typing
> is a better match for OO than static typing. But I'm probably making
> the common error of comparing with the rather pedestrian type systems
> of C++ and Java, perhaps O'Haskell and OCaml have systems that work
> better?[/color]

I have a my own pet theories to explain the current exitement about
dynamically typed languages. Here they are..

1- Most of this buzz comes from OO folk, many of whom will only have
(bad) experience of static typing from C/C++/Java.

2- Development of static type systems (and type inferencers/checkers)
which are strong enough to offer cast iron *guarantees* but at the
same time are flexible enough to allow useful programs involves
some tricky theory that few really understand (I won't pretend I do).
But some language developers don't want to get to bogged down with
all that difficult and boring theory stuff for however many months
or years it takes. They want to make their language cooler than the
competition right now, so have to rely exclusively on the expensive
run time checks they call "dynamic typing".

3- Given that once this design decision (hack) has been made it is
irreversible for all practical purposes, enthusiasts/advocates of
these languages need to "make a virtue of necessesity" by advertising
all the advantages that dynamic typing brings (allegedly) and
spreading FUD about all the things you can't do with statically typed
languages (allegedly). It is likely they will cite C++ in their
evidence. :-)

Regards
--
Adrian Hey

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Dirk Thierbach <dthierbach@gmx .de> writes:
[color=blue]
> prunesquallor@c omcast.net wrote:[color=green]
>> I don't understand why you think that most of them will be `dead code'.[/color]
>
> Because otherwise the code will be executed, and this will result
> in a crash -- there must be a reason why the type checker complains.[/color]

Allow me to rephrase: I don't understand why you think *most* of them
will be dead code. Aren't there other cases where the type checker
would complain?

[color=blue]
>[color=green]
>> I don't understand why a smart type checker would complain about dead
>> code.[/color]
>
> Because in general, it is not decidable if some part of the code will
> be executed or not (halting problem).
>
> - Dirk[/color]

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

"Andreas Rossberg" <rossberg@ps.un i-sb.de> writes:
[color=blue]
> Sorry, but that reply of yours somewhat indicates that you haven't really
> used modern type systems seriously.
>
> All decent type systems allow you to define your own types. You can express
> any domain-specific abstraction you want in types. Hence the type language
> gives you additional expressive power wrt the problem domain.[/color]

Cool! So I can declare `Euclidean rings' as a type an ensure that I
never pass a non-Euclidean ring to a function?