[Python-ideas] Type Hinting Kick-off

[Eugene Toder]

On Thu, Dec 25, 2014 at 10:41 PM, Guido van Rossum <guido at python.org> wrote:
> I don't know if this is the main use case (we should ask Jukka when he's
> back from vacation). I'm hesitant to propose more general features without
> at least one implementation. Perhaps you could try to see how easy those
> more general features would be implementable in mypy?
Sounds like a good idea. I'll probably start with a simpler feature, though.

> Neither syntax is acceptable to me, but let's assume we can do this with
> some other syntax. Your example still feels like it was carefully
> constructed to prove your point -- it would make sense in a language where
> everything is type-checked and types are the basis for everything, and users
> are eager to push the type system to its limits.
Andrew pointed below that this is better solved with a union type.

> I assume you're talking about the case where e.g. I have a frozenset of
> Managers and I use '+' to add an Employee; we then know that the result is a
> frozenset of Employees. But if we assume covariance, that frozenset of
> Managers is also a frozenset of Employees, so (assuming we have a way to
> indicate covariance) the type-checker should be able to figure this out. Or
> are you perhaps trying to come up with a way to spell covariance?
Just a quick note: typically, covariance will not help here, because of how
type variables work. Once you have Set[X] with X fixed to Manager, X stays as
Manager. A fresh variable is not inserted into every use of that X. So it will
not get adjusted to Employee in the call to +. OTOH, covariance helps in the
opposite direction -- if Set[Employee] is needed, Set[Manager] will work too.

The real Set cannot be covariant, though, because it supports mutation.

> Eek. That sounds like a bad idea -- copy.copy() uses introspection and I
> don't think there's much hope to be able to spell its type.
Does it really use more introspection than your space_for() function? Naively,
copy is implemented like:

def copy(obj):
    if isinstance(obj, int): return obj
    if isinstance(obj, list): return list(obj)
    ...
    return obj.__copy__()

This does not seem very hard to type. There are much simpler examples, though:

a) Keys of Dict and elements of Set must be Hashable,
b) To use list.index() list elements must be Comparable,
c) Arguments to min() and max() must be Ordered,
d) Arguments to sum() must be Addable.

So it's not uncommon to have generic functions that need restrictions on type
variables.

> That sounds like an artificial requirement on the implementation designed to
> help the type checker.
Perhaps I'm not explaining this right. The requirement is not for the type
checker, it is to be able to implement the function. As you pointed out
earlier, without any requirements on the type the function will not be able to
produce the value.

> Peter Norvig mentioned that the subtleties of co/contra-variance of generic
> types in Java were too complex for his daughter, and also reminded me that
> Josh Bloch has said somewhere that he believed they made it too complex.
IIUC the context for both statements is specifically the call site annotations
of variance, i.e. <?T extends C> and <?T super C>. Though you can also quote
Gilad Bracha, who declared that variance is too complicated notion for
programmers to understand, and made all generics in Dart covariant. This
was also the case in Beta, whose authors denounced invariance and
contravariance, as coming from people "with type-checking background" :-)

> But I can see a serious downside as well. There will likely be multiple
> tools that have to be able to read the type hinting annotations, e.g. IDEs
> may want to use the type hints (possibly from stub files) for code
> completion purposes. Also someone might want to write a decorator that
> extracts the annotations and asserts that arguments match at run time. The
> more handy shorthands we invent, the more complex all such tools will have
> to be.
I think if these tools cannot use functions from the typing module they will
have bigger problems than shorthands. And the number of shorthands is pretty
limited -- there are only as many literals in Python.

> How complex does it really have to be? Perhaps Name[Name, Name, ...] is the
> only form (besides a plain Name) that we really need?
Andrew's type of set.union is Set[Union[X, Y]], so nested names are possible.
Yes, one can always declare an alias for Union[X, Y], but at that point
using a forward declaration seems cleaner.

> Why don't you install mypy and check for yourself? (I expect it's as you
> desire, but while I have mypy installed, I'm on vacation and my family is
> asking for my attention.)
Will do. Thank you for your replies!


Eugene