Hacker News Reader

Comment by thinkpad20 | Hacker News Reader

You could look at ATS. I don't know a huge amount about it but I know it's a very high-performance bare-metal language with dependent types, or at least, more expressive types than Haskell/ML.

(Caveat: I've never written ATS, and although I've written in Coq and Idris, every time I look at ATS code it looks like complete gibberish).

View on HN

Most of the ATS examples begin with something which looks like ML, but as the types are made more and more strict they end up looking like incredibly verbose C.

To make things worse, I don't think ATS has any inference either, so all of this must be written explicitly. Idris, Agda, Coq, etc. can infer types and values, if they're unambiguous.

For example:

    Definition Prime p := forall n m, n * m = p -> n = 1 \/ m = 1.

All of these variables have type nat, which Coq can infer from the use of "*" and "=".

Reply on news.ycombinator.com