3 ms·
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-
by 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 agoCoq is all about the types.
- deleted 4y ago[deleted]
- ackfoobar 4y agoI'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 agoIntersection 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 agoHaskell 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 agoSure, 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