4 ms·
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 suc
by 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 agoI'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 agoNothing 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...