Python from Wise Guy's Viewpoint

[Pascal Costanza]

Those that can be described by the language available for static types
e.g. in Haskell or OCaml.

This sounds like a circular definiton.

Yes, but you will have a hard time developing a static type checker
that will work with such a language.

I am not asking for a definition of the term "static type", but for a
definition of the term "type".

Look at the definition for type in Haskell or OCaml, for example.

Haskell: "An expression evaluates to a value and has a static type."
(http://www.haskell.org/onlinereport/intro.html#sect1.3 )

Where is the definiton for "type"? (without "static"?)

I haven't found a definiton in http://caml.inria.fr/ocaml/htmlman/index.html

Yes, I know. What does that explain?

Let's first get our terminology right.

This depends on the definition of "well-behaved". The claim I make is
that for a suitable definition of "well-behaved", it is not an
objective truth. And even if you stick to your definition of
"well-behaved", it doesn't really matter in practice.

"well-behaved" means "doesn't show malformed behavior at runtime", i.e.
especially "doesn't core dump".

"Behavior" is a term that describes dynamic processes. I am only
interested in dynamic behavior here.

I don't mind if you want to change that terminology. Let's just rephrase
it: Static type systems need to reject programs that wouldn't
necessarily fail in serious ways at runtime.

What kind of arguments would you like to have? I have tried to
show with a few examples that even programs that you think should
be rejected with static typing will be accepted (if you allow for
the fact that they are written in a different language).

Yes, for some of them.

I didn't say that. Please do not put up a strawman. In fact, I
explicitely said "you use whatever tool you like best".

But that was the original question that initiated this thread. If we
have an agreement here, that's perfect!

And you didn't convince me; all your examples can be statically
typed.

What about the example in
http://groups.google.com/[email protected]
?

I don't think this can be done without a serious rewrite.

That's maybe the important point. HOW DO YOU KNOW IF YOU HAVE NEVER
TRIED IT? (In a language with good static typing, not in a language
with lousy static typing). And obviously you haven't tried it,
otherwise you wouldn't give examples that can be easily statically
typed, or confuse exceptions or dynamic checks with static type checks.
So it cannot come from your personal experience.

Right, it comes from a more principled consideration: You can't have
metacircularity in a statically type language. You might be able to have
metacircularity if you strictly separate the stages, but as soon as you
want to be able to at least occasionally call base code from meta code
and vice versa, then you lose.

Metacircularity gives me the guaranntee that I can always code around
any unforeseeable limitations that might come up, without having to
start from scratch.

So, yes, I am interested in having the opportunity to change invariants
during the runtime of a program. This might sound self-contradictory,
but in practice it isn't. Remember, "One man's constant is another man's
variable." (see http://www-2.cs.cmu.edu/afs/cs.cmu.edu/Web/csd/perlis.html )

But you insist that dynamically typed languages are "better" or
"superior to" statically typed, because you claim you cannot do things
in a statically typed language that you can do in a dynamically typed
one. That's the point where I disagree. I don't ask you to use a
statically typed language, I just want you to give admit that both
are equally good in this respect, or at least you should sit down and
verify that yourself before saying it.

I haven't said that I can do more things in a dynamically typed
language. I have said that statically typed languages need to reject
well-behaved programs. That's a different claim. We are not talking
about Turing equivalence.

If a base program calls its meta program and changes types, you can't
type check such a program by definition.

For example:

(defun check (x)
(integerp x))

(defun example-1 ()
(let ((x 5))
(assert (check x))
(print 'succeeded)
(eval '(defun check (x)
(stringp x)))))

Now, this might seem nonsensical, but consider this:

(defun example-2 ()
(eval '(defun check (x)
(realp x)))
(example-1))



Pascal

 

[Pascal Costanza]

Actually it does, in a statically typed language.

No, it doesn't.

If you write a
function which expects a Boolean and you pass it a string instead,
it's going to fail one way or another.

Yes, that's one example. This doesn't mean that this implication always
holds. What part of "doesn't imply" is the one you don't understand?

OK, the bad call of that function might never be reachable in actual
execution, but equally the syntax error in Tcl code might not be
reached. I'd rather find out about both kinds of mistake sooner
rather than later.

I don't care for unreachable code in this specific context. A part of
the program that passes a value of type "don't know" to a variable of
type "don't know" might be unacceptable to a static type sytem, but
might still not throw any exceptions at all at runtime. Or, in other
scenarios, only exceptions that you can correct at runtime, which might
be still useful, or even the preferred behavior.

(I do mean a type error and not a type 'error' - obviously if you have
some mechanism to catch exceptions caused by passing the wrong type,
you wouldn't want this to be checked at compile time.)

Exactly.


Pascal

 

[Joe Marshall]

Nitpick: Neither syntactic nor statically checked type errors make
programs fail. Instead, their presence simply implies the absence of a
program. No program, no program failing...

Nitpick: You are defining as a program that which passes a static type
checker. What would you like to call those constructs that make sense
to a human and would run correctly despite failing a static type
check? These are the ones that are interesting to debate.

 

[Pascal Costanza]

Nitpick: Neither syntactic nor statically checked type errors make
programs fail. Instead, their presence simply implies the absence of a
program.

Yes, the absence of a program that might not fail if it wouldn't have
been rejected by the static type system.


Pascal

 

[Joe Marshall]

It will be successfully type checked, because the static type system
does not allow you to express assumptions about value ranges of types.

I was working on the assumption that the type language *would* allow
one to express arbitrary types. Certainly one can create a
sufficiently weak static type system that terminates under all
conditions and produces correct answers within the system. Lisp has
one: everything is a subtype of type t and all programs pass. The
inference is trivial.

But I surely wouldn't be impressed by a type checker that allowed this
to pass:

(defun byte-increment (x)
(check-type x (integer 0 (256)))
(+ x 1))

(defun fib (n)
(if (< n 2)
1
(+ (fib (- n 1)) (fib (- n 2)))))

(print (byte-increment (fib 13)))

On the other hand, if there is no static type mismatch, that doesn't
mean that the program will not crash because of runtime errors
(division by zero, or dynamically checked restrictions).

I think most people here were assuming that passing an integer greater
than 255 to a routine expecting a single 8-bit byte is a type error,
and something that could cause a crash.

 

[Pascal Costanza]

That's a great paper; however, see Steele's later work:
http://citeseer.nj.nec.com/steele94building.html

Yes, I have read that paper. If you want to work with monads, you
probably want a static type system.

(And I think he still likes Scheme and Lisp.

Pascal

 

[Joe Marshall]

My point is that type systems can reject valid programs.

And the point of the guys with FPL experience is that, given a good
type system [*], there are few if any practial programs that would be
wrongly rejected.

We're stating a pretty straightforward, objective, testable hypothesis:

``There exists valid programs that cannot be statically checked by
such-and-such a system.''

and we get back

`yes, but...'
`in our experience'
`*I've* never seen it'
`if the type system is any good'
`few programs'
`no practical programs'
`no useful programs'
`isolated case'
`99% of the time'
`most commercial programs'
`most real-world programs'
`only contrived examples'
`nothings perfect'
`in almost every case'

Excuse us if we are skeptical.

 

[Dirk Thierbach]

Dirk Thierbach wrote:

I am not asking for a definition of the term "static type", but for a
definition of the term "type".

I am happy with a definition of "type" that allows arbitrary sets of
values, but how does this apply to static typing? Or dynamic type
checking? I was talking all the time about a definition of a "static
type", because that it what is relevant here.

Philosophically, there are a lot more sensible definitions for type,
but how does one such definition relate to our discussion?

Haskell: "An expression evaluates to a value and has a static type."
(http://www.haskell.org/onlinereport/intro.html#sect1.3 )

Where is the definiton for "type"? (without "static"?)

There is none, because that is not relevant.

Let's first get our terminology right.

Maybe we should also agree on what we want to use the terminology for.

I don't mind if you want to change that terminology. Let's just
rephrase it: Static type systems need to reject programs that
wouldn't necessarily fail in serious ways at runtime.

I think I already agreed with that several times, didn't I?

But then you have also to add "even if they won't necessarily fail,
nearly all of them won't be well-behaved".

But that was the original question that initiated this thread. If we
have an agreement here, that's perfect!

Finally. *Sigh*. Why do I have to repeat that multiple times?

What about the example in
http://groups.google.com/[email protected]
?

I don't think this can be done without a serious rewrite.

The problem here is that the object system of CLOS and OCaml is
quite different, and Haskell has no objects at all. So you cannot
directly transfer that example to those languages. Not because they
are statically typed, but because they are different. It probably
wouldn't be possible to do exactly the same in another arbitrary
dynamically typed language, either.

But you can trivially simulate the *effects* of your program once
you accept that such a simulation need not use classes.

Please don't mix the differences because of statically/dynamically
typing and because of other language features.

Right, it comes from a more principled consideration: You can't have
metacircularity in a statically type language. You might be able to have
metacircularity if you strictly separate the stages, but as soon as you
want to be able to at least occasionally call base code from meta code
and vice versa, then you lose.

But you don't need metacircularity, because then you simply solve
your problem in a different way.

Metacircularity gives me the guaranntee that I can always code around
any unforeseeable limitations that might come up, without having to
start from scratch.

You can also create very subtle bugs that are difficult to find.

I haven't said that I can do more things in a dynamically typed
language. I have said that statically typed languages need to reject
well-behaved programs. That's a different claim. We are not talking
about Turing equivalence.

Neither am I talking about Turing equivalence.

But if you can agree that it is not harder to express something in a
(properly) statically typed languages then to express it in a
dynamically typed language, then we can stop the discussion here.

What I want you is to give up the point of view that dynamically
languages have an *advantage* because they are dynamically typed.

- Dirk

 

[Neelakantan Krishnaswami]

Yes, the absence of a program that might not fail if it wouldn't have
been rejected by the static type system.

That sentence reflects a misunderstanding of what something like ML's
type system *means*. You're trying to hammer ML into the Lisp mold,
which is leading you to incorrect conclusions.

A value in any programming language is some pattern of bits
interpreted under a type. In Scheme or Lisp, there is a single
universe (a single type) that that all values belong to, which is why
it's legal to pass any value to a function. But in ML, there are
multiple universes of values, one for each type.

This means that the same bit pattern can represent different values,
which is not true in a dynamically typed language. To make this
concrete, consider the following Ocaml code:

type foo = A | B

type baz = C | D

let f1 x =
match x with
| A -> C
| B -> D

let f2 x =
match x with
| C -> 0
| D -> 1

Some apparently-similar Scheme code would look like:

(define (f1 x)
(case x
((A) 0)
((B) 1)))

(define (f2 x)
(case x
((C) 0)
((D) 1)))

The difference between these two programs gets revealed when you look
at the assembly code that the Ocaml compiler produces for f1 and f2,
side by side[*]:

f1: f2:
..L101: .L103:
cmpl $1, %eax cmpl $1, %eax
je .L100 je .L102
movl $3, %eax movl $3, %eax
ret ret
..L100: .L102:
movl $1, %eax movl $1, %eax
ret ret

The code generated for each function is identical, modulo label names.
This means that the bit patterns for the data constructors A/C and B/D
are identical, and the the program only makes sense because A and C,
and B and D are interpreted at different types. (In fact, notice that
the bit-representation of the integer zero and and the constructors A
and C are the same, too.) In contrast, this would not be a valid
compilation of the Scheme program, because A, B, C, and D would all
have to have distinct bit patterns.

So eliminating the types from an ML program means you no longer have a
program, because you can no longer consistently interpret bit patterns
as ML values -- there *isn't* any universal domain that all ML values
really belong to, as you are supposing.

[*] I cleaned up some extraneous alignment stuff, to make what's going
on clearer. But all that was identical too.

 

[Fergus Henderson]

What I want is:

testxyz obj = (concretemethod obj == 42)

Does the code compile as long as concretemethod doesn't exist?

No, because the likelihood of that being a typo (e.g. for `concrete_method')
is too high.

I recently added support to the Mercury compiler for an option
"--allow-stubs". For the equivalent code in Mercury, if this option
is enabled, then it will compile if there is a _declaration_ for
concretemethod, even if there is no _definition_. The compiler will
issue a warning and automatically generate a stub definition which just
throws an exception if it is ever called.

It would be fairly straight-forward to also add support for allowing
code like that to compile even if there was no declaration, but that
does not seems like a good idea to me -- it would make it easier for
typos to go unnoticed, with insufficient compensating benefit.

I'm sure it would also be easy for developers of other statically typed
languages to implement what you want, if they thought it was a good idea.

 

[Matthias Blume]

Nitpick: You are defining as a program that which passes a static type
checker.

Yes, that's how it is usually done with statically typed languages.

What would you like to call those constructs that make sense
to a human and would run correctly despite failing a static type
check?

I don't know. What would you *like* to call them? (They might be
called "programs" -- just programs in another language.)

These are the ones that are interesting to debate.

Right, I am not disputing this. (I was simply nitpicking on
terminology.)

Matthias

 

[Matthias Blume]

Yes, the absence of a program that might not fail if it wouldn't have
been rejected by the static type system.

"would" "if" bah

You first have to define what the meaning of a phrase is going to be
if you let it slip past the type checker even though it is not
well-typed. As Andreas Rossberg pointed out, it is quite often the
case that the type is essential for understanding the semantics.
Simply ignoring types does not necessarily make sense under such
circumstances. So it all depends on how you re-interpret the language
after getting rid of static types.

Matthias

 

[Pascal Costanza]

No, because the likelihood of that being a typo (e.g. for `concrete_method')
is too high.

This proves that a static type system requires you to write more code
than strictly necessary. (Please think twice before you react. This is
not meant as a pejorative remark, even if it strongly sounds like one.
It's just an objective truth. Even if you think that this is how it
should be, it doesn't make my statement wrong.)

I recently added support to the Mercury compiler for an option
"--allow-stubs". For the equivalent code in Mercury, if this option
is enabled, then it will compile if there is a _declaration_ for
concretemethod, even if there is no _definition_. The compiler will
issue a warning and automatically generate a stub definition which just
throws an exception if it is ever called.

It would be fairly straight-forward to also add support for allowing
code like that to compile even if there was no declaration, but that
does not seems like a good idea to me -- it would make it easier for
typos to go unnoticed, with insufficient compensating benefit.

A good development environment gives you immediate feedback on such
kinds of typos. A good compiler for a dynamically type language issues a
warning. So these typos don't go unnoticed. The only difference is that
a dynamically typed language trusts the programmer by default, whereas a
statically typed languages doesn't trust the programmer. (To rephrase
it: A statically typed language gives you stricter support, while the
dynamically typed language gives you weaker support. But that's a
actually more or less the same statement.)

I'm sure it would also be easy for developers of other statically typed
languages to implement what you want, if they thought it was a good idea.

Of course.

It might be interesting to note that dynamically typed language are
probably a really bad idea when you don't have a good IDE. The features
that fans of statically typed languages care about are usually regarded
as part of the development environment's jobs. This is only to indicate
that programming in a dynamically typed language is not as horrible as
you might think when seen in the right context.

And here is one of the probable replies: Statically typed languages
don't require a sophisticated IDE in order to do useful work. This might
be an advantage in some scenarios.

Pascal

 

[Pascal Costanza]

You first have to define what the meaning of a phrase is going to be
if you let it slip past the type checker even though it is not
well-typed. As Andreas Rossberg pointed out, it is quite often the
case that the type is essential for understanding the semantics.
Simply ignoring types does not necessarily make sense under such
circumstances. So it all depends on how you re-interpret the language
after getting rid of static types.

Can you show me an example of a program that does't make sense anymore
when you strip off the static type information?


Pascal

 

[Joachim Durchholz]

My point is that type systems can reject valid programs.

And the point of the guys with FPL experience is that, given a good
type system [*], there are few if any practial programs that would be
wrongly rejected.

We're stating a pretty straightforward, objective, testable hypothesis:

``There exists valid programs that cannot be statically checked by
such-and-such a system.''

and we get back

`yes, but...'
`in our experience'
`*I've* never seen it'
`if the type system is any good'
`few programs'
`no practical programs'
`no useful programs'
`isolated case'
`99% of the time'
`most commercial programs'
`most real-world programs'
`only contrived examples'
`nothings perfect'
`in almost every case'

Excuse us if we are skeptical.

Then be sceptical if you like.
Actually your hypothesis is ill-worded anyway: it says "valid" without
specifying what kind of validity means (which already has lead us into
many irrelevant meanderings about what correctness and validity mean,
and that they cannot be expressed if you don't have specifications). It
ignores that some programs need restructuring to have any useful static
types associated with its items (you can always put a Lisp-style type
system on top of a statically-typed language, with little effort). It
ignores the practical experience of people who indeed say "static typing
with type inference is not a straightjacket but a ladder: supports where
it's helpful, and extending my reach in directions that were unthinkable
before they were invented".
However, all I hear is questions "how to you type this". Whining for the
known and trusted idioms, instead of even thinking about the idioms that
static typing might provide.

Just take the testimony and accept it. Just as I take the testimony that
one can write large programs in Lisp. Stay sceptical if you like - I
certainly do.

I'm just tired of the Costanza-style constant nitpicking, topic evasion,
and not answering to critical questions (such as his experience with
modern type systems - he claims it but shows little evidence for that,
something that makes me suspicious about his credibility in general).

Technical newsgroups are a place for exchanging new ideas, and for
helping people along. This thread has already served that purpose to the
utmost extent imaginable, what's left is squabbling.

Good night and Over and Out for me (except for direct answers to my
posts, where appropriate).

Regards,
Jo

 

[Fergus Henderson]

+ Design process: There are clear indications that processes like
extreme programming work better than processes that require some kind of
specification stage.

This is certainly not clear to me, especially if you consider writing
type declarations to be "some kind of specification stage".

Dynamic typing works better with XP than static
typing because with dynamic typing you can write unit tests without
having the need to immediately write appropriate target code.

That one seems to have been pretty thoroughly debunked by other responses
in this thread. A static type system won't stop you writing unit tests.
And if you want to actually run the unit tests, then you are going to
need appropriate target code, regardless of whether the system is
statically or dynamically typed.

+ Error checking: I can only guess what you mean by this.

I mean compile-time detection of type errors.
I'm just talking about ordinary everyday detection of typos, functions
called with the wrong number of arguments, arguments in the wrong order,
arguments of the wrong type -- that kind of thing.

If you mean something like Java's checked exceptions,
there are clear signs that this is a very bad feature.

No, I do not mean that. I tend to agree that statically checked
exception specifications are not worth the complication and can be
positively harmful in some situations.

+ Efficiency: As Paul Graham puts it, efficiency comes from profiling.
In order to achieve efficiency, you need to identify the bottle-necks of
your program. No amount of static checks can identify bottle-necks, you
have to actually run the program to determine them.

It's not enough to just identify the bottlenecks. You have to make those
bottlenecks go fast! That's a lot harder with a dynamically typed language,
because you pay a lot of overhead: greater memory usage, and hence worse
cache performance, due to less efficient representations of types in memory;
plus added overhead from all of those dynamic type checks. Of course good
compilers for dynamic languages analyze the source to try to infer the types,
but since the language is not statically typed, such analysis will often fail.

 

[Pascal Costanza]

That one seems to have been pretty thoroughly debunked by other responses
in this thread. A static type system won't stop you writing unit tests.
And if you want to actually run the unit tests, then you are going to
need appropriate target code, regardless of whether the system is
statically or dynamically typed.

Not if I only want to check whether the first ten tests work, and don't
care about the remaining ones.

It's not enough to just identify the bottlenecks. You have to make those
bottlenecks go fast! That's a lot harder with a dynamically typed language,
because you pay a lot of overhead: greater memory usage, and hence worse
cache performance, due to less efficient representations of types in memory;
plus added overhead from all of those dynamic type checks. Of course good
compilers for dynamic languages analyze the source to try to infer the types,
but since the language is not statically typed, such analysis will often fail.

Good dynamically typed languages provide very good options in this
regard. However, other Lispers than me can probably provide much better
comments on that.


Pascal

 

[Fergus Henderson]

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.

No -- you don't need to implement the method. You only need to declare it.

Even the need to declare it is really just a property of implementations,
not languages.

Well, the research that ultimately lead to the HotSpot Virtual Machine
originated in virtual machines for Smalltalk and for Self. Especially
Self is an "extremely" dynamic language, but they still managed to make
it execute reasonably fast.

Please correct me if I'm wrong, but as I understand it, iterating over a
collection of values is still going to require keeping some representation
of the type of each element around at runtime, and testing the type for
each element accessed, in case it is not the expected type. AFAIK neither
HotSpot nor the Self compiler do the kind of optimizations which would
be needed to avoid that.

 

[Fergus Henderson]

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.

The following are at least a bit closer to what is meant:

[1] Mark P Jones and Simon Peyton Jones. Lightweight Extensible
Records for Haskell. In Haskell Workshop, Paris, September 1999.
<http://citeseer.nj.nec.com/jones99lightweight.html>

[2] B. R. Gaster and M. P. Jones. A polymorphic type
system for extensible records and variants. Technical
report NOTTCS-TR-96-3, Department of Computer Science,
University of Nottingham, UK, 1996. Available from URL
<http://www.cs.nott.ac.uk/Department/Staff/~mpj/polyrec.html>.
<http://citeseer.nj.nec.com/gaster96polymorphic.html>.

 

[Fergus Henderson]

....
BTW, is (3) really justified? My (admittedly old) experience with ML
was that type errors can be rather hard to track back to their sources.

It depends on whether you declare the types of functions or not.
If you leave it up to the compiler to infer the types of all the
functions, then compilers have a difficult job of pinpointing errors,
because sometimes your incorrectly-implemented functions will be
type-correct, just with a different type than you expected, and this
will then leave to type errors further up the call tree.

But declaring the intended types of functions improves things dramatically.
If you get a type error, and you can't immediately figure out what is wrong,
declaring the intended types of the functions involved and recompiling
will allow you to quickly pinpoint the problem.

Of course, the type checker's error messages won't tell you _exactly_
where the error is; they can only point out inconsistencies, e.g. between
the code for a function and its type declaration, or between the code
for a function and one or more of the type declarations for the functions
that it calls. But such inconsistencies should be easy to resolve;
the programmer should be able to tell which of the contradictory parts
are wrong. (The exception is when the inconsistency actually reveals
a design error; in the worst case, a major redesign may be required.)