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

[Devin Jeanpierre]

On Fri, Aug 22, 2014 at 10:13 PM, Steven D'Aprano <steve at pearwood.info> wrote:
> 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.
--snip--
> [2] http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/

You seem to be mischaracterizing ML's type system as something
magically powerful. The ML type checker can be implemented in a few
dozen lines of Python code, and resolved efficiently. ML does type
inference by looking at the constraints on arguments inside the body
of a function. Infinite recursion often accidentally results in you
omitting constraints that you didn't meant to. For example, "def
foo(): return foo()" will be straight up marked as not returning at
all, because no additional constraints are placed on the return value,
which can only mean that it recurses infinitely. Many infinite loops
will not be marked, though. It's a type system, not magic.

(The ML type system is actually substantially simpler than anything
one is likely to come up with to describe Python, because ML didn't
have an object system or structural subtyping.)

As for the comment that this is "nothing special", taken literally,
they said something wrong -- solving the halting problem for Turing
complete languages is impossible, static types or no.  The only way
static types can help is by allowing you to define a (sub-)language
that is not Turing-complete. I think they were alluding to the fact
that, counter to many peoples' intuition, creating a type system that
allows you to detect some of the code that halts isn't a matter of
creating a powerful type system. If you add even the simplest type
system to the lambda calculus, poof, now every well-typed expression
can only be "executed" finitely many steps!


As for whether IDEs need to make something complicated enough that it
can positively identify code that does or doesn't halt, I'd leave that
to the IDE folks. C and Java tools do this sort of thing all the time,
for things like detecting dead code. Why shouldn't Python tools? (This
isn't a feature of the type system so much as control flow analysis
under a given type system, so you're right that it doesn't belong in
the types themselves.)

-- Devin