5 ms·

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

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 4y 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 4y 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_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
Sharlin 4y 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 4y ago
  Coq is all about the types.
  - deleted 4y ago
    [deleted]
  - ackfoobar 4y ago
    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?
- chalst 4y 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 https://en.wikipedia.org/wiki/Intersection_type_discipline
- bradrn 4y 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 4y 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.
- samatman 4y 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.
- user5678 4y ago

ChadNauseam 4y 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 4y 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_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...

Sharlin 4y 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 4y ago
Coq is all about the types.
- deleted 4y ago
  [deleted]
- ackfoobar 4y ago
  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?
chalst 4y 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 https://en.wikipedia.org/wiki/Intersection_type_discipline
bradrn 4y 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 4y 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.
samatman 4y 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.
user5678 4y ago