[Python-ideas] Structural type checking for PEP 484

[Andrew Barnert]

On Sep 18, 2015, at 10:35, Sven R. Kunze <srkunze at mail.de> wrote:
> 
>> On 18.09.2015 05:00, Steven D'Aprano wrote:
>> I don't think they are all or nothing. I think it is possible to have 
>> incomplete documentation and partial test coverage -- it isn't like you 
>> go from "no documentation at all and zero tests" to "fully documented 
>> and 100% test coverage" in a single step.
> 
> This was a misunderstanding. The "all or nothing" wasn't about "test everything or don't do it at all". It was about the robustness of future benefits you gain from it. Either you have a test or you don't.
> 
> With type annotations you have 40% or 60% depending on the quality of the tool you use. It's fuzzy. I don't like to build stuff on jello. Just my personal feeling here.

Surely gaining 40% or gaining 60% is better than gaining 0%?

At any rate, if you're really concerned with this, there is research you might be interested in. The first static typer that I'm aware of that used a "fallback to any" rule like MyPy was for an ML language, and it used unsafety marking: any time it falls back to any, it marks the code unsafe, and that propagates in the obvious way. At the end of the typer run, it can tell you which parts of your program are type safe and which aren't. (It can also refactor the type safe parts into separate modules, which are then reusable in other programs, with well-defined type-safe APIs.) This sounds really nifty, and is fun to play with, but I don't think people found it useful in practice. (This is not the same as the explicit Unsafe type found in most SML descendants, where it's used explicitly, to mark FFIs and access to interval structures, which definitely is useful--although of course it's not completely unrelated.)

I think someone could pretty easily write something similar around PEP 484, and then display the results in a way similar to a code coverage map. If people found it useful, that would become a quality of implementation issue for static  typers, IDEs, etc. to compete on, and might be worth adding as a required feature to some future update to the standard; if not, it would just be a checklist on some typer's feature list that would eventually stop being worth maintaining.

Would that solve your "40% problem" to your satisfaction?
>> That's one use-case for them. Another use-case is as documentation:
>> 
>> def agm(x:float, y:float)->float:
>>     """Return the arithmetic-geometric mean of x and y."""
>> 
>> versus
>> 
>> def agm(x, y):
>>     """Return the arithmetic-geometric mean of x and y.
>> 
>>     Args:
>>         x (float): A number.
>>         y (float): A number.
>> 
>>     Returns:
>>         float: The agm of the two numbers.
>>     """
> 
> The type annotation explains nothing. The short doc-string "arithmetic-geometric mean" explains everything (or prepare you to google it). So, I would prefer this one:
> def agm(x, y):
>     """Return the arithmetic-geometric mean of x and y.""
What happens if I call your version with complex numbers? High-precision Decimal objects? NumPy arrays of floats?

I know that Steven wasn't expecting any of those, and will probably do the wrong thing (including silently doing something bad like silently throwing away Decimal precision or improperly extending to the complex plane). With yours, I don't know that. I may not even notice that there's a problem and just call it and get a bug months later. Even if I do notice the question, I have to read through your implementation and/or your test suite to find out if you'd considered the case, or write my own tests to find out empirically.

And that's exactly what I meant earlier by annotations sometimes being useful for human readers whether or not they're useful to the checker.
>>> So, I have difficulties to 
>>> infer which parameters actually would benefit from annotating. 
>> The simplest process may be something like this:
>> 
>> - run the type-checker in a mode where it warns about variables 
>>   with unknown types;
>> - add just enough annotations so that the warnings go away.
>> 
>> This is, in part, a matter of the quality of your tools. A good type 
>> checker should be able to tell you where it can, or can't, infer a type.
> 
> You see? Depending on who runs which tools, type annotations need to be added which are redundant for one tool and not for another and vice versa. (Yes, we allow that because we grant the liberty to our devs to use the tools they perform best with.)

The only way to avoid that is to define the type system completely and then define the inference engine as part of the language spec. The static type system is inherently an approximation of the much more powerful partly-implicit dynamic type system; not allowing it to act as an approximation would mean severely weakening Python's dynamic type system, which would mean severely weakening what you can write in Python. That's a terrible idea. Something like PEP 484 and an ecosystem of competing checkers is the only possibly useful thing that could be added to Python. If you disagree, nothing that could be feasibly added to Python will ever be useful to you, so you should resign yourself to never using static type checking (which you're allowed to do, of course).

> Coverage, on the other hand, is strict. Either you traverse that line of code or you don't (assuming no bugs in the coverage tools).
> 
>>> I am 
>>> either doing redundant work (because the typechecker is already very 
>>> well aware of the type) or I actually insert explicit knowledge (which 
>>> might become redundant in case typecheckers actually become better).
>> You make it sound like, alone out of everything else in Python 
>> programming, once a type annotation is added to a function it is carved 
>> in stone forever, never to be removed or changed :-)
> 
> Let me reformulate my point: it's not about setting things in stone. It's about having more to read/process mentally. You might think, 'nah, he's exaggerating; it's just one tiny little ": int" more here and there', but these things build up slowly over time, due to missing clear guidelines (see the fuzziness I described above). Devs will simply add them just everywhere just to make sure OR ignore the whole concept completely.
> 
> It's simply not good enough. :(
> 
> 
> Nevertheless, I like the protocol idea more as it introduces actual names to be exposed by IDEs without any work from the devs. That's great!
> 
> 
> You might further think, 'you're so lazy, Sven. First, you don't want to help the type checker but you still want to use it?' Yes, I am lazy! And I already benefit from it when using PyCharm. It might not be perfect but it still amazes me again and again what it can infer without any type annotations present.
> 
>> def spam(n=3):
>>     return "spam"*n
>> 
>> A decent type-checker should be able to infer that n is an int. What if 
>> you add a type annotation?
>> 
>> def spam(n:int=3):
>>     return "spam"*n
> 
> It's nothing seriously wrong with it (except what I described above). However, these examples (this one in particular) are/should not be real-world code. The function name is not helpful, the parameter name is not helpful, the functionality is a toy.
> 
> My observation so far:
> 
> 1) Type checking illustrates its point well when using academic examples, such as the tuples-of-tuples-of-tuples-of-ints I described somewhere else on this thread or unreasonably short toy examples.
> 
> (This might be domain specific; I can witness it for business applications and web applications none of which actually need to solve hard problems admittedly.)
> 
> 2) Just using constant and sane types like a class, lists of single-class instances and dicts of single-class instances for a single variable enables you to assign a proper name to it and forces you to design a reasonable architecture of your functionality by keeping the level of nesting at 0 or 1 and split out pieces into separate code blocks.

What you're essentially arguing is that if nobody ever used dynamic types (e.g., types with __getattr__, types constructed at runtime by PyObjC or similar bridges, etc.), or dynamically-typed values (like the result of json.loads), or static types that are hard to express manually (like ADTs or dependent types), we could easily build a static type checker that worked near-perfectly, and then we could define exactly where you do and don't need to annotate types.

That's true, but it effectively means restricting yourself to the Java type system. Which sucks. There are many things that are easy to write readably in Python (or in Haskell) that require ugliness in Java simply because its type system is too weak. Restricting Python (or even idiomatic Python) to the things that could Java-typed would seriously weaken the language, to the point where I'd rather go find a language that got duck typing right than stick with it.

You could argue that Swift actually does a pretty good job of making 90% of your code just work and making it as non-ugly as possible to force the rest of the 10% through escapes in the type system (at least for many kinds of programs). But this actually required a more complicated type system than the one you're suggesting--and, more importantly, it involved explicitly designing the language and the stdlib around that goal. Even the first few public betas didn't work for real programs without a lot of ugliness, requiring drastic changes to the language and stdlib to make it usable. Imagine how much would have to change about a language that was designed for duck typing and grew organically over two and a half decades. Also, there are many corners of Swift that have inconsistently ad-hoc rules that make it much harder to fit the entire language into your brain than Python, despite the language being about the same size. A language that you developed out of performing a similar process on Python might be a good language, maybe even better than Swift, but it would be not be Python, and would not be useful for the same kinds of projects where a language-agnostic programmer would choose Python over other alternatives.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-ideas/attachments/20150918/dba8fdcb/attachment-0001.html>