Python from Wise Guy's Viewpoint

[Marshall Spight]

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?

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.

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.


Marshall

 

[Pascal Costanza]

Then just do it. Write as many tests as you care; when you're ready,
compile them and run the type checker.

Where's the problem? One thing that is certainly missing for Haskell or
OCaml is a good IDE that supports as many styles of programming
as possible, but even with the primitive command line versions at the
moment you can do what you want in this case.

And anyway, this would be a question of the IDE, not of static typing.

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. Modern IDES even give you parameter lists, etc., when the
code isn't actually completely parsable.

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.

Done. But I still miss the point. OTOH, Lisp certainly doesn't check
types, so I don't see how a Lisp program can be an example of the
type system checking too many cases. OTOH, this example is tied to
a specific Lisp debugger feature. I think it would be better to give
an example in a statically typed language.

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. And the feature presented is extremely helpful, even in
end user applications.

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.

I don't want an "approximation of cerror". I want cerror!



Pascal

 

[Pascal Costanza]

(Aren't you supposed to write the method right after you
write the testcases, though?)
No.



I'll acknowledge dynamic languages have an advantage in interactive
execution, which may be considerable.

Thank you.


Pascal

 

[Marshall Spight]

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.

I can get behind that idea! It strikes me as being better
than what one has now with either statically typed
languages or dynamically typed languages.


Marshall

 

[Pascal Costanza]

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.

....and what does it do when it fails?

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.

I have given this example in another post. Please bear in mind that
expressive power is not the same thing as Turing equivalence.

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.


Pascal

 

[prunesquallor]

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), and can usually be
expressed as equivalent programs that will pass.

I don't understand why you think that most of them will be `dead code'.

I don't understand why a smart type checker would complain about dead
code.

 

[Dirk Thierbach]

Dirk Thierbach wrote:

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

 

[Marshall Spight]

class C {
void m();
}

class D {
void m();
}

...

void doSomething (Object o) {
if (o instanceof C) {
((D)o).m();
}
}

"Oops, by accident method m is also defined in D, although I wanted to
call method m in C."

Doesn't happen in languages with proper name space management. (The
problem is that Java gives you only the illusion of well-behaved
namespaces.)

The above code in Java would fail at runtime. What do you think it
ought to do? What would it do in Python? How is this superior to
what Java does? Do you consider this a real-world example?

Does the fact that you didn't respond to the other items
in my post mean you are no longer holding the position that
"explicitly cast[ing] objects" "is one of the sources for potential bugs
that you don't have in a decent dynamically typed language."


Marshall

 

[prunesquallor]

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.

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]

...and what does it do when it fails?

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.

I have given this example in another post.

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

Please bear in mind that
expressive power is not the same thing as Turing equivalence.

No prob.

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.

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

 

[Brian McNamara!]

The code you have given above doesn't give the user any feedback, right?
Do you really think that this is useful?

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

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.

 

[Henrik Motakef]

OTOH, Lisp certainly doesn't check types,

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.

OTOH, this example is tied to a specific Lisp debugger feature.

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.

 

[Dirk Thierbach]

Brian McNamara! wrote:

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.

The code you have given above doesn't give the user any feedback, right?
Do you really think that this is useful?

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]

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.

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

 

[Dirk Thierbach]

I don't understand why you think that most of them will be `dead code'.

Because otherwise the code will be executed, and this will result
in a crash -- there must be a reason why the type checker complains.

I don't understand why a smart type checker would complain about dead
code.

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

- Dirk

 

[Dirk Thierbach]

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.

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.

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.

And that's fine, but it is not an issue of static typing.

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.

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

I don't want an "approximation of cerror". I want cerror!

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

 

[Dirk Thierbach]

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

I am not sure if I read this correctly, but it seems equivalent to what
I say.

\exists branch. mismatch-in (branch)

should be the same as

\not \forall branch. \not mismatch-in (branch)

Anyway, I don't understand your point.

(Hindley-Milner typechecking works by traversing the expression tree
in postfix order, matching types on binary application nodes. Typing
fails if and only if such a match fails (ignoring constraints or
similar extensions for the moment) If a match fails, there's a problem
in this branch).

- Dirk

 

[John Atwood]

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

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.

That's because you're in an interpreted environemt, not because you're
using a dynamically typed language. Interpreters for statically typed
languages allow the same.

John

 

[Andreas Rossberg]

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.

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.

An increase of expressive power of the static type checker decreases the
expressive power of the target language, and vice versa.

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.

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.

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.

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

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.

Overloading relies on static typing? This is news to me. What do you mean?

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.

No, I don't think so.

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]

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?

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