On Mon, May 16, 2016 at 7:45 AM, Koos Zevenhoven <k7hoven@gmail.com> wrote:

On Mon, May 16, 2016 at 4:57 AM, Guido van Rossum <guido@python.org> wrote:
[...]
> unions in Python are always tagged (since you can always introspect the object type).

I suppose that is true at runtime, at least if the pairwise
intersections of the "arguments" of the union are empty as they
usually are. But for a static type checker, the "tag" for the Union
may be missing (which is the thing I was worried about).

Have you thought about how a type checker works? *Of course* the tags are "missing" for it. When it sees that an argument (e.g.) is a union it has to type check the following code with the assumption that it can be any of those types. (However certain flow control using isinstance() can refine this knowledge, like the "if isinstance(...)" example I've given before; also "assert isinstance(...)" has a similar effect.

When a type checker like mypy has a variable that it knows to be a str, and this variable is passed to a function whose signature is (Union[str, bytes]) -> Union[str, bytes], then the result has to be assumed to be the given union, because such a signature does not guarantee that the return type matches the input type. (E.g. if I had a function that turned bytes into str and str into bytes, this could be its signature!)

For this reason, the type variable AnyStr exists, and the mechanism of constrained TypeVars that makes AnyStr possible -- you can make your own type variables with such behavior too.

[...]
> in Haskell as in PEP 484, Sum types and generics are pretty much orthogonal
> concepts.

Although the parametrization provided by generics make TypeVars more
powerful for annotating functions that deal with the equivalent of sum
types.

Yeah, it's not uncommon for two orthogonal features to combine into something even more powerful like that. It's like Hydrogen plus Oxygen... :-)

--Guido van Rossum (python.org/~guido)