12 ms·
Python type hints are Turing complete
- XorNot 4y agoDoes 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?
- jerf 4y agoTuring 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.
- DougBTX 4y agoFWIW: https://www.youtube.com/watch?v=xP5-iIeKXE8 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!
- samatman 4y agoIt can run Doom, in other words, but Doom can't be played upon it.
- jerf 4y agoFair enough. :)
- planede 4y agoType hints might be Turing-complete, but I don't think it is Turing-complete in any practically useful way.
- lmkg 4y agoKinda-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>>>.
- hither_shores 4y agoYou're thinking of Peano numerals. The Church encoding of 3 is `lambda f: (lambda x: f(f(f(x))))`
- jimsimmons 4y agoIs this a joke? Python type checking allows eval with arbitrary code. Of course it's Turing complete.
- talideon 4y agoI 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.
- an1sotropy 4y agoIndeed - the paper is essentially talking about how to compile Turing Machines down to Python type hints, to be executed by mypy, not Python itself.
- lake_vincent 4y agoCan 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?
- hither_shores 4y agoIn 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.
- deltasevennine 4y agoIt 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
- talideon 4y agoI'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.
- ChadNauseam 4y agoYou’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).
- tromp 4y agoIndeed; 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_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
- Sharlin 4y agoI 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?
- zaik 4y agoCoq is all about the types.
- w-m 4y agoHere's the article rendered as html: https://ar5iv.labs.arxiv.org/html/2208.14755 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?)
- llimllib 4y agoThe 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 https://cdn.billmill.org/static/newsyctmp/pytyping.png
- messe 4y agoThe math typesetting, while not unreadable, is annoying as well. It seems to be using a smaller x-height for math than for text.
- davidatbu 4y agoThe code is a healthy dark color for me. Totally fine.
- folkrav 4y agoYou must be using Dark Reader or something similar? Page is light mode, and the text darker gray by default for me.
- layer8 4y ago
- titzer 4y agoI 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 https://twitter.com/TitzerBL/status/1567677824105947136
- jrvarela56 4y agoThere 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?
- eru 4y agoTwo 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.
- jrvarela56 4y ago| 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.
- ipnon 4y agoYou want an algebra for the bits and an algebra for the functions.
- belter 4y ago
- bmc7505 4y agoThere is a GitHub repository: https://github.com/OriRoth/python-typing-machines https://github.com/OriRoth/python-typing-machines
- cosmolev 4y agoSurprisingly Turing-Complete: https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete
- FartyMcFarter 4y agoI've seen it said that Turing completeness is so prevalent that one often has to intentionally prevent it when designing a system.
- Filligree 4y agoI've seen it demonstrated that people who try to prevent it, often fail.
- deleted 4y ago[deleted]
- asddubs 4y agoon the other hand, technically nothing is turing complete because of lack of infinite memory
- ModernMech 4y agoTuring completeness is about simulating a Turing machine, not being one.
- whimsicalism 4y agoNah they're technically correct. You can't simulate a Turing machine with finite memory.
- ModernMech 4y agoTo 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?
- muttantt 4y agoI'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.
- zx14 4y agoI'm typing my code very often for static analysers.
- hbrn 4y agoSame 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.
- the_af 4y agoDisclaimer: 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.
- BiteCode_dev 4y agoEven before talking about the typing system itself, annotations existed by themselves and are not attached to any behavior in Python: they simply hold metadata. 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().
- arjvik 4y agoWhat other use cases did the community come up with?
- Too 4y agoCreating argument parsers for CLIs: https://pypi.org/project/argtyped/ https://pypi.org/project/argtyped/ I've seen similar (in-house) to generate HTML forms also.
- ok123456 4y agoThings like pydantic and fastapi where the type annotations are used for run time argument validation and interface generation.
- deleted 4y ago[deleted]
- whimsicalism 4y agoDoes 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.
- paxys 4y agoAs others here have said, it is often more difficult to prevent Turing completeness in your system than add it.
- vngzs 4y agoI 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 str <: object ∧ str ≮: object a contradiction? Wouldn't `object ≮: string` be the correct representation of "not every object is a string"?
- OriRoth 4y agoYes, this is an obvious mistake. What you wrote is the right statement.
- samatman 4y agoI 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.
- envp 4y agoPython'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.
- __MatrixMan__ 4y agoBut 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.
- samatman 4y agoThat 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.
- crote 4y agoBut 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.
- freedude 4y agoAll 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.
- rcfox 4y agoNobody (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."
- OriRoth 4y agoExactly. 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-theory/ https://blog.sigplan.org/2021/03/02/fluent-api-practice-and-...
- jimcavel888 4y ago
- nneonneo 4y agoDon’t miss the code package linked in the paper: https://zenodo.org/record/7004898 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.
- xavdid 4y agoTypescript'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/ https://blog.joshuakgoldberg.com/type-system-game-engines/ [1]: https://github.com/jamiebuilds/json-parser-in-typescript-very-bad-idea-please-dont-use https://github.com/jamiebuilds/json-parser-in-typescript-ver...