Python from Wise Guy's Viewpoint

[Andreas Rossberg]

"Matthew Danish" <mdanish at andrew.cmu.edu> wrote:
> > 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.
>
> Tell that to the hackers who worked on the "Python" compiler found in
> CMUCL, SBCL, and some others.  It does extensive type inference for both
> efficiency and correctness.  But it doesn't get in the way (except in
> certain rare cases), it just (noisely) informs you what it thinks.

Clarification: I was talking about strong typing, i.e. full and precise
inference. As I wrote in another posting, I don't believe in soft typing,
since it has exactly the weaknesses that seems to make proponents of dynamic
typing judge type systems having marginal utility: its only use is to flag
more or less trivial errors, and unreliable so.

I would be very, very surprised to see a strong type system put on top of an
untyped language successfully, i.e. without changing or restricting the
language severely.

> > 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.
>
> Correction: it could not work without typing--dynamic typing does not
> imply a lack of typing.  I could be wrong, but it seems you would rule
> out generic functions in the CLOS (and dynamic dispatch in general) with
> the above statement.

See my example below.

> > 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.
>
> This doesn't sound right: erasing type information should not invalidate
> the post conditions; it should simply make it more difficult
> (impossible?) to check the validity of the post conditions.

It does, because it also invalidates the pre conditions, on which the post
conditions depend.

> This program should still work, even if you fail to type-check it, if
> said type-checking would have passed successfully.

This is only a meaningful observation if you look at a closed program. If
you simply erase types from some given piece of code it may or may not
continue to work, depending on how friendly client code will act. In that
sense it definitely changes meaning. You had to protect against that using
other, incomparable features. So there is a difference in expressiveness.

And making modular composition more reliable is exactly the main point about
the expressiveness types add!

> > 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.
>
> This statement is irrelevant because dynamic typing does not eliminate
> type information.

Yes it does. With "dynamic typing" in all its incarnations I'm aware of type
infromation is always bound to values. Proper type systems are not
restricted to this, they can express free-standing or relational type
information.

As an example of the kind of "overloading" (or type dispatch, if you want)
you cannot express in dynamically typed lagnuages: in Haskell, you can
naturally define functions which are overloaded on their return type, i.e.
you don't need any value at all at runtime to do the "dispatch". For
example, consider an overloaded function fromString, that produces values of
potentially arbitrary types from strings.

 - Andreas