Hacker News new | ask | show | jobs
by tome 4718 days ago
> So yes, Virginia, there is indeed a Pure Functional Programming. But you can't do it in Haskell.

True, but if you want to get as close to purity as possible whilst actually writing usable software Haskell is the answer. I'd love it if Agda was actually a fully fledged programming language, but currently it is not.
1 comments
jonsterling 4718 days ago
Yeah, though Idris I think will soon become the “reasonable trade-off” language that Haskell is today. We could do worse, I suppose!

What I really want is a proper Epigram with OTT (or, be still my quaking heart, HoTT).

link
tome 4718 days ago
> Yeah, though Idris I think will soon become the “reasonable trade-off” language

That would be cool.

Don't know anything about Epigram though. Dependent types is still firmly on my todo list.

link
jonsterling 4716 days ago
Come hang out with us on freenode (#agda, #coq, #idris) and we'll try to answer any questions you have about dependent types and such!
link