Hacker News Reader

Comment by acomar | Hacker News Reader

Agda and Coq retain inference and decidability by sacrificing Turing completeness. Terminating programs must terminate provably, and non-terminating programs must make concrete progress on every iteration. I'm not familiar enough with Idris to say how it tackles this issue - I do know that it is Turing complete.

So with that said, you're absolutely right.

View on HN

Another language with a Turing complete type system is Shen [1] (previous life as Qi). Just wanted to put that out there as its a Lisp dialect that really pushes Lisp out there.

[1] http://shenlanguage.org/

When it comes to awesomeness to fame ratio, I can't think of a language with a higher one than Shen. It's odd how little people talk about it. I, unfortunately, suspect it has to do with the people leading it.

I've looked at Shen a few times and, honestly, I always get turned off by the syntax. There's not enough out there explaining why I should continue past that concern, and it seems to throw out what's nice about Lisp syntax in order to get halfway to Haskell's.

I'm sure I'll take a look at it again sometime, but I'd really love some kind of intro that helped me to understand why it was worth the time investment to get to know it.

License has been a major turn off, just like Plan 9. Did they fix that yet?

> Agda and Coq retain inference and decidability by sacrificing Turing completeness.

I don't know if I would phrase it that way, but there's a more important slight of hand going on here and I think chongli was right in spirit. Haskell takes care of (most) type level things for you with inference. Coq and Agda allow you to give very precise types to things, but those very precise types involve values that are not automatically inferred for you. It's certainly not the case that you can write the same annotation-free function in Coq that you would have written in Haskell and have a very precise type inferred for you.

Reply on news.ycombinator.com