[jonsterling]

Since I'm being downvoted, let me clarify for the “hackers”.

By “pure”, I mean lacking unaccounted side effects (including crashing and non-termination).

I take a rather strong view, as you can tell, of what it means to “support” pure functional programming. That is, I think it is insufficient to show that your code lacks appeals to falsehood and rampant non-termination. Because your code is linked with other code from other sources, it must be shown that appeals to falsehood and rampant non-termination are in fact _impossible_.

(By “rampant non-termination” and “appeals to falsehood”, I mean the use of circular reasoning. This is distinct from structural recursion and coinduction, which can be used to do REPLs and servers.)

So yes, Virginia, there is indeed a Pure Functional Programming. But you can't do it in Haskell.

[tome]

> 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.

[jonsterling]

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).

[tome]

> 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.

[jonsterling]

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!