Python type hints are Turing complete

https://arxiv.org/abs/2208.14755

by nemoniac • 4 years ago

246 135 4 years ago

arxiv.org

XorNot• 4 years ago

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?

jerf2• 4 years ago

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.

DougBTX• 4 years ago

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!

samatman6• 4 years ago

It can run Doom, in other words, but Doom can't be played upon it.

planede• 4 years ago

Type hints might be Turing-complete, but I don't think it is Turing-complete in any practically useful way.

lmkg• 4 years ago

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>>>.

hither_shores2• 4 years ago

You're thinking of Peano numerals. The Church encoding of 3 is `lambda f: (lambda x: f(f(f(x))))`

jimsimmons• 4 years ago

Is this a joke?

Python type checking allows eval with arbitrary code. Of course it's Turing complete.

talideon2• 4 years ago

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.

an1sotropy3• 4 years ago

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.

deltasevennine3• 4 years ago

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.

oblvious-earth• 4 years ago

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.

talideon2• 4 years ago

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.

ChadNauseam• 4 years ago

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).

tromp• 4 years ago

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...

Sharlin• 4 years ago

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?

zaik• 4 years ago

Coq is all about the types.

chalst• 4 years ago

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

bradrn• 4 years ago

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.

WJW• 4 years ago

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.

samatman6• 4 years ago

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.

w-m2• 4 years ago

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?)

llimllib2• 4 years ago

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

messe• 4 years ago

The math typesetting, while not unreadable, is annoying as well. It seems to be using a smaller x-height for math than for text.

davidatbu• 4 years ago

The code is a healthy dark color for me. Totally fine.

folkrav• 4 years ago

You must be using Dark Reader or something similar? Page is light mode, and the text darker gray by default for me.

layer8• 4 years ago

That’s only in dark mode, because they use the default text color.

spicybright• 4 years ago

It's not like they can code their website for every custom style everyone wants to use on their browser...

pmontra• 4 years ago

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.

turbocon• 4 years ago

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.

w-m2• 4 years ago

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

titzer• 4 years ago

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

jrvarela562• 4 years ago

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?

eru3• 4 years ago

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.

ipnon• 4 years ago

You want an algebra for the bits and an algebra for the functions.

bmc7505• 4 years ago

There is a GitHub repository: https://github.com/OriRoth/python-typing-machines

cosmolev• 4 years ago

Surprisingly Turing-Complete: https://www.gwern.net/Turing-complete

FartyMcFarter• 4 years ago

I've seen it said that Turing completeness is so prevalent that one often has to intentionally prevent it when designing a system.

Filligree2• 4 years ago

I've seen it demonstrated that people who try to prevent it, often fail.

asddubs5• 4 years ago

on the other hand, technically nothing is turing complete because of lack of infinite memory

ModernMech3• 4 years ago

Turing completeness is about simulating a Turing machine, not being one.

samatman6• 4 years ago

A caveat which covers a whole category is illustrating an elision, not a mistake. We know that we mean finite memory, because of, er. Reality.

kps2• 4 years ago

A Turing machine has unbounded tape, not infinite tape.

kortex3• 4 years ago

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...

muttantt2• 4 years ago

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.

zx14• 4 years ago

I'm typing my code very often for static analysers.

hbrn3• 4 years ago

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.

the_af5• 4 years ago

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.

atomicnumber3• 4 years ago

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.

BiteCode_dev9• 4 years ago

Even 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().

arjvik3• 4 years ago

What other use cases did the community come up with?

ok123456• 4 years ago

Things like pydantic and fastapi where the type annotations are used for run time argument validation and interface generation.

BiteCode_dev9• 4 years ago

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.

patrick912• 4 years ago

I've created strawberry graphql, it uses type hints to generate GraphQL schemas

Waterluvian• 4 years ago

I 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.

_dain_• 4 years ago

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.

Too• 4 years ago

Creating argument parsers for CLIs: https://pypi.org/project/argtyped/

I've seen similar (in-house) to generate HTML forms also.

anderskaseorg2• 4 years ago

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:

    def f() -> int: return 1
    def f() -> (lambda: int)(): return 1

only the first is correctly typed by PEP 484. mypy rejects the second with “error: Invalid type comment or annotation”.

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.

eru3• 4 years ago

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.

BiteCode_dev9• 4 years ago

That's why my comment litterally starts with "even before talking about the typing system itself".

paxys• 4 years ago

As others here have said, it is often more difficult to prevent Turing completeness in your system than add it.

vngzs• 4 years ago

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

    str <: object ∧ str ≮: object

a contradiction? Wouldn't `object ≮: string` be the correct representation of "not every object is a string"?

OriRoth2• 4 years ago

Yes, this is an obvious mistake. What you wrote is the right statement.

samatman6• 4 years ago

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.

envp• 4 years ago

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.

__MatrixMan__3• 4 years ago

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.

samatman6• 4 years ago

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.

crote• 4 years ago

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.

freedude• 4 years ago

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.

rcfox• 4 years ago

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."

OriRoth2• 4 years ago

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-...

nneonneo• 4 years ago

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.

xavdid• 4 years ago

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...

Python type hints are Turing complete

Related Stories