[HN Gopher] Python type hints are Turing complete
___________________________________________________________________
Python type hints are Turing complete
Author : nemoniac
Score : 196 points
Date : 2022-09-09 13:56 UTC (9 hours ago)
(HTM) web link (arxiv.org)
(TXT) w3m dump (arxiv.org)
| muttantt wrote:
| 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.
| hbrn wrote:
| 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_af wrote:
| 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.
| hbrn wrote:
| 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.
| the_af wrote:
| Thanks for the reply. I think we actually agree on this,
| only coming from different sides.
| muttantt wrote:
| 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?
| __MatrixMan__ wrote:
| 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.
| zx14 wrote:
| I'm typing my code very often for static analysers.
| belter wrote:
| BiteCode_dev wrote:
| 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().
| anderskaseorg wrote:
| 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.
| arjvik wrote:
| What other use cases did the community come up with?
| patrick91 wrote:
| I've created strawberry graphql, it uses type hints to
| generate GraphQL schemas
| Waterluvian wrote:
| 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.
| ok123456 wrote:
| Things like pydantic and fastapi where the type annotations
| are used for run time argument validation and interface
| generation.
| [deleted]
| whimsicalism wrote:
| 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.
| BiteCode_dev wrote:
| There was a heated debate because it broke things at the
| time, but now it works, yes.
| whimsicalism wrote:
| 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
| patrick91 wrote:
| 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
| BiteCode_dev wrote:
| 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.
| arjvik wrote:
| Cool, any examples of libraries that use it for dependency
| injection or FFI or validation?
| BiteCode_dev wrote:
| 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.
| kylebarron wrote:
| Specifically it's the underlying pydantic that does
| validation based on annotations
|
| https://pydantic-docs.helpmanual.io/
| BiteCode_dev wrote:
| 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
| kortex wrote:
| Dependency-injector uses it for exactly this purpose
| @inject def main(service: Service =
| Provide[Container.service]) -> None: ...
|
| FastAPI also does a similar sort of trick, for DI and
| also request parsing.
|
| https://python-dependency-injector.ets-
| labs.org/introduction...
| GalaxySnail wrote:
| For FFI, there is a pure python mode in cython:
| https://cython.readthedocs.io/en/latest/src/tutorial/exte
| rnal.html
| samatman wrote:
| 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 wrote:
| 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.
| samatman wrote:
| 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 wrote:
| 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.
| __MatrixMan__ wrote:
| 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.
| paxys wrote:
| As others here have said, it is often more difficult to _prevent_
| Turing completeness in your system than add it.
| w-m wrote:
| 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?)
| llimllib wrote:
| 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
| spicybright wrote:
| It's not like they can code their website for every custom
| style everyone wants to use on their browser...
| llimllib wrote:
| I don't have a custom style, this is plain jane firefox
| squeaky-clean wrote:
| I get same on iOS/Safari with my phone in dark mode.
| samatman wrote:
| Yes, but not making a mess of dark mode is worth
| criticizing by now.
| messe wrote:
| 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 wrote:
| The code is a healthy dark color for me. Totally fine.
| pmontra wrote:
| 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.
| folkrav wrote:
| You must be using Dark Reader or something similar? Page is
| light mode, and the text darker gray by default for me.
| mcluck wrote:
| I have Dark Reader and disabled it. It looks like what they
| posted. It must be a poorly implemented dark mode.
| kevincox wrote:
| No, I think any prefers-colour-scheme: dark triggers this.
| layer8 wrote:
| That's only in dark mode, because they use the default text
| color.
| turbocon wrote:
| 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-m wrote:
| 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
| jimcavel888 wrote:
| cosmolev wrote:
| Surprisingly Turing-Complete: https://www.gwern.net/Turing-
| complete
| bmc7505 wrote:
| There is a GitHub repository: https://github.com/OriRoth/python-
| typing-machines
| freedude wrote:
| 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 wrote:
| 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."
| OriRoth wrote:
| 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-...
| vngzs wrote:
| 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"?
| OriRoth wrote:
| Yes, this is an obvious mistake. What you wrote is the right
| statement.
| XorNot wrote:
| 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?
| jerf wrote:
| 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 wrote:
| 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!
| samatman wrote:
| It _can_ run Doom, in other words, but Doom can 't be played
| upon it.
| jerf wrote:
| Fair enough. :)
| lmkg wrote:
| 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_shores wrote:
| You're thinking of Peano numerals. The Church encoding of 3
| is `lambda f: (lambda x: f(f(f(x))))`
| planede wrote:
| Type hints might be Turing-complete, but I don't think it is
| Turing-complete in any practically useful way.
| FartyMcFarter wrote:
| I've seen it said that Turing completeness is so prevalent that
| one often has to intentionally prevent it when designing a
| system.
| asddubs wrote:
| on the other hand, technically nothing is turing complete
| because of lack of infinite memory
| ModernMech wrote:
| Turing completeness is about _simulating_ a Turing machine,
| not being one.
| whimsicalism wrote:
| Nah they're technically correct. You can't simulate a
| Turing machine with finite memory.
| ModernMech wrote:
| 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?
| whimsicalism wrote:
| 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.
| ModernMech wrote:
| 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.
| asddubs wrote:
| >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.
| jasamer wrote:
| 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.
| samatman wrote:
| 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.
| asddubs wrote:
| of course, hence "technically", or "I'm being a smartass,
| but"
| kps wrote:
| A Turing machine has _unbounded_ tape, not _infinite_ tape.
| asddubs wrote:
| which effectively means it has infinite memory, does it
| not?
| tripa wrote:
| Infinite memory available, but never used.
| ezfe wrote:
| 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.
| kps wrote:
| When you look at the space complexity of an algorithm,
| it's never 'infinity'.
| Filligree wrote:
| I've seen it demonstrated that people who try to prevent it,
| often fail.
| nneonneo wrote:
| 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.
| jimsimmons wrote:
| Is this a joke?
|
| Python type checking allows eval with arbitrary code. Of course
| it's Turing complete.
| talideon wrote:
| 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.
| deltasevennine wrote:
| 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.
| an1sotropy wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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
| w1nk wrote:
| 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.
| an1sotropy wrote:
| 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 wrote:
| 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 wrote:
| 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...
| oblvious-earth wrote:
| 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.
| talideon wrote:
| 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.
| Sharlin wrote:
| 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?
| chalst wrote:
| 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 wrote:
| > 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.
| user5678 wrote:
| WJW wrote:
| 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.
| zaik wrote:
| Coq is all about the types.
| ackfoobar wrote:
| I'm a layman, and I understand that Coq is a proof
| assistant that uses type theory. This comment seems true to
| me.
|
| Why is it down-voted?
| [deleted]
| samatman wrote:
| 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.
| ChadNauseam wrote:
| 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 wrote:
| 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...
| titzer wrote:
| 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
___________________________________________________________________
(page generated 2022-09-09 23:00 UTC)