Hacker News Reader

Considering it's a port/rewrite of Qi, which uses a Turing-complete interpretation of the sequent calculus, yes, it is more powerful than all those languages.

You're right to be suspicious at extraordinary claims, but the tiniest bit of research gets you the extraordinary answers in this case. I'm quite surprised you know of Agda, Coq, and Epigram, but not Qi.

View on HN

If Turing-completeness is the kind of powerful you're talking about, then Qi's would be more powerful. However, if you're talking about the amount of things the type system can verify, a Turing-complete type system would be subject to the halting problem, and thus is less powerful in that way.

And it looks like Qi's type system is optional. If your only definition of type system power is Turing completeness, then sure, it's powerful, but it can't accomplish the same kinds of verification as Agda, etc.

Relevant: "When we say that a language is expressive, we mean that it is easy to use. When we say that a type system is expressive, we mean that it is not." - Gilad Bracha

Very true, and awesome quote. It's worth noting though that once you're talking about dependently-typed type systems, it's accepted that you're going to be doing a lot of work with the type system. You're going to be using proof tactics to type your programs. It's almost the point at that point.

Reply on news.ycombinator.com