Python from Wise Guy's Viewpoint

[Remi Vanicat]

Could you provide a link to an example of such a post?

I've no link but I'm sure to have seen (here or on one of the caml
list) people trying to do polymorphic recursion, something that is not
easy to do in ocaml...

 

[Nikodemus Siivola]

Apologies for the out-of-context snippage:

A 100,000 line program in an untyped language is useless to me if I am

^^^^^^^

Your choice of word here makes me suspect that you _may_ understand
something quite different than most of the residents of cll and clp by
dynamic typing:

dynamic typing is *not* the same as untyped!

Of course, maybe it was just an unfortunate choice of words.

Cheers,

-- Nikodemus

 

[Pascal Costanza]

Please do /not/ draw your examples from Java, C++, or Eiffel. Modern
static type systems are far more flexible and powerful, and far less
obtrusive than the type systems used in these languages.

This was just one obvious example in which you need a workaround to make
the type system happy. There exist others.

A modern type system has the following characteristics:

I know what modern type systems do.


Pascal

 

[Kenny Tilton]

By whose definition? What *is* your definition of "useful"? It is
clear to me that static typing improves maintainability, scalability,
and helps with the overall design of software.

That sounds right. When I divided a large app into half a dozen sensible
packages, several violations of clean design were revealed. But just a
few, and there was a ton of code.

I did a little C++ and Java once, porting Cells to those languages. This
was existing code, so I did not have to explore as I coded. It was a
total pain, but then it was pretty easy to get working because so many
casual goofs got caught by the compiler.

I just would never want to write original code this way, because then I
am working fast and loose, doing this, doing that, leaving all sorts of
code in limbo which would have to be straightened out to satisfy a compiler.

The other problem with static typing is that it does not address the
real problem with scaling, viz, the exponential explosion of state
interdependencies. A compiler cannot check the code I neglect to write,
leaving state change unpropagated to dependent other state, nor can it
check the sequence of correctly typed statements to make sure state used
in calculation X is updated before I use that state.

kenny

 

[Pascal Costanza]

Note that most literature contrasts dynamic typing with the static type
systems of C++ and/or Java. Good type systems are /far/ better.

You are changing topics here.

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.

But only at runtime, where a logic flaw may or may not trigger the
assertion.

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.

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

Don't let your production code run with assertion checking off then.

A test suite can never catch all permutations of data that may occur (on
a modern processor, you can't even check the increment-by-one operation
with that, the universe will end before the CPU has counted even half of
the full range).

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.

Well, I did - and the results were, ahem, unimpressive.

The results that are reported in the papers I have read are very
impressive. Can you give me the references to the papers you have read?

Besides, HotSpot is for Java, which is statically typed, so I don't
really see your point here... unless we're talking about different VMs.

Oh, so you haven't read the literature? And above you said you did.

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.

When all you wanted to say is that Java is not fast, that's not quite
true. The showstopper for Java is the Swing library. Java itself is very
fast.

In certain cases it's even faster than C++ because the HotSpot VM can
make optimizations that a static compiler cannot make. (For example,
inline virtual methods that are known not to be overridden in currently
loaded classes.)

And, yes, VMs got pretty fast these days (and that actually happened
several years ago).
It's only that compiled languages still have a good speed advantage -
making a VM fast requires just that extra amount of effort which, when
invested into a compiler, will make the compiled code still run faster
than the VM code.
Also, I have seen several cases where VM code just plain sucked
performance-wise until it was carefully hand-optimized. (A concrete
example: the all-new, great graphics subsystem for Squeak that could do
wonders like rendering fonts with all sorts of funky effects, do 3D
transformations on the fly, and whatnot... I left Squeak before those
optimizations became mainstream, but I'm pretty sure that Squeak got
even faster. Yet Squeak is still a bit sluggish... only marginally so,
and certainly no more sluggish than the bloatware that's around and that
commercial programmers are forced to write, but efficiency is simply
more of a concern and a manpower hog than with a compiled language.)

I know sluggish software written in statically typed languages.

Hey, there are also excellent programs written in assembly. By your
argument, using a higher language is not a necessary condition for
writing excellent languages.
Right.

The question is: what effort goes into an excellent program? Is static
typing a help or a hindrance?

Right, that's the question.

I'm still unconvinced that an inferring type system is worse than
run-time type checking. (Except for that "dynamic metaprogramming" thing
I'd like to know more about. In my book, things that are overly powerful
are also overly uncontrollable, but that may be an exception.)

Check the literature about metaobject protocols.


Pascal

 

[Adrian Hey]

Have you made sure that this is not a circular argument?

It is obviously not a circular argument.

Does "consistent design" mean "acceptable by a type checker" in your book?

Fergus was refering to programs that simply would not work, even if the
compiler ignored the type errors and generated code anyway. Obviously
not all type inconsistent programs fall into this category (only about
99.999..% of them. I've been using statically typed FPL's for a
good few years now, and I can only think of one occasion where I had
"good" code rejected by the type checker (and even then the work around
was trivial). All other occasions it was telling me my programs were
broken (and where they were broken), without me having to test it.

This is good thing.

As for dynamics, I don't think anybody would deny the usefulness of a
dynamic type system as a *supplement to* the static type system. (As
you have observed, there are occasions when type checking just can't
be done at compile time). But no way is a dynamic type system an
adequate *substitute for* modern static type systems. Most code
can be (and should be IMO) checked for type errors at compile time.

Regards

 

[Dirk Thierbach]

Unless the static type system takes away the expressive power that I need.

Even within a static type system, you can always revert to "dynamic
typing" by introducing a sufficiently universal datatype (say,
s-expressions).

Usually the need for real runtime flexiblity is quite localized (but
of course this depends of the application). Unless you really need runtime
flexibility nearly everywhere (and I cannot think of an example where
this is the case), the universal datatype approach works quite well
(though you loose the advantages of static typing in these places, of
course, and you have to compensate with more unit tests).

I have given reasons when not to use a static type system in this
thread.

Nobody forces you to use a static type system. Languages, with their
associated type systems, are *tools*, and not religions. You use
what is best for the job.

But it's a bit stupid to frown upon everything else but one's favorite
way of doing things. There are other ways. They may work a bit
differently, and it might be not obvious how to do it if you're used
to doing it differently, but that doesn't mean other ways are
completely stupid. And you might actually learn something once
you know how to do it both ways

Please take a look at the Smalltalk MOP or the CLOS MOP and tell
me what a static type system should look like for these languages!

You cannot take an arbitrary language and attach a good static type
system to it. Type inference will be much to difficult, for example.
There's a fine balance between language design and a good type system
that works well with it.

If you want to use Smalltalk or CLOS with dynamic typing and unit
tests, use them. If you want to use Haskell or OCaml with static typing
and type inference, use them. None is really "better" than the other.
Both have their advantages and disadvantages. But don't dismiss
one of them just because you don't know better.

- Dirk

 

[Remi Vanicat]

You are changing topics here.

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.

 

[Joe Marshall]

Pascal Costanza:

Ummm, both are infinite and both are countably infinite, so those sets
are the same size. You're falling for Hilbert's Paradox.

They aren't the same size if you limit the length of the program. This
is a reasonable restriction if you are interested in programs that might
be realizable within your lifetime.

Also, while I don't know a proof, I'm pretty sure that type inferencing
can do addition (and theorem proving) so is equal in power to
programming.

Yes, this is true. But it is also the case that a powerful enough
static type checker cannot be proven to halt or produce an answer in a
time less than that required to run the program being checked. It
makes little difference if the type checker produces the answer or the
program produces the answer if they both take about the same time to
run. Of course, it is generally more difficult to program in the type
metalanguage than in the target language.

 

[Pascal Costanza]

Not in ocaml.
ocaml is statically typed.

How does ocaml make sure that you don't get a message-not-understood
exception at runtime then?


Pascal

 

[Matthias Blume]

Apologies for the out-of-context snippage:

^^^^^^^

Your choice of word here makes me suspect that you _may_ understand
something quite different than most of the residents of cll and clp by
dynamic typing:

dynamic typing is *not* the same as untyped!

Ah, are we quibbling about *that* again? Words, words, words...

If you want to know how much I know about the difference between typed
and untyped (or "statically typed" vs. "dynamically typed" as you
prefer), look up my track record on implementing languages in either
part of the PL world.

Yes, "dynamically typed" programs are "typed", but the word "type"
here means something quite different from what it means when it is
used with the qualifier "static". I prefer the latter use, and from
that point of view there is only one (static) type in dynamically
typed programs, hence my use of the word "untyped". (If you have only
one (static) type, you might as well not even think about that fact.)

Anyway, unfortunate or not, we are both thinking about the same class
of languages. That shall suffice.

Matthias

PS: When I say "untyped" I mean it as in "the _untyped_ lambda
calculus".

 

[Matthias Blume]

The other problem with static typing is that it does not address the
real problem with scaling, viz, the exponential explosion of state
interdependencies. A compiler cannot check the code I neglect to
write, leaving state change unpropagated to dependent other state, nor
can it check the sequence of correctly typed statements to make sure
state used in calculation X is updated before I use that state.

Yes, the usefulness of static types seems to be inversely proportional
to the imperativeness of one's programming style (Haskell, Miranda).
Static types *really* shine in purely functional settings. In mostly
functional settings (SML, OCaml) they lose some of their expressive
"punch" if you start playing with mutable data structures. In
languages that heavily rely on imperative features (mutable state,
object identity, imperative I/O, exceptions) their usefulness goes
increasingly down the drain.

Matthias

 

[Matthias Blume]

The final statement is correct, but you don't need to solve the
halting problem: it's enough to allow the specification of some
easy-to-prove properties, without hindering the programmer too much.

In fact, you should never need to "solve the halting problem" in order
to statically check you program. After all, the programmer *already
has a proof* in her mind when she writes the code! All that's needed
-) is for her to provide enough hints as to what that proof is so
that the compiler can verify it. (The smiley is there because, as we
are all poinfully aware of, this is much easier said than done.)

Matthias

 

[Matthias Blume]

Have you made sure that this is not a circular argument?

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.

Does "consistent design" mean "acceptable by a type checker" in your book?

I cannot speak for Fergus, but I suspect (and hope!) the answer is
"no". By "consistent design" we usually mean design that is free of
certain problems at the time the code executes on a real machine.

Matthias

 

[Pascal Costanza]

Pascal Costanza wrote:

I've been using statically typed FPL's for a
good few years now, and I can only think of one occasion where I had
"good" code rejected by the type checker (and even then the work around
was trivial). All other occasions it was telling me my programs were
broken (and where they were broken), without me having to test it.

This is good thing.

Maybe you haven't written the kind of programs yet that a static type
system can't handle.

As for dynamics, I don't think anybody would deny the usefulness of a
dynamic type system as a *supplement to* the static type system.

I don't deny that static type systems can be a useful supplement to a
dynamic type system in certain contexts.

But no way is a dynamic type system an
adequate *substitute for* modern static type systems. Most code
can be (and should be IMO) checked for type errors at compile time.

There is an important class of programs - those that can reason about
themselves and can change themselves at runtime - that cannot be
statically checked.

Your claim implies that such code should not be written, at least not
"most of the time" (whatever that means). Why? Maybe I am missing an
important insight about such programs that you have.


Pascal

 

[Matthias Blume]

Yes, the usefulness of static types seems to be inversely proportional
to the imperativeness of one's programming style (Haskell, Miranda).
Static types *really* shine in purely functional settings (****).

[...]

Obviously, the parenthetical remark "(Haskell, Miranda)" should be where
the (****) is.

Matthias

 

[Remi Vanicat]

How does ocaml make sure that you don't get a message-not-understood
exception at runtime then?

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

 

[Pascal Costanza]

PS: When I say "untyped" I mean it as in "the _untyped_ lambda
calculus".

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

 

[Matthias Blume]

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.

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]

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.

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