[Types-sig] Sample declarations

[Daniel Wang]

Jeremy Hylton <jeremy@alum.mit.edu> writes:

> >>>>> "GvR" == Guido van Rossum <guido@digicool.com> writes:
> 
>   GvR> In short, it looks (and I am as surprised as you are!!!) like
>   GvR> we will need to agree on the Python type hierarchy before we
>   GvR> can ever hope to agree on any kind of type assertions.  That
>   GvR> is, unless you make the type assertions only deal with the
>   GvR> concrete types.  But that wouldn't be very useful, as there are
>   GvR> lots of cases where you want to express that you accept any
>   GvR> kind of sequence, mapping, file, etc.
> 
> I noodled with an ML-style type inference engine for simple Python
> functions.  One of the problems I remember running into was that most
> operators work for a variety of object types.  If I see an expression
> with a "+" operator, I can't infer a lot about the operands.  Even if
> I know one of the operands is an int, the other operand could be some
> other kind of number.  (I was explicitly ignore an instance with an
> __add__ method.)
> 

To get things like "+" type right, you probably want something like an
"intersection type". 

(* read /\ as "and" *)
val +:   (int * int -> int)
      /\ (float * floa`t -> float) 
      /\ (float * int) -> float
      /\ (int * float) -> float            


Intersection types are probably pushing the envelope for people who consider
ML's type systems confusing.... but they'll solve the problems with "+"

See 
 http://www.cs.cmu.edu/afs/cs/user/fp/www/papers/icfp00.pdf
and
 http://www.cs.cmu.edu/afs/cs/user/fp/www/talks/yale01-talk.ps

which contain some pretty good examples of how intersection types work. 

> It's an interesting problem, because it forces us to consider the
> documentation issue head on.  If you write code that requirs a
> file-like object to have only read and readlines, what name do you
> give that interface?  Other code might reasonably expect the file to
> have read, seek, and tell.  Etc.

I'm all for "object types" i.e. types need not be associated by name. So the
type of an object would just be an "anonymous interface".

> We can write code quickly in Python in part because we don't have to
> decide in advance which methods we want to require -- and we don't
> have to implement every method that a builtin file has when we write a
> class that is a file-like object.


> If we want to add type declarations to argument lists, we need to
> document exactly what the function requires or we need to pick a
> useful set of standard types (supports __getitem__, mapping, mutable
> mapping) and fix all the code that only implements part of a
> particular type.

Anyway, now that I think about how this whole discussion got started.
 i.e. lets avoid the complexity of a "real type system" and just use dynmaic
 checks. I think it's doomed. :) The complexity of a type system is not in
 how you enforce it, but deciding on how to document what you want enforced.
 A langauge of dynamically checked assertions has the same problem. The
 assertion language is just as complicated as a type system.

Someone suggested that one could infer a type by examining the "check"
method of an object. This actually is not as crazy as it sounds. If people
are willing to program in a small subset of Python for implementing checks,
these "behavioral" type checking isn't so crazy an idea. The subset would
have to be a terminating side-effect free subset of python.