4 ms·

Is this a joke? Python type checking allows eval with arbitrary code. Of course it's Turing complete.

talideon 4y 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.
- an1sotropy 4y 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.
  - lake_vincent 4y ago
    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?
    - hither_shores 4y ago
      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.
    - deltasevennine 4y ago
      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
      - hbrn 4y ago
        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).
        deltasevennine 4y ago
        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...
    - w1nk 4y ago
      It's mostly a curiosity. Occasionally things like this occur: https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-into-nso-zero-click.html 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.
    - an1sotropy 4y ago
      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.
      - lake_vincent 4y ago
        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.
        an1sotropy 4y ago
        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-annotations-help-pypy-s-performance https://doc.pypy.org/en/latest/faq.html#would-type-annotatio...
- deltasevennine 4y 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 4y 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.

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.

an1sotropy 4y 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.
- lake_vincent 4y ago
  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?
  - hither_shores 4y ago
    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.
  - deltasevennine 4y ago
    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
    - hbrn 4y ago
      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).
      - deltasevennine 4y ago
        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...
  - w1nk 4y ago
    It's mostly a curiosity. Occasionally things like this occur: https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-into-nso-zero-click.html 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.
  - an1sotropy 4y ago
    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.
    - lake_vincent 4y ago
      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.
      - an1sotropy 4y ago
        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-annotations-help-pypy-s-performance https://doc.pypy.org/en/latest/faq.html#would-type-annotatio...
deltasevennine 4y 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 4y 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.