4 ms·

> I think many people question that they are good ideas. Not pure functions -- but forcing all functions to be pure. If you do that, you are basically forced to

> I think many people question that they are good ideas. Not pure functions -- but forcing all functions to be pure. If you do that, you are basically forced to use monads for all effects, and that is very questionable. You aren't forced to use monads specifically. What you're forced to do is distinguish pure from impure computations somehow. In the CBPV papers, it's clearly explained that functions are just one particular kind of computation. In CBPV, there's an adjunction between the categories of value types and computation types, and it's this adjunction that gives rise to a monad [corresponding to the effect(s) that computations might exhibit]. If we consider pure computations only [no effects, not even nontermination], this adjunction is actually an equivalence of categories. --- > Yeah, Rust does something nice, too, but every operation allowed by Clojure is also allowed by Rust. I don't see how it's any better. Erlang's "let it crash" has nothing to do with data-race bugs. I'm not talking about data races. Of course the absence of sharing in Erlang frees you from data races. But they don't free you from breaking transactional invariants, such as "this doesn't even begin happening unless that condition is met". In spite of the absence of data races, Erlang is still about coping with failure, not outruling it. In Rust, you can use a nonforgeable witness that the precondition holds, and consume it when the operation begins. It's rare that a non-dependently typed language is better than Haskell at something other than performance, but that's exactly what's happening here. > Once you have a GC everything is a lot easier when it comes to concurrency. Rust works very hard to ensure safety without a GC, which is necessary for domains that can't use GCs (like programs in constrained environments). Garbage collection makes sharing easy. However, concurrency control (i.e., controlling access to shared mutable resources) remains just as hard. Otherwise, nobody would have invented such things as "global interpreter locks". > And in any case, I think most people would consider Rust to be even less functional or more imperative (whatever that means) than Clojure. Indeed, Rust isn't terribly functional (though it's more functional that meets the eye), which is exactly why I said it's a better argument for "there are other ways besides functional programming". --- > I also challenge you to program the world's most used sorting algorithm, TimSort, with equational reasoning. Well, in order to use equational reasoning alone, I need a purely functional algorithm. > And consider this -- Haskell is grossly insufficient to really reason about programs in this way. Idris is the very minimum to even start, and even that doesn't even begin to scratch temporal logic. Haskell's type system is insufficient to verify equational reasoning using the type system, but equational reasoning is so simple that programmers can do it manually anyway. [More on this later.] On the other hand, programming languages based on dependent type theory, like Idris, while often more beautiful, and certainly more powerful, don't yet pass my bang for the buck test for everyday programming: (0) They force me to annotate things that Haskell can infer on its own. (1) It is a royal pain in the ass to manually translate data between representations that are convenient for proving [e.g., Peano naturals] and representations that are efficient for calculating things at runtime [e.g., machine integers, big integers]. (2) Most dependently typed languages often don't have terribly efficient implementations. To the best of my knowledge, ATS is the only honorable exception to the last point. --- > That is a mathematical argument. Not a psychological one. You could use the same argument to claim that teaching a person to catch a ball is easier if you teach them Newton's equations than let them practice. Your analogy breaks when you think about it non-superficially. Merely understanding the laws of physics won't make your muscles strong enough, or your reflexes fast enough to go out there and actually catch a ball. On the other hand, when you've written a program alongside its proof of correctness, well, you've written a program! --- > Yes, imperative programming is too complicated for machines to verify in every circumstance, yet claiming it is too complicated for humans pretty much ignores reality (or, at the very least, requires some serious explaining). It's too complicated for humans to verify too. If it weren't, more people would be doing it casually. This is unarguable, unless you've tried it yourself. > even with security, memory safety has done a lot to make things better, and where it hasn't, dependent types would be necessary to prove correctness, anyway. I never said that everything has to be machine verified. If you give me a proof that I can understand (i.e., I'm confident I can correctly verify), that's more than enough for me. But, if the proof is past a certain complexity threshold, I'll ask you to convince someone else that I can trust (a better mathematician or a proof assistant).

pron 11y ago
> What you're forced to do is distinguish pure from impure computations somehow. Imperative languages can do that very, very easily. The definition of PFP, though, is that it is referentially transparent, i.e. no effects whatsoever (other than monads that are returned to the runtime at the top level). > I need a purely functional algorithm. Good luck finding one with the same performance... But the imperative one is now proven to be correct with no need for PFP. Writing a similar provably correct PFP one would have been harder (so it seems to me at least). > but equational reasoning is so simple that programmers can do it manually anyway. That's a nice claim. What we know for a fact is that programmers are able to write programs that are as correct as they're required to be with imperative reasoning. > IT's too complicated for humans to verify too. If it weren't, more people would be doing it casually. I don't understand exactly what you're referring to, but most programs as correct as people want them to be. The correctness crisis is over, mostly thanks to automated testing. > If you give me a proof Who says we want correction proofs to begin with? Most projects require some evidence of some measure of correctness. Certainly not proof of total correctness or even proof of partial correctness.
- catnaroek 11y ago
  > Imperative languages can do that [distinguish pure from impure computations] very, very easily. In an imperative language, can I write a map or filter whose argument is guaranteed to be pure? [Note that my notion of "pure" is stronger than Haskell's: I consider nontermination an effect.] Can you easily convince the type system that an imperative loop will indeed terminate? [Without supplying anything even vaguely resembling a proof.] With pattern matching and recursion, the compiler can check whether recursive calls are always passed smaller arguments. > Good luck finding one with the same performance... I'm pretty sure that, with substructural types, it's possible to update a single array element in O(1) in a referentially transparent manner. Conceptually, you're destroying the old array, and creating a new one with the same contents, except for the updated element. But, because the old array won't be used anymore, this can be done in-place. As far as I can tell, no other imperative facilities are needed to sort an array. > as correct as they're required to be What does this even mean?

pron 11y ago

> What you're forced to do is distinguish pure from impure computations somehow. Imperative languages can do that very, very easily. The definition of PFP, though, is that it is referentially transparent, i.e. no effects whatsoever (other than monads that are returned to the runtime at the top level). > I need a purely functional algorithm. Good luck finding one with the same performance... But the imperative one is now proven to be correct with no need for PFP. Writing a similar provably correct PFP one would have been harder (so it seems to me at least). > but equational reasoning is so simple that programmers can do it manually anyway. That's a nice claim. What we know for a fact is that programmers are able to write programs that are as correct as they're required to be with imperative reasoning. > IT's too complicated for humans to verify too. If it weren't, more people would be doing it casually. I don't understand exactly what you're referring to, but most programs as correct as people want them to be. The correctness crisis is over, mostly thanks to automated testing. > If you give me a proof Who says we want correction proofs to begin with? Most projects require some evidence of some measure of correctness. Certainly not proof of total correctness or even proof of partial correctness.

catnaroek 11y ago
> Imperative languages can do that [distinguish pure from impure computations] very, very easily. In an imperative language, can I write a map or filter whose argument is guaranteed to be pure? [Note that my notion of "pure" is stronger than Haskell's: I consider nontermination an effect.] Can you easily convince the type system that an imperative loop will indeed terminate? [Without supplying anything even vaguely resembling a proof.] With pattern matching and recursion, the compiler can check whether recursive calls are always passed smaller arguments. > Good luck finding one with the same performance... I'm pretty sure that, with substructural types, it's possible to update a single array element in O(1) in a referentially transparent manner. Conceptually, you're destroying the old array, and creating a new one with the same contents, except for the updated element. But, because the old array won't be used anymore, this can be done in-place. As far as I can tell, no other imperative facilities are needed to sort an array. > as correct as they're required to be What does this even mean?