4 ms·

I really think Haskell. Purity is super cool. As is functional programming in general.

by the_tractatus 13y ago

jonsterling 13y ago
If only Haskell were pure...
- jonsterling 13y ago
  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 13y 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.
    - jonsterling 13y 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).
      - tome 13y 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.
        jonsterling 13y 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!

I really think Haskell. Purity is super cool. As is functional programming in general.

jonsterling 13y ago

If only Haskell were pure...

jonsterling 13y ago
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 13y 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.
  - jonsterling 13y 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).
    - tome 13y 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.
      - jonsterling 13y 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!