Multimethods 101 (was Re: Multiple dispatch (Re: Q: Python 2.0 preliminary features?))

[Harry Chomsky]

Louis Madon wrote in message <381ACFEF.38E6B1E3 at bigfoot.com>...
>Guaranteed compile time errors on this would certainly be nice.  [BTW, I
>wonder what Cecil does here?  Its statically typed and the compiler does
>whole-program analysis, so perhaps it *can* report this kind of error at
>compile time?].

Yes.  Cecil has both static and dynamic type-checking.  The compiler and
type-checker are two separate beasts that operate independently of one
another, so you can compile and run code even if it doesn't satisfy the
type-checker's rules.  The run-time system does dynamic type-checking when
necessary, and it issues errors in a variety of situations, including
"message ambiguous" (as in the case being discussed in this thread).  The
type-checker's goal is to prove statically that none of those errors will
ever be issued.  It uses whole-program analysis, and it will report an error
in the case being discussed.

(The implementation of the type-checker that you can download is somewhat
limited, and it won't actually report this error.  But the language
designers have described in detail the algorithm that the type-checker
should use.  It just isn't implemented in the current release.)

One of the future goals for Cecil is to allow separate type-checking of
modules.  The designers have some ideas of how to do this; you can read
about them in one of the papers available for download on the site.  But
they've never completely formalized these ideas and they haven't attempted
to implement them yet.  Apparently it is more difficult than they suspected,
and their initial formulation doesn't quite work.  The basic idea is that if
module B introduces new subtypes of a type defined in module A, then module
B must be declared to "extend" module A.  The type-checker will then examine
module A when checking module B.  When modules are linked into a program,
the linker verifies that any two extensions of a module must in turn be
extended by a common module.  E.g., if B and C both extend A, then there
must be another module (say D) that extends both B and C.  B and C may each
type-check successfully, but if together they introduce an ambiguity, the
type-checker will notice that when it checks module D.  I'm probably not
being very clear; see the paper for more details.  I don't know exactly what
troubles they've run into in trying to formalize this.