Python type hints are Turing complete(arxiv.org)
arxiv.org
Python type hints are Turing complete
https://arxiv.org/abs/2208.14755
141 comments
That’s not at all what’s going on here. While the Python interpreter permits and executes arbitrary expressions as annotations, Python static type checkers (mypy, Pytype, Pyre, Pyright) do not. This isn’t just an implementation limitation; the typing specifications (PEP 484 and successors) don’t allow it. For example, although these two definitions evaluate to the same result at runtime:
That’s the whole idea of static type checking: in return for restricting yourself to a controlled subset of the language that isn’t “too dynamic”, you gain the ability to type-check your code without running it.
The result of this paper is that one can nonetheless abuse subtyping to perform Turing-complete computation in the type checker. The computation doesn’t happen when your code is executed (annotations have no effect on the Python interpreter at runtime unless your program chooses to inspect them), it happens when you run mypy on it.
This is generally considered undesirable, because we want type checking to be decidable, and Turing-complete computation is not.
def f() -> int: return 1
def f() -> (lambda: int)(): return 1
That’s the whole idea of static type checking: in return for restricting yourself to a controlled subset of the language that isn’t “too dynamic”, you gain the ability to type-check your code without running it.
The result of this paper is that one can nonetheless abuse subtyping to perform Turing-complete computation in the type checker. The computation doesn’t happen when your code is executed (annotations have no effect on the Python interpreter at runtime unless your program chooses to inspect them), it happens when you run mypy on it.
This is generally considered undesirable, because we want type checking to be decidable, and Turing-complete computation is not.
> That’s the whole idea of static type checking: in return for restricting yourself to a controlled subset of the language that isn’t “too dynamic”, you gain the ability to type-check your code without running it.
Eh, you are mixing up distinctions.
All that's required of _static_ typing is that your static type specification finishes running before you start your program.
Whether that static type specification language is Turing complete or not is a completely separate issue. And, yes, you are right that it's generally useful for that language to be decidable. But see eg Haskell's UndecidableInstances.
Eh, you are mixing up distinctions.
All that's required of _static_ typing is that your static type specification finishes running before you start your program.
Whether that static type specification language is Turing complete or not is a completely separate issue. And, yes, you are right that it's generally useful for that language to be decidable. But see eg Haskell's UndecidableInstances.
That's why my comment litterally starts with "even before talking about the typing system itself".
I’m sure that you understood the important differences, but there are likely many readers who didn’t (many more programmers are familiar with Python than with mypy). When you write “even if we don’t have P, we’d have Q anyway”, the reader is left with the impression that P and Q are somehow interchangeable or equivalent or comparable—that P is unimportant in the presence of Q. I think it’s instructive to point out that this impression would be mistaken, and the paper’s result of P is interesting and consequential.
What other use cases did the community come up with?
Dependency injections, foreign-language bridges, data validation and parsing, etc.
But thanks to how we can introspect annotations, we could have a specialized syntax for types that would be also usable for those things, while the other way around would be harder.
So it's nice we went the type hints road, because you can now define types, and yet have wonderful libs like pydantic, fastapi, typer, taichi and so on.
But thanks to how we can introspect annotations, we could have a specialized syntax for types that would be also usable for those things, while the other way around would be harder.
So it's nice we went the type hints road, because you can now define types, and yet have wonderful libs like pydantic, fastapi, typer, taichi and so on.
Pydantic typing differs from mypy typing. Optional[T] means something different under the two.
I designed typedload before pydantic was a thing and I made it with mypy in mind already, and with the idea of using the standard library, not defining my own dataclass.
Unfortunately mypy has a limitation so you can't make a function that takes Type[T] and returns T. You can define it but it won't work for all types. There is still discussion on how to provide this feature.
I designed typedload before pydantic was a thing and I made it with mypy in mind already, and with the idea of using the standard library, not defining my own dataclass.
Unfortunately mypy has a limitation so you can't make a function that takes Type[T] and returns T. You can define it but it won't work for all types. There is still discussion on how to provide this feature.
Yeah this ones is really annoying with default values.
Cool, any examples of libraries that use it for dependency injection or FFI or validation?
Dependency-injector uses it for exactly this purpose
https://python-dependency-injector.ets-labs.org/introduction...
@inject
def main(service: Service = Provide[Container.service]) -> None:
...
https://python-dependency-injector.ets-labs.org/introduction...
django-ninja and fastapi does dep injection, parsing and validation based on annotations.
taichi does ffi with their own dsl, cython with c.
I you haven't tried pydantic or sister projects (django-ninja, fastapi and typer), this is a good place to start. They bring a breath of fresh air and are quite fun to use.
taichi does ffi with their own dsl, cython with c.
I you haven't tried pydantic or sister projects (django-ninja, fastapi and typer), this is a good place to start. They bring a breath of fresh air and are quite fun to use.
Specifically it's the underlying pydantic that does validation based on annotations
https://pydantic-docs.helpmanual.io/
https://pydantic-docs.helpmanual.io/
Indeed.
The dep injection is fastapi and typer code though, and quite tied to it. So it's worth mentioning that somebody is attempting (quite successfully from the look of it) to create a generic lib of dep injection using annotation named DI, inspired by those libs: https://github.com/adriangb/di
The dep injection is fastapi and typer code though, and quite tied to it. So it's worth mentioning that somebody is attempting (quite successfully from the look of it) to create a generic lib of dep injection using annotation named DI, inspired by those libs: https://github.com/adriangb/di
I always find it very funny that fastapi has that name when it relies on pydantic that is one of the slowest libraries in that space :D
It's not one of those that you listed, but the @dataclass decorator uses type hints to auto-generate classes and class constructors (__init__ method) for you.
An example:
It can do some other things too!
https://docs.python.org/3/library/dataclasses.html
An example:
@dataclass
class HackerNewsPost:
title: str
author: str
votes: int = 0
def __init__(title: str, author: str, votes: int = 0):
self.title = title
self.author = author
self.votes = votes
It can do some other things too!
https://docs.python.org/3/library/dataclasses.html
For FFI, there is a pure python mode in cython:
https://cython.readthedocs.io/en/latest/src/tutorial/external.htmlI used them at runtime to define the types for my (absolutely stupid) library that takes a Python function and replaces its contents with a C call.
You define a Python function interface but populate it with a string of C code.
You define a Python function interface but populate it with a string of C code.
Wait, so like this?
That's...horrifying yet amazing.
def add(x: int, y: int) -> int:
""" // c code
int x, y
return x + y
"""
That's...horrifying yet amazing.
That might be a worthwhile addition to the suggestion at https://github.com/faster-cpython/ideas/issues/453
Combined with the cog (https://nedbatchelder.com/code/cog) to have the c declaration in a proper separate c file, but included in the docstring, you could have the best of both worlds.
That's a neat hack!
There's a library for simulating the Excel calculation engine in Python. It uses annotations to hint functions, but according to Excel's type system, not Python's. Then at runtime, those hints are used to do conversion and promotion based on how Excel does it, so you can do e.g. the equivalent of "1" + 1 and get 2.
It's either xlcalculator or pycel, one of the two. I forgot which one does it that way.
It's either xlcalculator or pycel, one of the two. I forgot which one does it that way.
Looks like it's xlcalculator:
https://github.com/bradbase/xlcalculator#addingregistering-e...
https://github.com/bradbase/xlcalculator#addingregistering-e...
Things like pydantic and fastapi where the type annotations are used for run time argument validation and interface generation.
Does this still work with Python 3.10 changes removing runtime evaluation of type annotations? I seem to recall this screwed me when I was writing something for runtime usage of types.
They postponed that change.
It remained enabled with a future and while it kinda works, it doesn't work in all cases. Non top level definitions can never be retrieved basically.
It remained enabled with a future and while it kinda works, it doesn't work in all cases. Non top level definitions can never be retrieved basically.
There was a heated debate because it broke things at the time, but now it works, yes.
Oh it looks like they actually pushed back the PEP 563 changes..
From this thread [0] it does not look open and shut that it will work once these changes go into effect.
[0]: https://github.com/pydantic/pydantic/issues/2678
From this thread [0] it does not look open and shut that it will work once these changes go into effect.
[0]: https://github.com/pydantic/pydantic/issues/2678
we still don't know what's going to happen with type hints in future though, but I'm sure things won't break as they might have broken if they changed the default behaviour
[deleted]
Creating argument parsers for CLIs: https://pypi.org/project/argtyped/
I've seen similar (in-house) to generate HTML forms also.
I've seen similar (in-house) to generate HTML forms also.
I've created strawberry graphql, it uses type hints to generate GraphQL schemas
I may be misunderstanding this, but it seems like there is a mistake on the first page:
> For example, every string is an object, `str <: object`, but not every object is a string, `str ≮: object`.
Is not
> For example, every string is an object, `str <: object`, but not every object is a string, `str ≮: object`.
Is not
str <: object ∧ str ≮: object
Yes, this is an obvious mistake. What you wrote is the right statement.
I tongue-in-cheek tweeted this, but I was semi-serious. Types end up being Turing-complete all the time: https://twitter.com/TitzerBL/status/1567677824105947136
There has to be a joke in here somewhere: We add a language on top to help us with our problems in the original language.
Would building a DSL in the language give you the same dynamic?
Would building a DSL in the language give you the same dynamic?
Two languages can both be Turing complete, but still be adapted to very different purposes.
> Would building a DSL in the language give you the same dynamic?
The Lisp people did something like that. I can't find it now, alas.
> Would building a DSL in the language give you the same dynamic?
The Lisp people did something like that. I can't find it now, alas.
| Two languages can both be Turing complete
Doesn't this just cause the same problems? If language B (the type system) is Turing complete you'll start doing whatever you don't like doing in language A (the host) and end up with similar problems you had in A, but now in B.
| but still be adapted to very different purposes.
I guess this is what's needed but each should be constrained as to NOT be able to do certain things.
Doesn't this just cause the same problems? If language B (the type system) is Turing complete you'll start doing whatever you don't like doing in language A (the host) and end up with similar problems you had in A, but now in B.
| but still be adapted to very different purposes.
I guess this is what's needed but each should be constrained as to NOT be able to do certain things.
You want an algebra for the bits and an algebra for the functions.
Here's the article rendered as html: https://ar5iv.labs.arxiv.org/html/2208.14755
(Replace the x in arxiv.org with a 5 to get there. I feel like it's working well enough in most cases, when will they start linking these from the actual arxiv article pages?)
(Replace the x in arxiv.org with a 5 to get there. I feel like it's working well enough in most cases, when will they start linking these from the actual arxiv article pages?)
The code is completely unreadable, gray on yellow, for me - seems like there's still work to do
screenshot: https://cdn.billmill.org/static/newsyctmp/pytyping.png
screenshot: https://cdn.billmill.org/static/newsyctmp/pytyping.png
That’s only in dark mode, because they use the default text color.
You must be using Dark Reader or something similar? Page is light mode, and the text darker gray by default for me.
The math typesetting, while not unreadable, is annoying as well. It seems to be using a smaller x-height for math than for text.
Dark mode turned that part of the code to gray text. The default light mode is readable even if the yellow background is a little strange.
It's not like they can code their website for every custom style everyone wants to use on their browser...
Yes, but not making a mess of dark mode is worth criticizing by now.
I don't have a custom style, this is plain jane firefox
I get same on iOS/Safari with my phone in dark mode.
The code is a healthy dark color for me. Totally fine.
Anyone know what they use to convert the PDF to html here? I'm looking for a good converter and so far I've only found a few bad ones.
They aren't using the rendered PDFs. They are convering from the LaTeX sources, that you upload to arxiv with https://github.com/brucemiller/LaTeXML
Surprisingly Turing-Complete: https://www.gwern.net/Turing-complete
I've seen it said that Turing completeness is so prevalent that one often has to intentionally prevent it when designing a system.
on the other hand, technically nothing is turing complete because of lack of infinite memory
> In colloquial usage, the terms "Turing-complete" and "Turing-equivalent" are used to mean that any real-world general-purpose computer or computer language can approximately simulate the computational aspects of any other real-world general-purpose computer or computer language. In real life this leads to the practical concepts of computing virtualization and emulation.[citation needed]
> Real computers constructed so far can be functionally analyzed like a single-tape Turing machine (the "tape" corresponding to their memory); thus the associated mathematics can apply by abstracting their operation far enough. However, real computers have limited physical resources, so they are only linear bounded automaton complete. In contrast, a universal computer is defined as a device with a Turing-complete instruction set, infinite memory, and infinite available time.
https://en.m.wikipedia.org/wiki/Turing_completeness#Non-math...
> Real computers constructed so far can be functionally analyzed like a single-tape Turing machine (the "tape" corresponding to their memory); thus the associated mathematics can apply by abstracting their operation far enough. However, real computers have limited physical resources, so they are only linear bounded automaton complete. In contrast, a universal computer is defined as a device with a Turing-complete instruction set, infinite memory, and infinite available time.
https://en.m.wikipedia.org/wiki/Turing_completeness#Non-math...
Turing completeness is about simulating a Turing machine, not being one.
Touring completeness is about accurately simulating any Turing machine. Not approximately simulating one (what would that even mean?), or simulating just some of them.
When we say something is Turing complete, there’s always an implicit “if it ran on a computer with unlimited memory” assumption that comes with it, because no computer with limited memory can ever simulate all Turing machines. You can always construct a Touring machine that makes a given computer run out of memory.
So technically, no real computer or computer program is Turing complete, or able to accurately simulate any Turing machine. The whole thing is an irrelevant technicality though, as A) we have so much memory available that we might as well treat it as unlimited and B) touring completeness is a theoretical property - if you prove it for something like python type hints, that proof won’t assume any memory limitations, ie. it’ll assume the computer the thing runs on has infinite memory. The proof is valid even though no such infinite computer actually exists.
When we say something is Turing complete, there’s always an implicit “if it ran on a computer with unlimited memory” assumption that comes with it, because no computer with limited memory can ever simulate all Turing machines. You can always construct a Touring machine that makes a given computer run out of memory.
So technically, no real computer or computer program is Turing complete, or able to accurately simulate any Turing machine. The whole thing is an irrelevant technicality though, as A) we have so much memory available that we might as well treat it as unlimited and B) touring completeness is a theoretical property - if you prove it for something like python type hints, that proof won’t assume any memory limitations, ie. it’ll assume the computer the thing runs on has infinite memory. The proof is valid even though no such infinite computer actually exists.
Nah they're technically correct. You can't simulate a Turing machine with finite memory.
To simulate something is not to be something. Simulations are approximations of the thing. What you're implying is that we can't simulate anything, as the simulation can never be the thing. Can we not simulate the weather or the solar system because we can't take into account every possible detail? If your position is that nothing can be Turing complete, than why should anyone care about Turing completeness?
We can simulate a model of the weather. We can simulate (as in completely replicate the software behavior of) a gameboy advanced.
Not going to keep replying as this is not really a point I am going to get convinced of - to be technically turing complete is to show that every thing computable by a turing machine is computable by your construct. This is not possible in a memory constrained system.
Not going to keep replying as this is not really a point I am going to get convinced of - to be technically turing complete is to show that every thing computable by a turing machine is computable by your construct. This is not possible in a memory constrained system.
Appreciate you've bowed out of this discussion, but what you're saying makes no sense to me, because then we would just say things are or are not Turing machines. The reason we have the term "Turing complete" and not just "Turing machine" is precisely the fact that nothing can literally be a Turing machine, and we need a useful term in discussions of computability nonetheless. The analysis as to whether or not a system is Turing complete or not is done with respect to the operations it can perform, not its memory capacity, or even the time over which is performs the operations, both of which are always assumed to be "enough" rather than infinite.
>The reason we have the term "Turing complete" and not just "Turing machine" is precisely the fact that nothing can literally be a Turing machine, and we need a useful term in discussions of computability nonetheless.
a turing machine is something way more specific than just "something that can execute algorithms" though, it's a machine that executes them using a specific system and constraints (namely advancing and modifying a strip of tape). So calling anything that can compute what a turing machine can compute a turing machine would be inaccurate just by merit of that.
of course ultimately you're right though, words mean what they're used to mean, so turing completeness excludes the infinite memory constraint, my initial comment wasn't really meant fully seriously, just being a smartass for a joke.
a turing machine is something way more specific than just "something that can execute algorithms" though, it's a machine that executes them using a specific system and constraints (namely advancing and modifying a strip of tape). So calling anything that can compute what a turing machine can compute a turing machine would be inaccurate just by merit of that.
of course ultimately you're right though, words mean what they're used to mean, so turing completeness excludes the infinite memory constraint, my initial comment wasn't really meant fully seriously, just being a smartass for a joke.
A Turing machine has unbounded tape, not infinite tape.
which effectively means it has infinite memory, does it not?
I don't see a distinction myself between unbounded and infinite, but the Typing system might be unbounded but it's being run on a computer with bounded memory so it becomes bounded. But that isn't a property of the Typing system, it's a property of the environment it's being executed in.
Unless you allow unbounded input there is technically a limit to the amount of memory an N-state Turing machine could possibly allocate (and still halt).
Infinite memory available, but never used.
I'm not at all surprised by this. Accidental Turing-completeness is easy to fall into. Python's type hints take a lot of influence from the likes of, say, Scala, which has a Turing-complete type system, as is Haskell's.
You’re right, it’s amazing how common turing completeness is. Even powerpoint is turing complete. But I just wanted to mention one thing: Haskell’s type system isn’t turing complete unless you have certain extensions on (like UndecidableInstances).
Indeed; Haskell uses an extension of the Hindley-Milner type system, which is decidable, and the extension with type classes doesn't impact decidability.
Yet, Haskell type inference is not necessarily efficient; as noted in [1]
> Hindley–Milner type inference is DEXPTIME-complete. In fact, merely deciding whether an ML program is typeable (without having to infer a type) is itself DEXPTIME-complete. Non-linear behaviour does manifest itself, yet mostly on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community.
[1] https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
> Hindley–Milner type inference is DEXPTIME-complete. In fact, merely deciding whether an ML program is typeable (without having to infer a type) is itself DEXPTIME-complete. Non-linear behaviour does manifest itself, yet mostly on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community.
[1] https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
I wonder if there are type systems that are intentionally Turing-complete rather than accidentally. As in, given that you're likely going to end up with Turing-completeness anyway, why not make type-level programming intuitive and convenient rather than the tarpit it typically is?
> I wonder if there are type systems that are intentionally Turing-complete rather than accidentally.
I’d consider most dependent type systems to be in this category.
I’d consider most dependent type systems to be in this category.
Intersection types are an example where the theory is in its full generality undecidable, and where applications in useful PLs tends to use only low-rank intersection types.
See https://en.wikipedia.org/wiki/Intersection_type_discipline
See https://en.wikipedia.org/wiki/Intersection_type_discipline
Haskell and many related languages certainly don't shy away from trying to make it intentionally Turing-complete. I wouldn't say they have succeeded at making it intuitive quite yet though.
Sure, CLOS was the first that comes to mind.
Shen has a 'static' type system which embeds a predicate calculus, thus being trivially Turing-complete, and not by accident.
Shen has a 'static' type system which embeds a predicate calculus, thus being trivially Turing-complete, and not by accident.
I've been using Python for a very long time.
I can't get used to the Typing features. It makes the code look overly verbose and needlessly explicit. I love the simplicity and cleanliness of Python code, even at the expense of not specifying type hints and all that new jazz.
I can't get used to the Typing features. It makes the code look overly verbose and needlessly explicit. I love the simplicity and cleanliness of Python code, even at the expense of not specifying type hints and all that new jazz.
I'm of two minds. I like most python code to be untyped where types are obvious. But I almost always use them for function signatures, unless they're absurdly trivial. And once I have a collection where it is not a matter of the utmost ease to determine what the contained type is, I add a type hint for that.
Class members, I generally always type. Hmm let me think. That's probably about it.
I extensively use named tuples and dataclasses too which I think also benefit from having as much type info as possible. I think it fills them in nicely given they're already immutable.
My first job - 5 years - was being neck deep in a huge python 2 codebase with dubious historical maintenance and programmer capability track record. I grew to despise enormous List[Dict[Tuple[str, str, str], Tuple[str, str, int]]] except that oopsies! Sometimes that int is a float and sometimes null and sometimes a string and on the last day of the month one of the records will be a custom class that we insert and test for to handle specially.
Also cases where some variable is passed down through multiple call sites without usage and a short name - like "f" - and it's not clear to me if it's a file, an io object, a string holding a filename, or what. I'd like that typed too.
Class members, I generally always type. Hmm let me think. That's probably about it.
I extensively use named tuples and dataclasses too which I think also benefit from having as much type info as possible. I think it fills them in nicely given they're already immutable.
My first job - 5 years - was being neck deep in a huge python 2 codebase with dubious historical maintenance and programmer capability track record. I grew to despise enormous List[Dict[Tuple[str, str, str], Tuple[str, str, int]]] except that oopsies! Sometimes that int is a float and sometimes null and sometimes a string and on the last day of the month one of the records will be a custom class that we insert and test for to handle specially.
Also cases where some variable is passed down through multiple call sites without usage and a short name - like "f" - and it's not clear to me if it's a file, an io object, a string holding a filename, or what. I'd like that typed too.
Same here. I used type annotations before static analyzers became popular, and was quite happy with them (though I would not enforce them). They were a great source of documentation. And yes, like any documentation, occasionally they can deviate from reality.
With static analysis they won't deviate anymore. But the price you're paying for this is verbosity, complexity, and constant support of types.
I find Python static analysis incredibly unpythonic.
With static analysis they won't deviate anymore. But the price you're paying for this is verbosity, complexity, and constant support of types.
I find Python static analysis incredibly unpythonic.
Disclaimer: what I'm about to say has resulted, in the past, in someone on HN harassing me in a conversation of 30+ nested depth levels, and his line of attack was basically alternating between "you don't understand type hints" and "what is your company optimizing for, anyway?".
So before I say this, let's agree nobody will harass anybody, and we will politely disagree on this.
Ok, disclaimer done. Here's what I got to say:
I find Python type hints unsatisfying because they don't do enough. Existing type checkers that use them have limitations, are difficult to use beyond trivial usage, and fail to detect cases which are trivial for statically typed languages. Because of this, you never feel truly safe or covered because you're using them, so writing type hints seems like wasteful effort that is difficult to justify to skeptical Python developers.
However, simply saying "it's not enforced, it's just documentation" is also unsatisfying to me. Computers should work for us; if they can automate and enforce something, we should let them. This feels like the worst of both worlds: it's unenforced, slowly-drifting documentation (so the language does very little work for you) but it lacks the freeform of other documentation styles, and you must follow a formal syntax. And developers don't like writing it, since it does nothing anyway.
So before I say this, let's agree nobody will harass anybody, and we will politely disagree on this.
Ok, disclaimer done. Here's what I got to say:
I find Python type hints unsatisfying because they don't do enough. Existing type checkers that use them have limitations, are difficult to use beyond trivial usage, and fail to detect cases which are trivial for statically typed languages. Because of this, you never feel truly safe or covered because you're using them, so writing type hints seems like wasteful effort that is difficult to justify to skeptical Python developers.
However, simply saying "it's not enforced, it's just documentation" is also unsatisfying to me. Computers should work for us; if they can automate and enforce something, we should let them. This feels like the worst of both worlds: it's unenforced, slowly-drifting documentation (so the language does very little work for you) but it lacks the freeform of other documentation styles, and you must follow a formal syntax. And developers don't like writing it, since it does nothing anyway.
I agree that it's unsatisfying when compared to a statically typed language. There's a time and place for those. But the ability to use it only where it actually adds value--like at an API boundary where you don't know who will be calling your function but you want to help their IDE help them--that's pretty cool.
The problem is justifying type hints to skeptical developers with no experience from either world.
Coming from the statically typed world, I struggled to justify type hints to inexperienced devs who saw all the holes in them, and so they simply refused. I had no authority to enforce anything, and in any case, enforcing by mandate is not ideal.
So I wish type hints were better so that my arguments for them could be more solid.
Coming from the statically typed world, I struggled to justify type hints to inexperienced devs who saw all the holes in them, and so they simply refused. I had no authority to enforce anything, and in any case, enforcing by mandate is not ideal.
So I wish type hints were better so that my arguments for them could be more solid.
I've had a lot of luck with:
"ok now type g... wait, why isn't get_foo autocompleting for you? Hold on, lets go add a hint..."
I realize that you're not going to piecemeal your way to satisfying mypy output like this, but I think it plants the seed in a way that prevents the mentor from being the type-cops.
"ok now type g... wait, why isn't get_foo autocompleting for you? Hold on, lets go add a hint..."
I realize that you're not going to piecemeal your way to satisfying mypy output like this, but I think it plants the seed in a way that prevents the mentor from being the type-cops.
The API is where type hints should absolutely be mandatory for any serious project in my opinion, and my company has adopted this stance for all new code being written.
Even then, I still fully type all of my code because it lets me write fewer tests.
Even then, I still fully type all of my code because it lets me write fewer tests.
The types that let you write fewer tests are the types that work consistently and are sufficiently enforced by the tooling; sadly, not the kind type hinting that Python has ;)
I think I can do a healthy disagreement without harassment.
> Computers should work for us; if they can automate and enforce something, we should let them
I agree. But in my experience type hints are often treated as a goal, not as a low cost solution. "We're not going to compromise on type safety". Same happens in TypeScript ecosystem.
As you correctly mentioned, Python type hints are somewhat limited. So naturally what happens next is people change the way they write code to work around those limitations. Readability and velocity (major things Python is praised for) gets sacrificed for the sake of "type safety".
The promise was for tooling to correct my mistakes. But more often than not I felt that I have to correct tooling mistakes.
Before mypy became popular, I often used type annotations because I wanted to. I didn't use them everywhere, I wouldn't enforce them in code reviews, I would never use deeply nested types (those are just unreadable) or generics. I was able to extract value from type hints, they gave me 80% of value for 20% of effort. Static analysis feels like it tries to get another 10% of value for 90% of cost. It's not a good deal anymore.
> Computers should work for us; if they can automate and enforce something, we should let them
I agree. But in my experience type hints are often treated as a goal, not as a low cost solution. "We're not going to compromise on type safety". Same happens in TypeScript ecosystem.
As you correctly mentioned, Python type hints are somewhat limited. So naturally what happens next is people change the way they write code to work around those limitations. Readability and velocity (major things Python is praised for) gets sacrificed for the sake of "type safety".
The promise was for tooling to correct my mistakes. But more often than not I felt that I have to correct tooling mistakes.
Before mypy became popular, I often used type annotations because I wanted to. I didn't use them everywhere, I wouldn't enforce them in code reviews, I would never use deeply nested types (those are just unreadable) or generics. I was able to extract value from type hints, they gave me 80% of value for 20% of effort. Static analysis feels like it tries to get another 10% of value for 90% of cost. It's not a good deal anymore.
Thanks for the reply. I think we actually agree on this, only coming from different sides.
As an aside, if this is the disclaimer you give out before saying your opinion on Python type hints... how do you handle dishing out your political views or other more serious matters?
I expect opposition when discussing political topics.
I wrote this disclaimer because I was surprised to find harassment for such a harmless topic as Python's type hinting. I'm surprised dang never stepped in. The flamewar went for a surreal nesting depth, and you know what goes on at that level -- nobody cares what the initial disagreement was, we were arguing about the meaning of the word "is" at that point.
I wrote this disclaimer because I was surprised to find harassment for such a harmless topic as Python's type hinting. I'm surprised dang never stepped in. The flamewar went for a surreal nesting depth, and you know what goes on at that level -- nobody cares what the initial disagreement was, we were arguing about the meaning of the word "is" at that point.
I'm typing my code very often for static analysers.
There is a GitHub repository: https://github.com/OriRoth/python-typing-machines
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.
I bet it could.
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.
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.
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.
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.
Typescript's type system (not the language, the _type system_ specifically) is the same! Folks have done cool things, like implement TicTacToe types [0] and a pure-types JSON parser [1]
[0]: https://blog.joshuakgoldberg.com/type-system-game-engines/
[1]: https://github.com/jamiebuilds/json-parser-in-typescript-ver...
[0]: https://blog.joshuakgoldberg.com/type-system-game-engines/
[1]: https://github.com/jamiebuilds/json-parser-in-typescript-ver...
Don’t miss the code package linked in the paper: https://zenodo.org/record/7004898
I always felt like the Python type system was underpowered compared to e.g. TypeScript (not necessarily a bad thing), but I guess it’s still enough to be Turing-complete.
I always felt like the Python type system was underpowered compared to e.g. TypeScript (not necessarily a bad thing), but I guess it’s still enough to be Turing-complete.
Does this imply dependent types can be implemented?
I.e. if the hinting system is turing complete, it surely can express the concept as a program?
I.e. if the hinting system is turing complete, it surely can express the concept as a program?
Turing complete means that any computation can be done within the system. However, there are many Turing complete systems that still can't do a particular thing because they lack the relevant input/output ports. For instance, Conway's Life is well known to be Turing complete, but you can't make it run Doom, because there's no way to input values into it from a controller of any type, and there's no hook-up for the Life simulation to output to a conventional display. (The latter might be theoretically addressable, but the former is not. Life is intrinsically defined with its whole universe specified at the beginning. If you create something that can take in "input" you've created a new variant of Life. Which would not be a crime or anything and may be interesting in its own right, you just wouldn't be working with Life anymore.) You could statically convert some fixed series of inputs into some particular Life initial state, and somehow give it a specification for how to "output" Doom internally, and then run that, but that's not really "running Doom".
The fact that you can embed any arbitrary Turing complete operation into the type checking operation does not mean you have the correct input and output operations to apply a Turing-complete dependent type system onto a Python program.
Now, I'm not saying it can't be done, because I'm not taking a close enough look to be sure, and underestimating motivated type hackers is not a smart idea. But my gut says the odds that you're missing at least one critical source of information or output action you'd need to make this work approaches one. Especially in Python, of all languages. Python's "primitives" are incredibly complex and full of capability and trying to constrain them via dependent types is not entirely dissimilar to trying to make a "safe" subset of Python, which has proved to be effectively impossible even with a great deal more access to the internals of Python over the decades than a type system checking would have.
The fact that you can embed any arbitrary Turing complete operation into the type checking operation does not mean you have the correct input and output operations to apply a Turing-complete dependent type system onto a Python program.
Now, I'm not saying it can't be done, because I'm not taking a close enough look to be sure, and underestimating motivated type hackers is not a smart idea. But my gut says the odds that you're missing at least one critical source of information or output action you'd need to make this work approaches one. Especially in Python, of all languages. Python's "primitives" are incredibly complex and full of capability and trying to constrain them via dependent types is not entirely dissimilar to trying to make a "safe" subset of Python, which has proved to be effectively impossible even with a great deal more access to the internals of Python over the decades than a type system checking would have.
FWIW: https://www.youtube.com/watch?v=xP5-iIeKXE8 If you allowed toggling particular points manually as input from a controller... probably not too far away from possible!
Kinda-sorta, but possibly not in a useful way. The fact that the type system can express numbers doesn't mean that those numbers are the same numbers used in the host language.
Church-encoded numerals are a common trick. This basically means the number 3 is encoded as Suc<Suc<Suc<Zero>>>.
Church-encoded numerals are a common trick. This basically means the number 3 is encoded as Suc<Suc<Suc<Zero>>>.
You're thinking of Peano numerals. The Church encoding of 3 is `lambda f: (lambda x: f(f(f(x))))`
Type hints might be Turing-complete, but I don't think it is Turing-complete in any practically useful way.
As others here have said, it is often more difficult to prevent Turing completeness in your system than add it.
Is this a joke?
Python type checking allows eval with arbitrary code. Of course it's Turing complete.
Python type checking allows eval with arbitrary code. Of course it's Turing complete.
I don't think it's looking at that: it's looking purely at the type hints themselves. It's the _solver_ (which doesn't run any Python code as such) for the type checker that's Turing complete.
I'd recommend actually reading the paper.
I'd recommend actually reading the paper.
Indeed - the paper is essentially talking about how to compile Turing Machines down to Python type hints, to be executed by mypy, not Python itself.
Can you please explain why this is useful? I'm an intermediate python programmer with some undergrad level knowledge of complexity theory, so this is mostly over my head, but it's interesting. I have no idea what one would actually use the results of this paper for - is it just a curiosity?
Like others have said, this isn't really about being useful, so much as interesting or revealing. It answers the question "can we be certain that a Python program with type hints can actually be type-checked?" by saying "sorry, no: it's possible that the type checking will never finish".
The paper does that by hooking into some basic results of theoretical computer science: Turing Machines (TMs) can model any program, there is no program that can look at another program and say that it finishes execution (the halting problem is undecidable), and, oops, you can compile TMs into Python type hints, therefore type checking Python is undecidable.
The paper does that by hooking into some basic results of theoretical computer science: Turing Machines (TMs) can model any program, there is no program that can look at another program and say that it finishes execution (the halting problem is undecidable), and, oops, you can compile TMs into Python type hints, therefore type checking Python is undecidable.
Ah, I see! That makes a lot of sense, thank you for explaining.
If I understand correctly, that means type-checking python as you described was an open problem before, and this paper effectively proves it will never happen (ideally). They do this by establishing Turing completeness of type-hints, which are the main mechanisms for type-checking.
If I understand correctly, that means type-checking python as you described was an open problem before, and this paper effectively proves it will never happen (ideally). They do this by establishing Turing completeness of type-hints, which are the main mechanisms for type-checking.
Well, I'm sure mypy and things like it will continue to grow, and the discipline of Python type hinting will probably become more popular, not less, because it offers new opportunities for catching bugs (but maybe not for optimizations, which I think is interesting*). So maybe it was an open question whether type checking would always terminate (now answered in the negative), but that shouldn't stop anyone from using type hints, considering their practical benefits.
* https://doc.pypy.org/en/latest/faq.html#would-type-annotatio...
* https://doc.pypy.org/en/latest/faq.html#would-type-annotatio...
In principle, this means you can ask mypy to check arbitrary properties of your code at compile-time. (It won't necessarily succeed, because not all properties can be checked, but you can make it try). In practice, python is very poorly suited to this kind of work.
It means that the type checker is Turing complete and can in theory run forever or get stuck in an infinite loop.
It also means that it's expressive enough such that it can be more powerful then a traditional type system
It also means that it's expressive enough such that it can be more powerful then a traditional type system
I'm surprised how many people are pointing to the halting problem. It might be the most well known thing about Turing Machines, but doesn't seem like the most relevant here.
Turing equivalence seems more interesting. Intuitively I'd think that type systems are supposed to be more constrained than programs they are being applied to. The fact that they are equivalent makes me think that those type systems are flawed (though I can't explain why).
Turing equivalence seems more interesting. Intuitively I'd think that type systems are supposed to be more constrained than programs they are being applied to. The fact that they are equivalent makes me think that those type systems are flawed (though I can't explain why).
Nothing is suppose to be one way or the other. It's just a feature with a trade off that exists or doesn't exist.
There are plenty of languages with turing complete type systems.
agda, idris, coq, haskell, scala, etc...
There are plenty of languages with turing complete type systems.
agda, idris, coq, haskell, scala, etc...
It's mostly a curiosity. Occasionally things like this occur: https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-i... . TL;DR exploited an accidentally turing complete file format to execute instructions inside a virtual machine.
I often don't even read the article. I just read the comments and tidbits like this thread help me piece together what's going on without ever consulting the actual article.
I wonder how many people actually do this and whether the proportion is big enough such that much of what's written in comments is heavily distorted.
I wonder how many people actually do this and whether the proportion is big enough such that much of what's written in comments is heavily distorted.
Annotations evaluate arbitrary code, type hints do not.
Although often confused, fairly enough as they were introduced in the same PEP, an annotation is a part of the Python syntax and type hints are a specific set of notations and ways you can use those notations inside an annotation to be used by a type hinter (yes those notations are evaluated to objects at Python runtime but the type hinter never has to be aware of that or even ever use a Python runtime).
The paper is talking about those notations inside a type hinter, not annotation objects inside a Python runtime. e.g. you can get mypy to run a turing complete program using only the notations defined in PEP 484.
Although often confused, fairly enough as they were introduced in the same PEP, an annotation is a part of the Python syntax and type hints are a specific set of notations and ways you can use those notations inside an annotation to be used by a type hinter (yes those notations are evaluated to objects at Python runtime but the type hinter never has to be aware of that or even ever use a Python runtime).
The paper is talking about those notations inside a type hinter, not annotation objects inside a Python runtime. e.g. you can get mypy to run a turing complete program using only the notations defined in PEP 484.
All this proves is Turing's methodology is flawed. It ignores the primary question in a vain attempt to create an oddity.
What good does it do for the "hints" to do the work of Python, Pascal, C++ or anything else for that matter?
It does "hints". Does it do "hints" well? If yes, then it provides value.
What good does it do for the "hints" to do the work of Python, Pascal, C++ or anything else for that matter?
It does "hints". Does it do "hints" well? If yes, then it provides value.
Nobody (okay, mostly nobody) is saying, "We should do computation in the type system!"
I think it's more: "Watch out, you could create types that never resolve."
I think it's more: "Watch out, you could create types that never resolve."
Exactly. Although, I would add that type level computations definitely can be used to perform useful metaprogramming tasks, such as embedding domain-specific languages or enforcing API protocols at compile time. I show some examples in my other papers. You can also check out my blog post: https://blog.sigplan.org/2021/03/02/fluent-api-practice-and-...
When Python 3 came out, annotations were indeed added to the language, but no use case was decided for them. It was an experiment to see what the community would do with them instead of forcing a use case base on what the core devs would think would be useful.
In order to allow this, annotations where permitted to be any legal python expression.
Nowadays, type hints have won: annotations are widely used to add static type checking in Python. But the way the language treat them have not changed much appart from becomming lazy. While mypy cannot understand dynamic Python expressions in them, those are nevertheless legal syntax, and will result in correct metadata at runtime.
Therefore, were the typing system not turing complete, the annotations would have been anyway by nature of being basically an exec().