Hacker News Reader

Comment by olliesaunders | Hacker News Reader

Anyone here use Qi, Mercury, or Agda? I’m interested in what people think of those languages.

Agda is a proof assistant. I've used Coq, but not Agda -- I imagine they're similar. You wouldn't use it for general development.

Qi is interesting but the development community is much smaller than its competitors (mainly Haskell). You probably want to look into Shen, not Qi. Qi development has mostly stalled.

Why wouldn’t you use it Agda/Coq for general development? (Looking for reasons other than a presumed lack of libraries.)

It's very slow and every function must have formal properties, e.g. all functions are total and must formally be proved to terminate.

(As far as I know. I've only worked through Pierce's book.)

In the dependently typed family of languages it's a little bit arbitrary to divide between programming languages and proof assistants since everyone in this space can be made to play both roles in a pinch. I think most people think of Coq as more on the proof assistant side and Agda more on the programming language side.

Sort of. Dependent types doesn't explain Coq's requirement for pure, total functions. Unless this restriction is weakened I cannot see it as being useful in any general-purpose domain. Agda may be looser.

> Dependent types doesn't explain Coq's requirement for pure, total functions.

That's where you are wrong. Partial functions introduce the bottom value and then you can 'prove' arbitrary incorrect things.

I'm not sure what you're saying. I was saying that simply being dependently typed doesn't necessitate pure total functions. Obviously, these features can be considered either highly suggested or necessary for ITPs. There are a number of ways you can get around totality with dependent types.

I have tried Mercury a few times. Prolog sans REPL is no use to me. I'm interested in Agda but haven't put much effort into it.

Reply on news.ycombinator.com