[Types-sig] A late entry

[scott]

On Tue, Mar 14, 2000 at 05:54:52PM -0500, John Viega wrote:
> Whoops.  For me, this has always been an area of interest, but I
> completely missed the fact that people were actually discussing stuff
> here now, until the DC PIGgies meeting last night.  Here are my
> comments so far on what I've seen on the type sig.  Unfortunately, I
> haven't read much of what's been said, so I'm sorry if some things
> have been discussed or are not appropriate.  I've tried to at least
> read or skim the proposals on the list web page.

It's great to see a post from you here.  I know you've studied this
stuff and can offer valuable insights.

> 
> Here I'm going to mainly focus on Guido's proposal, since it seems to
> be one of the more recent proposals, incorporating select ideas from
> other proposals.
> 
> Let's start with some notes on terminology.  I've seen the word
> "typesafe" thrown around quite a bit in a short period of time.  Let's
> try to avoid using the word casually here, because it can lead to
> confusion. I find people often don't know what they're refering to
> when they use (or hear) the term.  Does it mean that no type errors
> can ever happen at run time?  At all?  Or that they can only happen
> under specific conditions?  If so, what are those conditions?
> Cardelli would probably say that "safe" means that the error won't
> cause a crash or go unnoticed at runtime (not everyone agrees with his
> definitions).  By his definition, Python is already a type safe
> language.  However, I often hear people who use the term to mean
> static type safety... i.e., no type error will happen at run time.
> There's essentially no practical hope for that in an object oriented
> language like python.
> 
> I think it might be nice for us to agree to share a common
> terminology.  I know there's a bit of dissention w/ Cardelli's
> prefered terminology, but it at least provides us with a common
> reference in a field where terminology tends to be very muddled.  I
> would recommend we all read Section 1 of Cardelli's "Type Systems"
> (it's about 9 pages). I have copies of this paper in ps and pdf:
> 
> http://www.list.org/~viega/cs655/TypeSystems.ps
> http://www.list.org/~viega/cs655/TypeSystems.pdf

neat paper.  any other references to throw at us?
> 
> Oh, one thing that I should mention is that throughout this document I
> assume an inline syntax for type checking.  I far prefer it.
> 
> Okay, next I want to talk about the way that "checked" and "unchecked"
> modules interact in Guido's proposal.  He says that when an checked
> module imports and uses an unchecked module, all the objects in the
> unchecked module are assigned the type 'any' for the purposes of the
> checking.  I am not 100% sure that's the best idea in the face of type
> inference.  The checked module deserves type information that's as
> specific as possible, so that better types can be infered for the
> checked program.  Of course, in many situations a type inference
> engine isn't going to be able to infer much more than "any" when there
> are absolutely no type hints in the code.  But if something can be
> done, why not?
> 
> The flip side of the coin is that after the type checking occurs, the
> unchecked code can exhibit bad behavior, breaking infered invariants.
> For example, let's say some checked code calls foo.bar(), which is
> infered to have the type: integer*integer->integer.  Someone can
> dynamically load a module from unchecked code which replaces foo.bar()
> with a function of type string->integer.
> 
> Options here?  Run-time checks can be added at points where this is
> possible. I don't know if I support runtime checks if they can be
> avoided. Another option is to say that "guarantees" made by the type
> checker only hold if the whole program is checked.  I'm comfortable
> with that (though I am still probably slightly in favor of the
> addition of runtime checks), but I suspect that others will not be.  I
> have the same opinion when it comes to using checked modules from
> unchecked modules.  Guido proposes adding runtime checks.  I might
> prefer not to have them.  Of course, one option is to support both
> options...

When we talk about adding runtime checks, it's a little unclear to me
exactly what is meant.  Are you referring to additional runtime checks
that the existing dynamic type system in python does not provide?  Is
leveraging the existing dynamic type system in this way feasible for
these sorts of checks?  If this is possible, it is one approach I'd
prefer -- there's no performance hit, and nothing that isn't checked.
The only drawback I can see to using the existing system as a fallback
is that it would limit the degree of optimization that is available,
but I believe that's OK.

> 
> I also might disagree with always performing type checking at load
> time (when an unchecked module imports a checked module).  I see new
> type checking features as a static convenience for people who want to
> use it.  Are people going to want to pay a runtime hit when linking
> against checked code when they don't want to check code themselves?  I
> don't think so.
> 
> Arguing against myself again, you can also make a case that this sort
> of dynamic checking is necessary to be able to live up to the promises
> a static checker makes when it "passes" a piece of code.  Guido talks
> about dynamically importing a module and checking to see if the module
> matches the expected signature.  That's certainly true... here's a
> really simple case: let's assume that A imports B, and that A+B were
> fully checked statically, but someone replaced B with C after checking
> and before runtime.  Is it worth performing those extra checks?  The
> static checks have done the best they could, and now, if there are
> gross incompatabilities, we're hopefully going to see an error
> dynamically whether we added extra checks or not (you can certainly
> construct cases where that's not true).  I'd probably say it is worth
> performing those static checks in some less frequent, highly dynamic
> situations, such as when you've got a completely checked application,
> then you import a module that was essentially typed to stdin.
> 
> I think the right answer for Python depends on what the goals are.
> I'm looking for something that will help me find bugs statically that
> traditionally only cropped up at run time, when possible.  Getting
> contraversial, I don't know if I really care about supporting those
> dynamic checks that are only there to support cases in which the
> application is used in ways that subverts the assumptions I made when
> performing the type checking, such as what modules I'd be using in my
> application.  It should be possible to turn all that stuff off, at the
> very least, and just let everything go while completely ignoring type
> information.  Remember, dynamic features in the type system can end up
> slowing down a language...

I agree very much with all these points about checking modules
dynamically.

> 
> Okay, going to the GCD example...  Do we really need to use the "decl"
> keyword alone to indicate that a module has been checked?  I'm fine
> with gcd(3.5,3) throwing a dynamic error if the module is not checked
> (I'd also be fine with it trying to run here, honestly).  But should
> it try to compute the result if I remove the "decl" keyword from the
> file, but still specify types of the arguments to gcd??
> 
> Why does the word "decl" indicate the module is checked?  Just because
> the programmer added the keyword doesn't mean the types he or she
> assigned are even internally consistant.  Is the interpreter going to
> recheck on startup every single time?  It seems like a lot of overhead
> to me.  Plus, if the keyword isn't there, but there's some type
> information, shouldn't we check the types?
> 
> If the type checker is a separate static program, it seems to me that
> things are more natural.  We try to check the inputs to the program.
> If those inputs use other modules, we go and check them, too.  If the
> checking fails (say it's unchecked), then we warn, and can either fail
> or (optionally?) make assumptions (e.g., assign any everywhere) and
> continue.
> 

[ gcd working w/ floats ]

> 
> Next, let's talk briefly about what type inferencing can do.  In
> particular, consider Guido's example where he assumes that the type
> inference algorithm isn't sophisticated enough to handle complex
> types, such as lists.  Let me say that lists are pretty easy to handle
> when doing type inferencing.  Object types can get a tad bit tricky,
> but everything should be doable.  When I have time, I'll ramble a bit
> about what I see as the best approach to implementing a type inference
> engine for Python based on well-known algorithms.

looking forward to the ramblings!

> 
> There's a problem though.  No one has ever been successful at coming
> up with an OO language that successfully integrates all 3 of the
> following:
> 
> 1) Type inferencing
> 2) Subtyping
> 3) principal types
> 
> Currently, you can choose any two (See Jens Palsburg's brief note
> "Type Inference For Objects", which I have at
> http://www.list.org/~viega/cs655/ObjInference.pdf.  BTW, a principal
> type summarizes all possible types of a given piece of code (variable,
> function, etc).  I'd like to capture all 3.  Basically, 'a->'a is the
> principal type of the "identity" function, even though there are
> plenty of valid specific types that will work in a particular context.
> 
> I don't know if we can solve this problem in the general case. I don't
> think it's possible for Python's needs, but I haven't really given it
> too much thought yet.

It seems like you are refering to inferencing as a mechanism which can
both allow the user to denote fewer types and as a means of dealing
with the mixing of unchecked code with checked code.  With regards to
meating the first goal, a very limited kind of inferencing is
possible, where the first assignment to a variable from an expression
of a given type has the same affect as declaring the variable as that
type in the first place.  I think that the former goal of reducing the
number of declarations the programmer must make is attainable with a
mechanism like this, but the latter goal would require a real
inferencing algo.

> 
> A couple of brief thoughts at this point... What should the type
> checker do with infered types?  Place them directly into the code?
> Place them in comments or a doc string so that they have no effect but
> you can see what the checker did and double-check its work?

maybe just print out inferred types if requested and the type checker
is a separate program?

> 
> Also, it might be nice to type code when you don't have access to the
> source.  Should it be possible to specify the types of features in a
> module for which you don't have source (assume it wasn't written with
> checking code)?  If so, how?  An interface definition file?  Then do
> you try to check the byte code to make sure the given interfaces are
> actually valid?
> 
> Here's an issue I haven't seen brought up yet. Consider the following
> function:


[ identity function signature ]

> I think it would be best to be able to say, "the in type is the out
> type, and who cares about the type beyond that".  Parametric
> polymorphism to the rescue... the type could be <a>-><a>, where <a>
> indicates that x can be of any type.  I think the <a> syntax could be
> better (I prefer ML's, which types identity as 'a->'a, but I hear
> there's some resistance to it in this community... I'm going to use 'a
> from now on because it looks more natural to me).  One problem here is
> that it probably isn't going to be possible to infer an accurate
> principal polymorphic type for things in all cases (see above).  I'll
> have to give the worst cases some thought.

The stab I have taken at writing a checker allows this kind of
polymorphism for functions.  It uses ~ instead of '.  Using a prefix
character is something I prefer as well, though I think there are much
more important issues to ponder, so I get on with it :)

> 
> You may have noticed that 'a looks a heck of a lot like the "any"
> keyword proposed by others.  It turns out to be pretty much the same
> thing, except parametrically polymorphic. One thing you can do is
> differentiate between different types (basically buying you
> parameterized functions, but with a much better syntax, IMHO.  Eg:
> 
> def init_dict(key : 'a, val : 'b):
>   global dict : {'a:'b}
>   dict[key] = val
> 
> The proposed alternative is something like:
> 
> def init_dict<a,b>(key: a, val : b):
>   ...
> 
> There seems to be an implication that functions named init_dict will
> need to be instantiated...  That's a kludgy C++-ism... instantiation
> is not necessary for parametric polymorphism.

Correct.  the stab-at-type-checker I wrote does this, and it would be
handy.

> 
> So should the proposed "any" keyword go away?  Unfortunately, no.  The
> difference in semantics between "any" and generic types is that the
> "any" keyword basically forces the program to forego type checks when
> variables involving "any" are involved, which will sometimes be
> necessary.
> 
> An example might clear up the distinction:
> 
> def f(x): # Here, x is infered to be of type 'a, which is currently
>           # the principal type SO FAR.
>   x.foo() # Whoops, we just had to narrow 'a to any object with a "foo"
>           # method.  If x were of type "any", its type would stay the
> same.
> 
> 
> I really hope that people avoid using "any" *always*, but it does need
> to be there, IMHO.
> 
> Another problem that falls out at this point is how to write the type
> of x when we've seen x call "foo".  Do we look at all classes across
> the application for ones with a foo method?  And do we care if that
> solutions precluds classes that dynamically add their "foo" method
> from applying?  Ick.  I'd prefer to avoid the concrete, and infer
> something like:
> 
> << foo: None->'a >>
> 
> Which would read: an object with a field foo of type function taking
> no arguments and returning anything.

Do you think it's ok to require that the programmer declare something
about x in this case?  If something like what you suggest is inferred
there, it seems like a class of errors might slip through that we
might not want to allow to slip.  

> 
> In the following case:
> 
> def f(x):
>   decl i : integer
>   x.foo()
>   i = i + x.bar("xxx")
>   z = x.blah(1,2)
> 
> We would infer the following type:
> 
> <<
>    foo:  None->'a,
>    bar:  string->integer,
>    blah: integer*integer->'b
> >>
> 
> Adding contrained polymorphic types in declarations should be
> possible, even though it'd get messy without some sort of typedef
> statement:
> 
> def add_observer(x : << notify: string->None >> ) -> None:
>     global notify_list: << notify : string->None >>
>     if not notify_list: notify_list = [x]
>     else: notify_list.append(x)
> 
> It'd be nice to be able to do:
> 
> typedef notifyable << notify: string->None >>
> def add_observer(x : notifyable) -> None:
>     global notify_list: notifyable
>     if not notify_list: notify_list = [x]
>     else: notify_list.append(x)

contstrained polymorphism seems to solve lots of more complex static
type issues in clean ways.  Do you know of any references on
implementations for constrained polymorphism?  I'd like to look more
closely at how it's done elsewhere before taking a crack at it myself.

> 
> Ok, back to the OR-ing of types.  The result of such a construct is
> only going to be lots of ad hoc typecase stuff and types that are not
> as precise as they should be (e.g., the
> (string|integer)->(string|integer) example above).  For example,
> consider the following code:
> 
> class a:
>   def foo(self : a, x : integer): ...
> class b:
>   def bar(self : b): ...
> 
> def blah(x : a | b):
>   x.foo(2)
> 
> That code shouldn't pass through the type checker, because there's no
> guarantee that x has a method foo.  The only real solution every time
> you have an OR type is a typecase statement, which is ad hoc and can
> lead to maintainance problems.  I really don't think there should be a
> language construct to support what's really bad programming
> practice... I think that "any" should be the only place in the system
> where types can be that ambiguous.  (To clarify... typecases are
> sometimes necessary, but I think the OR-ing of types is a pretty bad
> idea).

I like the idea of discouraging OR'ing of types as much as possible.
There are two cases where I think it could come in very handy:  first,
if the static type of None is considered a distinct type rather
something like a null type, then there are lots of things that return
or produce type-of(None) OR something else.  Examples are dict.get and
default arguments.   After wrestling with this for a while, I've come
to think that the introduction of a null-type in a static type system
is more manageable for the programmer.  Do you see other ways of
dealing with that or how would you prefer that those things are
handled?  The other case is recursive data types such as trees, where
a node can contain either other nodes or leaves.

> 
> I do, however, support the AND-ing of types.  There's still a minor
> issue here.  Consider the code:
> 
> class a:
>   def foo(self: a, x: integer) -> integer: ...
> class b:
>   def bar(self: b) -> None: ...
> 
> def blah(x:a&b):
>   x.foo()
> 
> This should definitely type check.  However, what are the requirements
> we should impose on the variable x?  Must it inherit both a and b?  Or
> need it only implement the same methods that a and b statically
> define?  I prefer the former.  There's also the option of restricting
> &'s to interface types only, which I think is fine.  BTW, if there
> isn't an interface mechanism in the 1.0 version of the type system,
> people will start defining "interfaces" as such:
> 
> class IWidget:
>   def draw(self: IWidget) -> None: pass
>   def getboundingbox(self: IWidget) -> (float*float)*(float*float): pass
> 
> That's okay, but you do want the type checker to be able to
> distinguish between an abstract method and a concrete method.
> Otherwise:
> 
> class Scrollbar(IWidget):
>   pass
> 
> Would automatically be a correct implementation of the IWidget
> interface, even though we failed to define the methods listed in that
> interface (we should be forced to add them explicitly, even if their
> body is just a "pass").  I'd much rather the above give an error.  I
> think that special casing classes with no concrete implementations
> isn't that good an idea, so an "interface" keyword should be
> considered, which would look the same as classes without the method
> bodies, and with the restriction that interfaces cannot inherit
> classes (though it's desirable for classes to inherit interfaces,
> obviously).  I wonder if it would be good to also pull out the
> explicit self parameter.

I think it's a good idea to pull out the self parameter.  It makes
interfaces things that are more flexible and not constrained to class
methods being the only callable attributes.

> 
> 
> Eg:
> 
> interface IWidget:
>   def draw() -> None
>   def getboundingbox() -> (float*float)*(float*float)
> 
> I think it would be good to allow parameter-based method overloading
> for people who use the type system.  You'd be allowed to do stuff like:
> 
> class Formatter:
>   def print(self: Formatter, i : integer)->None: ...
>   def print(self: Formatter, s : string)->None:  ...
>   def print(self: Formatter, l : ['a])->None: ...
> 
> It would be easy for the compiler to turn the above into something like:
> 
> class Formatter:
>   def $print_integer(self, i)->None: ...
>   def $print_string(self, s)->None: ...
>   def $print_list_of_generic(self, l)->None: ...
>   def print(self, x)->None:
>     typecase x:
>       case i: integer => self.$print_integer(i)
>       case s: string  => self.$print_string(s)
>       case l: ['a]    => self.$print_list_of_generic(l)
> # The following should be implicit, but I'll list it explicitly...
>       default    => raise TypeError
> 
> The $'s above are just some magic to prevent collisions... however
> this is actually implemented is also not very important.  One
> difficulty here is making sure the debugger handles things properly
> (i.e., maps stuff back to the original code properly)...

Having multiple signatures for method overloading is a convenient way
to express the idea.  If such a thing were available to the type
checking engine, it would be fairly easy to use the underlying data
structures to map the overloading of the arithmetic operators, for
example.

> 
> The syntax of typecasing is not too important here. It could be the
> casting syntax proposed elsewhere.  I prefer a real typecase statement
> based on matching as above.  It's more powerful, and easier to read (I
> don't like choosing arbitrary operators).  The problem is what exact
> syntax to use so that you can show types, bind to variables and allow
> for code blocks, while keeping the syntax as consistant with the rest
> of the language and type system as possible.  The colon always
> precedes a code block, but we're using the colon to separate a
> variable from its type, too.  However, don't like:
> case l : ['a] : self.$print_list_of_generic(l)
> Perhaps:
> case ['a] l : self.$print_list_of_generic(l)
> 
> Though that suddenly makes type decls very irregular.  Then there's
> the option of not explicitly assigning to a new variable:
> 
> case ['a] : self.$print_list_of_generic(x)  # note the x
> 
> I think that last one gets my vote, currently.  We can definitely
> figure out the type of x within that block.  If it needs to be used
> outside the block, then people can copy it into a variable if they
> want to preserve the cast:
> 
> decl l : ['a]
> typecase x:
>   case ['a] : l = x
> 
> By the way, note that the two "'a"'s in the above code can be
> different and still work:
> 
> decl l : ['whatever]
> typecase x:
>   case ['a] : l = x  # This is okay... the types are compatible,
>                      # but now there is an implicit equivolence of
>                      # the 2 types.
> 
> To implement the same kind of matching better functional languages
> provide, we'd need something that allowed for assigning to multiple
> vars at once:
> 
> decl z : integer
> typecase a:
>   case (x : integer, y : integer) => z = x + y
>   case (x : integer,)             => z = x
>   case x : integer                => z = x
> 
> I'd like this type of matching, but it's got the too many colon syntax
> problem, since the => is not pythonesque...
> 
> Hmm, what if all types were expressed using :- instead of :?  Yes, :-
> is the assignment operator in one or two languages, but not too many
> people have used those languages:
> 
> decl z :- integer
> typecase a:
>   case (x :- integer, y :- integer) : z = x + y
>   case (x :- integer,)              : z = x
>   case x :- integer                 : z = x
> 
> That's not quite as bad.

With regards to type casing possibly causing the language to slow down
by bringing the static type information into runtime, do you think it
would be reasonable to allow typecasing only on types that are easily
expressible in terms of the existing dynamic type system?  It seems to
me that this approach would save a lot of work, limit the runtime
overhead, and discourage OR'ing all at once. 


> 
> 
> Now, on to variance of arguments.  Contravariance is definitely bad
> IMHO.  Yes, it's a simpler model, and lends itself to type safety
> better, but if you've ever programmed in Sather, you probably know
> that it can get really inconvenient to do really simple
> things. Invariance (aka nonvariance or novariance) is the approach
> taken by C++ and Java.  It usually does pretty well, and is simple to
> implement.  It usually does what you want, and doesn't lead to the
> same runtime type problems covariance does.  However, consider a
> situation like the following:
> 
> class Container: pass
> class LinkedList(Container):
>    def add(self, l :- LinkedList):
>      ...
> 
> class BidirectionalLinkedList(LinkedList):
>    def add(self, l :- ???):
>      ...
> 
> (BTW, I'm going to drop the type of self from here on out, and assume
> that it is always the type of the class in which the method is
> defined.  I don't think there should be a type variable to allow for
> talking about the type of self, such as in the __add__ example in
> Guido's proposal.  Let covariance of parameters do the work... type
> variables can lead to some pretty subtle problems.)
> 
> In the above example, what should the type of l be?  In a
> contravariant language, as the class gets more specific, the
> parameters must get more generic or stay the same.  Therefore,
> implementing BidirectionalLinkedList requires an explicit type cast if
> we want to enforce the natural restriction that you can only add
> another bidirectional linked list on to the end of a bidirectional
> linked list...
> 
> In a covariant language, "BidirectionalLinkedList" would be the right
> answer, and that seems natual.  Choosing to keep your parameter
> invariant is actually fine as well, so you can do:
> 
> class LinkedList:
>   def merge(self, l :- LinkedList):
>     ...
> 
> class BidirectionalLinkedList(LinkedList):
>   def merge(self, l :- LinkedList):
>     ...
> 
> (We don't care whether the parameter is bidirectional or not)
> I'll get back to the problems with this approach in a second.
> 
> Invariance is an answer... the parameter would forever have to be
> LinkedList in all subclasses, but really requires a typecase on the
> parameter, or the clever use of a constrained generic type:
> 
> class LinkedList<T -> LinkedList>: # specifies that the parameter must
> be
>                                    # substitutable with LinkedList.
>    def add(self, l :- T):
>      ...
>    def merge(self, l : LinkedList):
>      ...
> 
> class BidirectionalLinkedList(LinkedList<BidirectionalLinkedList>):
>    def add(self, l):
>      ... # l is of type BidirectionalLinkedList here.
>    def merge(self, l : LinkedList):
>      ...
> 
> I think constrained generic types are good(tm) and should be added.
> This was the approach I was leaning towards last night at the DC
> PIGgies meeting, but I've changed my mind, as, there are some
> reasonable problems with using them here.  If we have a lot of
> parameters of different types that each need to vary, we have to use a
> ton of constrained types.  It can get ugly quickly.  Plus, if we
> wanted to add a feature to a base class that required a covariant
> parameter, we'd have to add a new constrained parameter, which change
> the interface of the class, potentially breaking a lot of code.  I
> think this is bad, and perhaps worse than typecasting, which is
> another solution when you only have invariance.

Have you read about expressing the above with "mytype"?  that is:

interface if_LinkedList:
	def add(self, l :- mytype):
		...
		
class LinkedList(if_LinkedList):
	def add(self, l):
		...

class BiDirectionalLinkedList(LinkedList):
	...

the syntax is fairly simple, and 'mytype' just means the type of
instances of the class that implements the method.
> 
> So what's wrong with covariance?  Here's a common example of the
> problem:
> 
> class Person:
>   def ShareRoom(self, p :- Person)->None:
>     self.room = p.room
> 
> class Boy(Person):
>   pass
> 
> class Girl(Person):
>   pass
> 
> Hmm, the above isn't quite what we want, as the intent is probably to
> keep boys from rooming with girls.  Let's assume we want to allow
> invariant parameters.  We'd have to recode our Boy and Girl classes as
> such:
> 
> class Boy(Person):
>   def ShareRoom(self, p :- Boy)->None:
>     Person.ShareRoom(self, p)
> 
> class Girl(Person):
>   def ShareRoom(self, p :- Girl)->None:
>     Person.ShareRoom(self, p)
> 
> The problem here is that we can now do the following:
> 
> decl p :- Person
> decl g :- Girl
> p = Boy()
> g = Girl()
> g.room = blah
> p.ShareRoom(g)
> 
> The last call there appears type correct... a static type checker will
> say "looks good!" because Person's ShareRoom accepts any person
> object.  At run time, we will dispatch to the Boy's version of
> ShareRoom, which narrows the type, and yields a type error (if we are
> adding dynamic checks).
> 
> One solution is adding anchored types to the language, which is okay,
> but the programmer could still write the above code, and it would
> still be broken.  Anchored types essentially just gives the programmer
> a way to perform the above and get an error on the p.ShareRoom(g) call
> statically, but only if he added additional magic to one of his
> classes.  Anchored types are cool, but I don't think this is the right
> solution for the problem, so I won't cover them right now.
> 
> Meyer's prefered approach is to add a rule that says "polymorphic
> catcalls are invalid".  What's a catcall?  CAT stands for "Changing
> Availability or Type".  In the context of this discussion, a routine
> that is a cat is a routine where the type of the arguments of a
> function vary in a derived class(*).  A catcall is any call to a cat
> method.  A polymorphic catcall is a call to a cat method where the
> target object is polymorphic, which happens in at least 2 cases:
> 
>   1) The object appears in the LHS of an assignment, where the RHS is
>      a subtype of the LHS.
> 
>   2) The object is a formal parameter to a method.
> 
> There might be a third case... I'll have to go look it up.  I don't
> think there is any problem that would make the solution not
> appropriate for Python, though.
> 
> It should be possible to implement this solution, and even do so
> incrementally.  There's another (better, less pessimistic) solution
> called the global validity approach.  The problem with it, IIRC, is
> that the algorithm basically assumes that type checking goes on in a
> "closed world" environment, where you're checking the entire system at
> once.  That probably isn't desirable.  I wonder if there haven't been
> refinements to this algorithm that allow it to work incrementally.
> Therefore, I'd definitely prefer covariance w/ a polymorphic catcall
> rule, assuming that the catcall rule can actually work for Python.

One possible approach to covariance of method parameters is to check
each method of class against all the possible different types of
'self'.  This is what "stick" does, and it finds exactly the cases
where there are type errors.  It does require more checking than a
general rule, and it does add complications to the problem of mixing
checked modules and unchecked ones accross class inheritence, but it
does work.  I'd be interested in any feedback on this approach you
have...

> 
> BTW, return types should be covariant too.
> 
> Syntax for exceptions: If we add exceptions as part of a signature, I
> don't think that I see a good reason to use anything other than
> something similar to Java's "throws" syntax.  I'd add a comma before
> the "throws" for clarity's sake. Here's a right-recursive (LL) grammar
> fragment:
> 
> throws_clause: "," "raises" throws_list;
> throws_list:   identifier more_throws;
> more_throws:   "," throws_list
>                |;
> 
> Example:
> 
> class Client:
>   def getServerVersion(self) -> string, raises ENotConnected, ETimeout:
>       pass
> 
> The problem is that "raises" is a bit wordy.  I just don't like using
> symbols without natural meanings in these situations... who wants to
> be Perl?  *Maybe* a ! would be alright, since there is a very loose
> connection:
> 
> class Client:
>   def getServerVersion(self) -> string ! ENotConnected, ETimeout:
>       pass
> 
> Or perhaps 2 bangs..., but I am really uncomfortable about the
> readability of that syntax for people new to the language.
> 
> Whatever, I'm not too enamored by having exceptions as part of a
> signature.  Part of the reason is variance of exceptions.  I've seen
> cases where people wanted contravariance and it seemed natural.  I
> don't think those situations are all that common, but I do also
> believe that exceptions in signatures can lead to code that is
> massively difficult to maintain as exceptions added to one method end
> up needing to propogate all the way up a call chain through a program.
> You end up with LONG exception lists.  I need to think more about this
> topic, but right now I don't really care whether the programmer
> explicitly lists exceptions on a per-function basis.  The type checker
> can still determine what exceptions don't get caught in the scope of
> what's been checked.  If there is a new build process for static
> checking, it could report all uncaught exceptions at that time
> (probably optionally), and it could dump them to a supplimental file
> when doing incremental checking.  In short, I haven't thought about
> this problem enough recently to say which way I prefer, but I lean
> towards not making exceptions part of signatures.
> 
> Okay, this has been pretty long and rambling, and it's time for me to
> stop writing.  I'm sorry if I didn't make total sense.  I have more to
> say, but it'll have to wait until another day...

I'm waiting :)

thanks for taking the time to write all this.  

scott


> 
> John
> 
> (*) Changing availability: The catcall rule also applies if a derived
> type also chooses to make a feature unavailable to the outside world
> (e.g., by removing the feature).  No one has been proposing a feature
> of the system to do this sort of thing (yet... but visibility
> mechanisms haven't been discussed much so far as I've seen).  Of
> course, you can always muck around with the attribute directly...
> 
> 
> 
> _______________________________________________
> Types-SIG mailing list
> Types-SIG@python.org
> http://www.python.org/mailman/listinfo/types-sig