Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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



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).


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...




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: