Python from Wise Guy's Viewpoint

[Matthew Danish]

Re: Python from Wise Guy's Viewpoint

On Mon, Oct 27, 2003 at 07:00:01PM +0100, Andreas Rossberg wrote:[color=blue]
> Pascal Costanza wrote:[color=green]
> >
> >Can you show me an example of a program that does't make sense anymore
> >when you strip off the static type information?[/color]
>
> 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.[/color]

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.

--
; Matthew Danish <mdanish@andrew .cmu.edu>
; OpenPGP public key: C24B6010 on keyring.debian. org
; Signed or encrypted mail welcome.
; "There is no dark side of the moon really; matter of fact, it's all dark."

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Fergus Henderson wrote:
[color=blue]
> Pascal Costanza <costanza@web.d e> writes:[/color]
[color=blue][color=green]
>>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.[/color]
>
>
> 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.[/color]

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]

Re: Static typing

John Atwood wrote:
[color=blue]
> Pascal Costanza <costanza@web.d e> wrote:
>[color=green]
>>John Atwood wrote:
>>[color=darkred]
>>>Pascal Costanza <costanza@web.d e> wrote:
>>>
>>>>No, you definitely can do a lot of things with macros in Lisp that are
>>>>impossibl e to do in other languages. There are papers that show this
>>>>convincingl y. 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".
>>>
>>>That's a great paper; however, see Steele's later work:
>>> http://citeseer.nj.nec.com/steele94building.html[/color]
>>
>>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. ;)[/color]
>
> Perhaps, but the paper shows convincingly that statically typed languages
> can do a lot of things that Lispers use macros for.[/color]

Right. I have no problems with that. Monads are pretty interesting, and
monads and static typing go very well together.
[color=blue]
> 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[/color]

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]

Re: Python from Wise Guy's Viewpoint

Andreas Rossberg wrote:
[color=blue]
> Pascal Costanza wrote:
>[color=green]
>>
>> Can you show me an example of a program that does't make sense anymore
>> when you strip off the static type information?[/color]
>
>
> 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.[/color]

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]

Re: Python from Wise Guy's Viewpoint

On Mon, 27 Oct 2003 13:40:24 -0500, Matthew Danish wrote:
[color=blue]
> 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?[/color]

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.

--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org. pl
^^ http://qrnik.knm.org.pl/~qrczak/

[Dirk Thierbach]

Re: Python from Wise Guy's Viewpoint

Joe Marshall <jrm@ccs.neu.ed u> wrote:[color=blue]
> Dirk Thierbach <dthierbach@gmx .de> writes:[color=green]
>> It will be successfully type checked, because the static type system
>> does not allow you to express assumptions about value ranges of types.[/color][/color]
[color=blue]
> I was working on the assumption that the type language *would* allow
> one to express arbitrary types.[/color]

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.)
[color=blue]
> Certainly one can create a sufficiently weak static type system that
> terminates under all conditions and produces correct answers within
> the system.[/color]

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.
[color=blue]
> But I surely wouldn't be impressed by a type checker that allowed this
> to pass:[/color]

[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 misunderstandin g 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.
[color=blue]
> 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.[/color]

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

[Matthias Blume]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue]
> Andreas Rossberg wrote:
>[color=green]
> > Pascal Costanza wrote:
> >[color=darkred]
> >>
> >> Can you show me an example of a program that does't make sense
> >> anymore when you strip off the static type information?[/color][/color]
>[color=green]
> > Here is a very trivial example, in SML:[/color]
>[color=green]
> > 20 * 30[/color]
>[color=green]
> > 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.[/color]
>[color=green]
> > So the program does not make sense without type information, because
> > it does not have an unambiguous (i.e. no) semantics.[/color]
>[color=green]
> > 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.[/color]
>
>
> 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?[/color]

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:
[color=blue]
> (assert (typep (* 20 30) '(integer 0 255)))[/color]

or simply this:

(* 20 30)

Matthias

[Joachim Durchholz]

Re: Python from Wise Guy's Viewpoint

Matthew Danish wrote:
[color=blue]
> On Mon, Oct 27, 2003 at 07:00:01PM +0100, Andreas Rossberg wrote:
>[color=green]
>>Pascal Costanza wrote:
>>[color=darkred]
>>>Can you show me an example of a program that does't make sense anymore
>>>when you strip off the static type information?[/color]
>>
>>Here is a very trivial example, in SML:
>>
>> 20 * 30
>>
>>Multiplicatio n, 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.[/color]
>
> May I point out that the correct answer is 600, not overflow?[/color]

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]

Re: Python from Wise Guy's Viewpoint

Matthew Danish wrote:
[color=blue]
> On Mon, Oct 27, 2003 at 05:57:00PM +0100, Joachim Durchholz wrote:
>[color=green]
>>(you can always put a Lisp-style type system on top of a
>>statically-typed language, with little effort).[/color]
>
> 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.[/color]

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]

Re: Python from Wise Guy's Viewpoint

Joe Marshall <jrm@ccs.neu.ed u> writes:
[color=blue]
>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?[/color]

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.

--
Ed Avis <ed@membled.com >

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Fergus Henderson wrote:
[color=blue]
> Pascal Costanza <costanza@web.d e> writes:
>
>[color=green]
>>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.[/color]
>
>
> 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/jones99lightwei ght.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/gaster96polymor phic.html>.[/color]

Thanks.


Pascal

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Marcin 'Qrczak' Kowalczyk wrote:
[color=blue]
> On Mon, 27 Oct 2003 13:40:24 -0500, Matthew Danish wrote:
>
>[color=green]
>>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?[/color]
>
>
> 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).[/color]

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.
[color=blue]
> 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.[/color]

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


Pascal

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Ed Avis <ed@membled.com > writes:
[color=blue]
> Joe Marshall <jrm@ccs.neu.ed u> writes:
>[color=green]
>>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?[/color]
>
> 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.[/color]

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]

Re: Python from Wise Guy's Viewpoint

Matthias Blume wrote:
[color=blue]
> Pascal Costanza <costanza@web.d e> writes:
>
>[color=green]
>>Andreas Rossberg wrote:
>>
>>[color=darkred]
>>>Pascal Costanza wrote:
>>>
>>>
>>>>Can you show me an example of a program that does't make sense
>>>>anymore when you strip off the static type information?[/color]
>>[color=darkred]
>>>Here is a very trivial example, in SML:[/color]
>>[color=darkred]
>>> 20 * 30[/color]
>>[color=darkred]
>>>Multiplicati on, 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.[/color]
>>[color=darkred]
>>>So the program does not make sense without type information, because
>>>it does not have an unambiguous (i.e. no) semantics.[/color]
>>[color=darkred]
>>>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.[/color]
>>
>>
>>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?[/color]
>
>
> 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:
>
>[color=green]
>>(assert (typep (* 20 30) '(integer 0 255)))[/color]
>
>
> or simply this:
>
> (* 20 30)[/color]

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

[Matthias Blume]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue]
> Can you give a better example of a program that would render
> meaningless without type annotations?[/color]

fun f A = "A"
| f B = "B"

This could be the function that always returns "A" for arbitrary
arguments, it could be the function that can only be legally applied
to the value (constructed by) A where it returns "A", it could be the
function that can be applied precisely to values A and B, it could
accept more than those two and raise an exception if the argument is
neither A nor B, it could be the function that can be applied to A
where it returns "A" and also many other values where it always
returns "B", ...

Which of these versions you get depends in part on the typing
environment that is in effect when the above code is encountered by
the compiler.

Matthias

PS: Just in case you wonder, here are examples of type definitions
which would trigger the results outlined above. I go in the same
order:

1. (* no type definition in effect *)
2. datatype t = A
3. datatype t = A | B
4. datatype t = A | B | C
5. datatype t = A | C | D of int | E of real | F of t -> t

Notice that the compiler will probably warn about a redundant match in
cases 1. and 2. and about a non-exhaustive match in case 4.