Hacker News Reader

Comment by Peaker | Hacker News Reader

When someone writes "Shen has the most powerful type system of any existing functional language, including ML and Haskell", I get suspicious.

Have they really studied each and every type system out there? What kind of dependent types do they have? How do they compare to Agda, Coq, Epigram?

View on HN

The idea is that Shen has a turing-complete type system, so it shouldn't even be possible to create a more powerful type system (given a specific definition of "powerful").

To expand on that idea a little bit: that's a valid definition of 'powerful', but there's another definition of 'powerful' which some people mean when they talk about type systems, and that's "To what degree does this type system prevent errors?" It seems from cursory research that Shen is powerful with respect to the definition, "To what degree can we encode computations in the type system at compile-time?" and Agda and Coq's type systems are powerful with respect to the definition, "How can we limit the class of programs by encoding constraints in the type system such that the resulting programs are provably correct?" Consequently, neither Agda nor Coq are Turing-complete even at the language level, much less the type level, but that accordingly gives them greater power to know information about their programs at compile time.

I think this may be kind of a question of definitions. Agda and Coq at least are more like DSLs for constructing proofs than general-purpose functional programming languages. I'm not familiar with Epigram, but assuming it's similar to the other two in the list, I think you're redefining his terms for him, which is a little bit unfair.

Nobody said anything about "general-purpose functional programming languages", the blurb says "existing functional languages". All of Epigram, Agda and Coq are functional and currently exist. :) More seriously, Coq is designed explicitly to be a proof assistant, but Agda and Epigram are meant to be programming languages.

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.

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