Python from Wise Guy's Viewpoint

[Pascal Costanza]

Hmm, could a kind of "meta type system protocol" be feasible? I.e., a
language environment in which you could tweak the type system to your
concrete needs, without having to change the language completely?

Yes. But that is still a research issue at this stage.
For some work in this area, see the following references:

[1] Martin Sulzmann, "A General Type Inference Framework for
Hindley/Milner Style Systems." In 5th International Symposium
on Functional and Logic Programming (FLOPS), Tokyo, Japan,
March 2001.

[2] Sandra Alves and Mario Florido, "Type Inference using
Constraint Handling Rules", Electronic Notes in Theoretical
Computer Science volume 64, 2002.

[3] Kevin Glynn, Martin Sulzmann, Peter J. Stuckey,
"Type Classes and Constraint Handling Rules",
University of Melbourne Department of Computer Science
and Software Engineering Technical Report 2000/7, June 2000.

Also the work on dependent type systems, e.g. the language Cayenne,
could be considered to fit in this category.

Thanks a lot for the references!


Pascal

 

[Joachim Durchholz]

Now you're conflating two readings of "want declarations" (i.e. "want
them whenever they're convenient for optimizing" vs. "want them
everywhere and always")

Type inference is about "as much static checking as possible with as
little annotations as absolutely necessary".
HM typing is extremely far on the "few declarations" side: a handful
even in large systems.

It sounds unbelievable, but it really works.

Oh, there's one catch: Most functional programs have heaps of type
definitions similar to this one:
Tree a = Leaf a
| Node (Tree a) (Tree a)
| Empty
However, these definitions don't only declare the type, they also
introduce constructors, which also serve as inspectors for pattern matching.

In other words, the above code is all that's needed to allow me to
construct arbitrary values of the new type (gratuitious angle brackets
inserts to make the code easier to recognize with a C++ background),
like this:
Leaf 5 -- Creates a Leaf <Integer> object that contains value 5
Node Empty Empty -- Creates a node that doesn't have leaves
-- Type is Tree <anything>, i.e. we can insert this object into
-- a tree of any type, since there's no way that this can ever
-- lead to type errors.
Node (Leaf 5) (Leaf 6) -- Creates a node with two leaves

It also allows me to use the constructor names as tags for pattern
matching. Note that every one of the following three definitions
consists of the name of the function being defined, a pattern that the
arguments must follow to select this particular definition, and the
actual function body (which is just an expression here). Calling a
function with parameters that match neither pattern is considered an
error (which is usually caught at compile time but not in all cases -
not everything is static even in functional languages).
mapTree f (Leaf foo) = Leaf f foo
-- If mapTree if given a "something" called f,
-- and some piece of data that was constructed using Leaf foo,
-- then the result will be obtained by applying f as a function
-- to that foo, and making the result a Leaf.
-- The occurence of f in a function position on the right side
-- makes type inference recognize it as a function.
-- The Leaf pattern (and, incidentally, the use of the Leaf
-- constructor on the right side) will make type inference
-- recognize that the second parameter of mapTree must be
-- of Tree <anything> type. Usage details will also make
-- type inference conclude that f must be a function from
-- one "anything" type to another, potentially different
-- "anything" type.
-- In other words, the type of mapTree is known to be
-- (a -> b) -> Tree a -> Tree b
-- without a single type declaration in mapTree's code!
mapTree f (Node left right) = Node (maptree f left) (maptree f right)
-- This code is structured in exact analogy to the Leaf case.
-- The only difference is that it uses recursion to descend
-- into the subtrees.
-- Incidentally, this definition of mapTree
mapTree f Empty = Empty
-- The null value doesn't need to be mapped, it will look the
-- same on output.
-- Note that this definition of mapTree doesn't restrict the
-- type of f in the least.
-- In HM typing, you usually don't specify the types, every
-- usage of some object adds further restrictions what that
-- type can be. If the set of types that a name can have becomes
-- empty, you have contradictory type usage and hence a type error.

Hope this helps
Jo

 

[Fergus Henderson]

Why? If the collection happens to contain only elements of a single type
(or this type at most), you only need to check write accesses if they
violate this condition. As long as they don't, you don't need to check
read accesses.

So which, if any, implementations of dynamic languages actually perform such
optimizations?

 

[Pascal Bourguignon]

I have worked on projects where people worried about *every cycle*.
(Most of the time I agree with you, though. Still, using infinite
precision by default is, IMO, a mistake.

What are you writing about? Figments of your imagination or real
concrete systems?


[20]> (typep (fact 100) 'fixnum)
NIL
[21]> (typep (fact 100) 'bignum)
T
[22]> (typep (/ (fact 100) (fact 99)) 'fixnum)
T
[23]> (typep (/ (fact 100) (fact 99)) 'bignum)
NIL
[24]> (/ 1 3)
1/3
[25]> (/ 1.0 3)
0.33333334

Where do you see "infinite precision by default"?

 

[Joe Marshall]

Type inference is about "as much static checking as possible with as
little annotations as absolutely necessary".
HM typing is extremely far on the "few declarations" side: a handful
even in large systems.

I certainly don't mind as much static checking as possible. I get a
little put off by *any* annotations that are *absolutely necessary*,
though. My preference is that all `lexically correct' code be
compilable, even if the object code ends up being the single
instruction `jmp error-handler'. Of course I'd like to get a
compilation warning in this case.

It sounds unbelievable, but it really works.

I believe you. I have trouble swallowing claims like `It is never
wrong, always completes, and the resulting code never has a run-time
error.' or `You will never need to run the kind of code it doesn't allow.'

 

[Joe Marshall]

No, for christ's sake! There are dynamically typed programs that you
cannot translate into statically typed ones!

You are really going to confuse the static typers here. Certainly
there is no program expressable in a dynamically typed language such
as Lisp that is not also expressible in a statically typed language
such as SML.

But it *is* the case that there are programs for which safe execution
*must* depend upon checks (type checks or pattern matching) that are
performed at run time. Static analysis will not remove the need for
these.

It is *also* the case that there are programs for which safe execution
requires *no* runtime checking, yet static analysis cannot prove that
this is the case.

A static analyzer that neither inserts the necessary run-time checks,
nor requires the user to do so will either fail to compile some correct
programs, or fail to correctly compile some programs.

I think the static typers will be agree (but probably not be happy
with) this statement: There exist programs that may dynamically admit
a correct solution for which static analyzers are unable to prove that
a correct solution exists.

 

[Garry Hodgson]

With lisp, you only add as much type checking as you need, *when* you
need it.

if you knew how much you needed and when, you wouldn't need it.

 

[Pascal Costanza]

You are really going to confuse the static typers here. Certainly
there is no program expressable in a dynamically typed language such
as Lisp that is not also expressible in a statically typed language
such as SML.

Yes, of course. Bad wording on my side.

Thanks for clarification.

I am not interested in Turing equivalence in the static vs. dynamic
typing debate. It's taken for granted that for every program written in
either kind of language you can write an equivalent program in the other
kind of language. I seriously don't intend to suggest that dynamically
typed languages beat Turing computability. ;-)

I am not interested in _what_ programs can be implemented, but in _how_
programs can be implemented.


Pascal

 

[John Thingstad]

Pascal

Do you ever do any real work? Or do you spend all your time constructing
replies here...

 

[Kees van Reeuwijk]

[This whole discussion is entirely due to a mismatch of our notions of
what constitutes expressive power.]

No, it is due to your desire to be type constrained inappropriately
early in the development process. Lispers know that early on,

That's very arrogant. You presume to know what is appropriate for *him*.

And I could retort with ``Static typers know that even early in the
development process it is appropriate to have the additional safety that
static typing brings to a program'', but I won't, since I'm not that
arrogant .

 

[Henrik Motakef]

Do you ever do any real work? Or do you spend all your time
constructing replies here...

Proves the point about programmer efficiency, eh? Use Lisp, and you
too can spend most of the day posting to Usenet! ;-)

 

[Dave Brueck]

Do you ever do any real work? Or do you spend all your time

Proves the point about programmer efficiency, eh? Use Lisp, and you
too can spend most of the day posting to Usenet! ;-)

Because you're unemployed? ;-)

 

[Dirk Thierbach]

I have trouble swallowing claims like `It is never wrong, always
completes, and the resulting code never has a run-time error.'

I can understand this. Fortunately, you don't have to swallow it,
you can verify it for yourself.

A comprehensive book about the lambda calculus should contain the
Hindley-Mindler type inference algorithm. The HM-algorithm is fairly
old, so I don't know if there are any papers on the web that explain
it in detail. Unification of types and the HM-algorithm together are
maybe two pages.

* Termination is easy to verify; the algorithm works by induction on
the structure of the lambda term.

* For "it never has a runtime error" look at the typing rules of
the lambda calculus and convince yourself that they express the
invariant that any function (including "constants", i.e. built-in
functions) will only be applied to types that match its own
type signature. Hence, no runtime errors.

A good book will also contain the proof (or a sketch of it) that
if the HM-algorithm succeeds, the term in question can indeed by
typed by the typing rules.

* For the other case (i.e., there is a mismatch during unification; I
guess that's what you mean by "it is never wrong"), try to assign to
every variable a value of the type under the current type
environment, and reduce along every possible reduction path of the
subterm. One of those reductions will fail with a type error (though
this reduction may never happen if execution never reaches this part
of the subterm on the path that the evaluation strategy of your
language chooses).

Maybe it's best to do this for a few examples.

or `You will never need to run the kind of code it doesn't allow.'

The last point should show that such a code at least is problematic,
unless you can somehow make sure that the part that contains the
type error is never executed. In that case, this part is useless,
so the code should be probably rewritten. At least I cannot think
of a good reason why you would "need" such kind of code.

- Dirk

 

[Joachim Durchholz]

I certainly don't mind as much static checking as possible. I get a
little put off by *any* annotations that are *absolutely necessary*,
though. My preference is that all `lexically correct' code be
compilable, even if the object code ends up being the single
instruction `jmp error-handler'. Of course I'd like to get a
compilation warning in this case.

Then static typing is probably not for you.
Mainstream FPLs tend to require an occasional type declaration. And
you'll have to know about the type machinery to interpret the type
errors that the compiler is going to spit at you - never mind that these
errors will always indicate a bug (unless one of those rare explicit
type annotations is involved, in which case it could be a bug or a
defective type annotation).

I believe you. I have trouble swallowing claims like `It is never
wrong, always completes, and the resulting code never has a run-time
error.' or `You will never need to run the kind of code it doesn't allow.'

This kind of claim comes is usually just a misunderstanding.
For example, the above claim indeed holds for HM typing - for the right
definitions of "never wrong" and "never has an error".

HM typing "is never wrong and never has a run-time error" in the
following sense: the algorithm will never allow an ill-typed program to
pass, and there will never be a type error at run-time. However, people
tend to overlook the "type" bit in the "type error" term, at which point
the discussion quickly degenerates into discourses of general correctness.
Adding to the confusion is the often-reported experience of functional
programmers, that annotating your code with static type declarations can
be a very efficient way to finding design errors soon.
The type correctness claims are backed by hard theory; the design
improvement claims are of a social nature and cannot be proved (they
could be verified by field studies at best).

 

[Stephen J. Bevan]

These are both all or nothing solutions.

+ "all the tests for a particular feature in one place" - maybe that's
not what I want (and you have ignored my arguments in this regard)

and:
+ what if I want to run _some_ of the tests that my macro produces but
not _all_ of them?


Actually, that seems to be the typical reaction of static typing
fans.

The solutions may be all or nothing but IMHO they are simple and I
like simple things. I can't really say the same for scenarios which
involve running only some tests generated by macros that may or may
not be in the same files as other tests generated from the same
macros. Perhaps it all comes down to different approaches to the
programming process rather than languages per se, e.g. I don't do
either of the above even when writing Common Lisp.

 

[Stephen J. Bevan]

Are these algorithms reason enough to have machine word sized
numerical data types as the default for a _general purpose_ language?

I've no idea, I don't care that much what the default is since I
prefer to specify what the type/size should be if the compiler fails
to infer the one I wanted

 

[Jacques Garrigue]

This is simply not true. See above.

OK, let's try to distill this to some simple questions.

Assume you have a compiler ML->CL that translates an arbitrary ML
program with a main function into Common Lisp. The main function is a
distinguished function that starts the program (similar to main in C).
The result is a Common Lisp program that behaves exactly like its ML
counterpart, including the fact that it doesn't throw any type errors at
runtime.

Assume furthermore that ML->CL retains the explicit type annotations in
the result of the translation in the form of comments, so that another
compiler CL->ML can fully reconstruct the original ML program without
manual help.

Now we can modify the result of ML->CL for any ML program as follows. We
add a new function that is defined as follows:

(defun new-main ()
(loop (print (eval (read)))))

(We assume that NEW-MAIN is a name that isn't defined in the rest of the
original program. Otherwise, it's easy to automatically generate a
different unique name.)

Note that we haven't written an interpreter/compiler by ourselves here,
we just use what the language offers by default.

Furthermore, we add the following to the program: We write a function
RUN (again a unique name) that spawns two threads. The first thread
starts the original main function, the second thread opens a console
window and starts NEW-MAIN.

Now, RUN is a function that executes the original ML program (as
translated by ML->CL, with the same semantics, including the fact that
it doesn't throw any runtime type errors in its form as generated by
ML->CL), but furthermore executes a read-eval-print-loop that allows
modification of the internals of that original program in arbitrary
ways. For example, the console allows you to use DEFUN to redefine an
arbitrary function of the original program that runs in the first
thread, so that the original definition is not visible anymore and all
calls to the original definiton within the first thread use the new
definition after the redefinition is completed. [1]

Now here come the questions.

Is it possible to modify CL->ML in a way that any program originally
written in ML, translated with ML->CL, and then modified as sketched
above (including NEW-MAIN and RUN) can be translated back to ML? For the
sake of simplicity we can assume an implementation of ML that already
offers multithreading. Again, for the sake of simplicity, it's
acceptable that the result of CL->ML accepts ML as an input language for
the read-eval-print-loop in RUN instead of Common Lisp. The important
thing here is that redefinitions issued in the second thread should
affect the internals of the program running in the first thread, as
described above.

You have an interesting point here, but it is only partly related to
static typing. It is more about static binding vs. dynamic binding.
That is, are you able to dynamically change the definition of any
identifier in the language.
One must recognizes that dynamically typed systems, in particular Lisp
and Smalltalk, also give you full dynamic binding, and that this is an
incredibly powerful feature, at least for developpers.

Now, would it be possible to do it in a statically typed language?
I don't see why not. Some parts are relatively easy: allowing you to
change function definitions, as long as you don't change the type. I
say only relatively, because polymorphism may get in your way: you
would have to replace any polymorphic function by a function at least
as polymorphic as it, whether this polymorphism is really needed by
the rest of the program or not.

Some parts are much more difficult: how to change the data
representation dynamically. This is already difficult in dynamically
typed language (you must introduce lots of kludges to convert the data
on the fly, probably on an as-needed basis), but in a statically typed
language this must be expressed at the level of types. Matthias'
argument would be that anyway you need to do some formal reasonning to
prove that, knowing the dataflow of your program, you have indeed
introduced all the needed conversions and kludges in you dynamically
typed program, and that this reasonning could be converted to some
kind of types, but this is going to be very hard. The most I know
about this is some work on data versionning, but it doesn't consider
modifications inside a running program.

I'm willing to concede you the point: there may be applications where
you want this ability to dynamically modify the internals of your
program, and, while knowing this is just going to be damned dangerous,
a fully dynamic (both types and binding) language is your only way to
be sure that you will be able to do all and every possible changes.
But these applications strike me as being of the high availability
kind, so that the very fact this is so dangerous may be a major
concern.

On the other hand, in the huge majority of cases, this feature is only
used during program development, and once you're done you compile and
optimize, and optimizing actually means loosing most of the dynamic
binding to allow inlining.
In those cases, clever statically typed languages like ML compensate
for their staticness in various ways, for instance by allowing
efficient separate compilation as long as interfaces do not change.
You may have to restart your program, but do not loose much time for
that. And since more bugs are caught by the type system, the need to
correct them is less frequent. You are also provided with an
interactive toplevel, which lets you change some of the definitions at
runtime, at least those functions and variables you have explicitly
declared as mutable. Static typing does not prevent you from running
and modifying interactively a GUI application, it just restricts the
extent of the modifications you can do.

(Contrary to Matthias I'm a purely static guy, but I've always been
attracted by those fancy dynamic development environments.)

 

[Daniel C. Wang]

I think the static typers will be agree (but probably not be happy
with) this statement: There exist programs that may dynamically admit
a correct solution for which static analyzers are unable to prove that
a correct solution exists.

Agreed. However, if you allow the programer to explicitly guide the static
analyzers with hints. I think that set of correct programs that are
provablely correct under with a static analyzer and explicit programer
hints, is very small.

Type inference and type checking are different things. Inference will always
be incomplete or undecidable in ways that are probably quite annoying. Type
checking maybe be incomplete, but no more incomplete than modern
mathematics.

 

[Matthias Blume]

[ ... ]

Thanks for the detailed reply, Jacques! (I was contemplating a reply
of my own, but I think I have to start behaving again and cut down on
the time I waste on netnews.

(Contrary to Matthias I'm a purely static guy, but I've always been
attracted by those fancy dynamic development environments.)

Do you mean that you don't have any dynamically typed skeletons in
your closet? My excuse is that I have been attracted by the static
side of the force all along, but for a long time I didn't understand
that this was the case...

Matthias

 

[Raffael Cavallaro]

I can get behind that idea! It strikes me as being better
than what one has now with either statically typed
languages or dynamically typed languages.

Then the addition of parameterized types to goo, might interest you.

<http://www.csail.mit.edu/research/abstracts/abstracts03/dynamic-languages/03knight.pdf>

Also see the main goo page:
<http://www.ai.mit.edu/~jrb/goo/>