[Python-ideas] Proposal: Use mypy syntax for function annotations

[Andrew Barnert]

On Aug 22, 2014, at 22:13, Steven D'Aprano <steve at pearwood.info> wrote:

> I can't speak for the author of mypy, Jukka Lehtosalo, but for me, I 
> think the answer is that type declarations make a *mini-language*, not 
> full-blown Python. It is unclear to me just how powerful the type 
> language will be, but surely we don't expect it to evaluate arbitrarily 
> complex Python expressions at compile time? Do we?
> 
> I find it unlikely that we expect a static linter to make sense of this:
> 
> def bizarre(param:int if random.random() > 0.5 else str)->float:
> 
> except to say it returns a float and takes who-knows-what as argument. 
> An extreme case, I grant, but I expect that there are going to be limits 
> to what can be checked at compile time based on static analysis. I admit 
> that I don't fully understand all the implications of static versus 
> runtime type checking, but it doesn't seem unreasonable to expect static 
> declarations to be considerably simpler than what can be expressed at 
> runtime. Hence, a simpler mini-language is appropriate.

I agree.

Trying to make the declarative type system more powerful is possible, but probably not a good idea. Look at C++98's template system. It's a complete compile-time language for defining types declaratively (in terms of other types, integer literals, and pointer literals), except that it's missing the ability to recursively decompose recursive types (like a compile-time cons). While that sounds nice in theory, in practice it's painful to use, and completely different from programming in C++. That's what happens if you take a declarative type system and try to expand it until it's fully general: you end up with a type system that looks like ML instead of your language.

C++14 lets you use almost the entire runtime language for computing at compile time (no goto or try, some limits on inheritance) with constexpr values and functions. You can always use the declarative language, but you can also write complex stuff imperatively, in a way that looks like C++. 

If we really need something as powerful as ML or Haskell for our compile-time type system, the latter would be the way to do it. And if this obviously takes too much effort to be worth doing, that means we probably don't actually need the former either.

So, trying to extend MyPy's declarative system to be fully general probably isn't worth doing.

>> Really, for it to be powerful enough, the type description system has to 
>> use its own set of classes. It can't try to hack away existing builtins 
>> and ABCs in the hope of expressing different things with them, or it 
>> *will* hit a wall some day (and, IMO, sooner rather than later).
> 
> How powerful is "powerful enough"? Powerful enough for what?
> 
> You've probably heard of the famous "the compiler found my infinite 
> loop", where the ML type checker was able to detect that code would 
> never terminate. I find that remarkable, and even more astonishing that, 
> according to some, solving the halting problem is "nothing special" for 
> type systems.[2] But many languages make do with less powerful type systems, 
> and tools such as IDEs and editors surely don't need something that 
> powerful. So:
> 
> - how powerful do we expect the type system to be?
> 
> - and how much of that power needs to be expressed using 
>  function annotations?
> 
> The second question is critical, because there are alternatives to 
> function annotations: decorators, docstring annotations, and external 
> stub files.
> 
> 
> 
> 
> [1] Although if you do so, it is not clear to me how much the static 
> checker will be able to use it.
> 
> 
> [2] http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/
> 
> 
> -- 
> Steven
> _______________________________________________
> Python-ideas mailing list
> Python-ideas at python.org
> https://mail.python.org/mailman/listinfo/python-ideas
> Code of Conduct: http://python.org/psf/codeofconduct/