Python from Wise Guy's Viewpoint

[Andreas Rossberg]

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

Here is a very trivial example, in SML:

20 * 30

Multiplication, as well as literals, are overloaded. Depending on
whether you type this expression as Int8.int (8-bit integers) or
IntInf.int (infinite precision integer) the result is either 600 or an
overflow exception.

So the program does not make sense without type information, because it
does not have an unambiguous (i.e. no) semantics.

I'm ready to admit that it may be a dubious example of a typing feature.
But it is simple, and clearly sufficient to disprove your repeated claim
that static types don't add expressiveness to a language. If you did not
have them for the example above, you needed some other feature to
express the disambiguation.

- Andreas

--
Andreas Rossberg, (e-mail address removed)-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc.

 

[Fergus Henderson]

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

You can easily declare "EuclideanRings" as a type class
(in Haskell/Clean/Mercury, or similar constructs in other languages),
and ensure that you only pass this function values whose type has been
declared to be an instance of that type class.

Generally the type system won't be able to enforce that the
"EuclideanRings" type class really represents Euclidean rings
that conform to all the appropriate axioms. However, declaring
an abstract type like this is nevertheless very useful as documentation:
it makes it clear where the proof obligation lies. _If_ you prove that
every declared instance of the type class is really a Euclidean ring,
then that, together with the type system, will be enough to guarantee
that the function's argument is always a Euclidean ring.

 

[Fergus Henderson]

(e-mail address removed) once said:

Finally, an example that I don't think you can type in Haskell.
You score a point for that.

I don't think it deserves any points, because as another poster said,
in Haskell that is equivalent to

black_hole _ = undefined

 

[John Atwood]

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.

Perhaps, but the paper shows convincingly that statically typed languages
can do a lot of things that Lispers use macros for. Work in
meta-programming, aka mult-stage programming, shows how to more finely
control the power of macros, reflection, etc. See, e.g.:
http://citeseer.nj.nec.com/sheard00accomplishments.html
http://citeseer.nj.nec.com/taha99multistage.html

John

 

[Matthew Danish]

(you can always put a Lisp-style type system on top of a
statically-typed language, with little effort).

This is not true, as I've pointed out on several occasions. Such
systems do not behave like a Lisp-style type system when dealing with
redefinition.

 

[Joe Marshall]

_If_ you prove that
every declared instance of the type class is really a Euclidean ring,
then that, together with the type system, will be enough to guarantee
that the function's argument is always a Euclidean ring.

Yeah, but *that's* the easy part.

 

[Matthew Danish]

Here is a very trivial example, in SML:

20 * 30

Multiplication, as well as literals, are overloaded. Depending on
whether you type this expression as Int8.int (8-bit integers) or
IntInf.int (infinite precision integer) the result is either 600 or an
overflow exception.

May I point out that the correct answer is 600, not overflow?

Something that annoys me about many statically-typed languages is the
insistence that arithmetic operations should return the same type as the
operands. 2 / 4 is 1/2, not 0. Arithmetically, 1 * 1.0 is
well-defined, so why can I not write this in an SML program?

I do believe Haskell does it right, though, with its numeric tower
derived from Lisp.

 

[Dirk Thierbach]

I was working on the assumption that the type language *would* allow
one to express arbitrary types.

It doesn't. (There are languages with a type languages that do
allow to express arbitrary types, but the consequence is that typing
is no longer decidable at compile-time, so your compilation may
not terminate. For many people, this is not acceptable.)

Certainly one can create a sufficiently weak static type system that
terminates under all conditions and produces correct answers within
the system.

Yes. The trick is that there is a fine line between "too weak" and
"not decidable". As I repeatedly said, it helps to think of the
static type system as a tool that automatically writes tests in
a limited area, but these tests are more powerful than unit tests
because they work on all possible execution paths. But this tool
clearly won't write all the tests you need, so for the rest, you
insert checks or write the unit tests by hand.

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

[more stuff with value ranges]

It's not a question whether it will pass or fail. You cannot express
this in the type language.

Maybe the misunderstanding is that you and others think that a static
type checker must now check everything at compile time that is checked
at runtime with dynamic typing. It doesn't, and in those cases where
it doesn't, you of course write the same tests in a statically typed
language as you do in a dynamically typed language.

But that doesn't mean static typechecking is not useful; it *will*
help you in a lot of cases.

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.

But that's not how it works. What you can use the static type system
for is to make two different types, say Byte and Integer, and then
write a conversion routine from Integer to Byte that does a range check,
and the type checker will make sure that this conversion routine
is called everywhere where it is necessary. So you can use the type
checker to remind you when you forget that. (That's quite helpful,
because it is easy to forget adding a manual type check.)

(And, BTW, that's quite different from C where the static typechecker
allows you to assign values of different ranges without ever asking
for a range check.)

- Dirk

 

[Pascal Costanza]

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.

You don't need to check the type on each access. If you only copy a
value from one place to other, and both places are untyped, you don't
need any check at all.

Furthermore, if I remember correctly, dynamically compiled systems use
type inferencing at runtime to reduce the number of type checks.


Pascal

 

[Pascal Costanza]

Perhaps, but the paper shows convincingly that statically typed languages
can do a lot of things that Lispers use macros for.

Right. I have no problems with that. Monads are pretty interesting, and
monads and static typing go very well together.

Work in
meta-programming, aka mult-stage programming, shows how to more finely
control the power of macros, reflection, etc. See, e.g.:
http://citeseer.nj.nec.com/sheard00accomplishments.html
http://citeseer.nj.nec.com/taha99multistage.html

Wait: Meta-programming and multi-stage programming is not the same
thing. The latter is only a subset of the former.

The metaprogramming facility that doesn't let you call the meta program
from the base program and vice versa in the same environment, o
grasshopper, is not the true metaprogramming facility.

Pascal

 

[Pascal Costanza]

Here is a very trivial example, in SML:

20 * 30

Multiplication, as well as literals, are overloaded. Depending on
whether you type this expression as Int8.int (8-bit integers) or
IntInf.int (infinite precision integer) the result is either 600 or an
overflow exception.

So the program does not make sense without type information, because it
does not have an unambiguous (i.e. no) semantics.

I'm ready to admit that it may be a dubious example of a typing feature.
But it is simple, and clearly sufficient to disprove your repeated claim
that static types don't add expressiveness to a language. If you did not
have them for the example above, you needed some other feature to
express the disambiguation.

Sorry, do you really want to say that I can't make my program throw an
exception when some variables are not inside a specified range?

(assert (typep (* 20 30) '(integer 0 255)))


Pascal

 

[Marcin 'Qrczak' Kowalczyk]

Something that annoys me about many statically-typed languages is the
insistence that arithmetic operations should return the same type as the
operands. 2 / 4 is 1/2, not 0. Arithmetically, 1 * 1.0 is
well-defined, so why can I not write this in an SML program?

Confusing integer division with rational division is not a consequence
of static typing, except that with static typing it's not as dangerous as
with dynamic typing (because a function declared as taking floating point
arguments and performing / on them will do the same even if you pass
integers to it, which in most languages will be automatically converted).

But in Haskell / is defined only on types in class Fractional, which
doesn't include integers. Integer division is `div` and `quot` (they
differ for negative numbers). In Pascal 2/4 is 0.5, in SML / is only
for floats, in both languages integer division is spelled div. Most
languages don't support rational numbers, so / on integers can only
return a floating point number or be an error.

Yes, many languages inherited the confusion of divisions from C. This
includes some dynamically typed languages, e.g. Python - but it's planned
to be fixed, and Ruby.

Mixed-type arithmetic is a different story. I'm talking only about 1/2
being equal to 0 in some languages - this doesn't coincide with static
typing.

 

[Matthias Blume]

Sorry, do you really want to say that I can't make my program throw an
exception when some variables are not inside a specified range?

No. Where did you get that from.

His point was that without the type information you don't know whether
the above "program" should be transliterated into this:

(assert (typep (* 20 30) '(integer 0 255)))

or simply this:

(* 20 30)

Matthias

 

[Joachim Durchholz]

May I point out that the correct answer is 600, not overflow?

No, the correct answer isn't 600 in all cases.
If it's infinite-precision arithmetic, the correct answer is indeed 600.
If it's 8-bit arithmetic with overflow, there is no correct answer.
If it's 8-bit arithmetic with wrap-around, the correct answer is 88.
If it's 8-bit arithmetic with saturation, the correct answer is 255.
(The result happens to be independent of whether the arithmetic is
signed or unsigned.)

Using infinite-precision internally for all calculations isn't always
practicable, and in some algorithms, this will give you even wrong
results (e.g. when multiplying or dividing using negative numbers, or
with saturating arithmetic).

Of course, this doesn't say much about the distinction between static
and dynamic typing, actually the issues and unlucky fringe cases seem
very similar to me. (In particular, overloading and type inference don't
tell us whether the multiplication should be done in 8-bit, 16-bit,
machine-precision, infinite-precision, wrap-around, or saturated
arithmetic, and run-time types don't give us any useful answer either.)

Regards,
Jo

 

[Joachim Durchholz]

This is not true, as I've pointed out on several occasions. Such
systems do not behave like a Lisp-style type system when dealing with
redefinition.

Add a State monad and they will do even that.

(I thought we were talking about differences between compile-time and
run-time typing, not about specifics of Lisp.)

Regards,
Jo

 

[Ed Avis]

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?

In a language such as Haskell, there are no constructs that 'would run
correctly' despite being ill-typed. If you define

f :: Int -> Int

then there's no way that f 'would run' if you somehow passed it a
String instead. I should point out, however, that typically a
function will be defined over a whole class of values, eg

f :: Eq a => a -> a

so that the function f works with any type that has equality defined.

In Lisp too, there are no programs that 'would run correctly' after
failing type-checking, because a type checker for Lisp would have to
be more liberal (and so potentially less helpful) than one for a
language like Haskell or ML.

The job of a type checker, just like a syntax checker, is to eliminate
programs which do not work. That's all there is to it.

By narrowing the set of programs which work - that is, introducing
some redundancy into the programming language by increasing the number
of programs which are 'wrong' - you can often save the human
programmer some effort by catching mistakes.

 

[Pascal Costanza]

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

Thanks.


Pascal

 

[Pascal Costanza]

Confusing integer division with rational division is not a consequence
of static typing, except that with static typing it's not as dangerous as
with dynamic typing (because a function declared as taking floating point
arguments and performing / on them will do the same even if you pass
integers to it, which in most languages will be automatically converted).

Sorry, I don't get this. Why should it be more dangerous with dynamic
typing? Common Lisp definitely gets this right, and most probably some
other dynamically typed languages.

Mixed-type arithmetic is a different story. I'm talking only about 1/2
being equal to 0 in some languages - this doesn't coincide with static
typing.

Yes, dynamic vs static typing seems to be irrelevant here. (Although I
wonder why you should need to distinguish between / and div...)


Pascal

 

[prunesquallor]

In a language such as Haskell, there are no constructs that 'would run
correctly' despite being ill-typed. If you define

f :: Int -> Int

then there's no way that f 'would run' if you somehow passed it a
String instead. I should point out, however, that typically a
function will be defined over a whole class of values, eg

f :: Eq a => a -> a

so that the function f works with any type that has equality defined.

What would you like to call those `syntactic constructs' that do not
currently type check in Haskell, yet *may* belong to a class of
syntactic constructs that *could* conceivably be type checked in a
successor to Haskell that has a better type inferencing engine?

Did I close all the loopholes?

Look, early versions of Haskell did not have as powerful a type
inferencing mechanism as the recent versions. What do you call those
syntactic constructs that weren't programs before but are now? What
do you call the syntactic constructs that aren't programs now, but
might be tomorrow? *THOSE ARE THE THINGS WE ARE TALKING ABOUT*

 

[Pascal Costanza]

No. Where did you get that from.

His point was that without the type information you don't know whether
the above "program" should be transliterated into this:




or simply this:

(* 20 30)

Well, what's the obvious meaning?

Meta comment: I think we are already side-stepping too much here. I
don't think this is a useful example to illustrate serious advantages of
either static or dynamic typing. In all languages, you could simply
define a default meaning for the version that doesn't have explicit type
annotations, and then force the programmer to use explicit annotations
for the other ones. (Andreas already said it is a dubious example.)

Can you give a better example of a program that would render meaningless
without type annotations?

Pascal