Hacker News Reader

Comment by samatman | Hacker News Reader

I wonder if a linter can be constructed, such that Python type hints can be statically divided into "will halt" and "yeah, maybe not", such that the latter category has effectively no type hints found in code not targeted directly at such shenanigans.

I bet it could.

View on HN

Python's type hints are undecidable. You cannot know, without evaluating the type-level program if it will halt.

The only way around this would be to set a recursion depth, which changes the semantics.

But you can do some static analysis on it. There is most likely a very common set of patterns known to terminate, a rare-but-expected set of patterns known to never terminate, and an infinite set of rare patterns which is unknown.

Rust is doing basically the same thing. Default code is "safe", and the compiler is able to prove its correctness. If the compiler can't make heads or tails of it, you have to put it in "unsafe" - and the programmer is expected to check the correctness herself.

That is true in general, yes.

This is also true of Python, but a program which is just `print("hi!")` can be statically proven to halt.

I suspect this is true of a very great majority of type hints in Python which actually exist.

But you can know if it has halted. And if you're a linter, you know how long it took to halt last time. So you can keep track of the times and if it goes from 200ms to 210ms to to 215ms to 10s-and-counting you can let the user know that something significant has changed without being sure that it won't halt any second now.

Reply on news.ycombinator.com