6 ms·

Yes, we all know how functional languages work; this is Y Combinator after all. However, that is a pedantic remark and missing OP's point. It is clear OP meant

Yes, we all know how functional languages work; this is Y Combinator after all. However, that is a pedantic remark and missing OP's point. It is clear OP meant a program as in an entire non-trivial system, not individual functions; even if they are programs themselves. Regardless, when one talks about function purity, it is about the final evaluation, not about partial binding or lazyness.

jcora 8y ago
This is actually not at all pedantic but a very fundamental, if subtle at first glance, point about purity. Once you start doing more advanced monadic programming it stops being subtle at all. Many people, yes "even on HN", are totally fooled by do notation and the imperative nomenclature, but there is nothing similar. You misunderstand it as well: it has nothing to do with evaluation mode. Idris is eagerly evaluated, for example, and _that function is still pure_! `f x = putStrLn x` gets "finally" evaluated and yes there is still no side effect. It is so evaluated that you can bind it to a variable and apply another function on it. Just like 2^100 is a pure expression, so is `putStrLn "hello"`. > It is clear OP meant a program as in an entire non-trivial system, not individual functions; even if they are programs themselves. It is not clear. Does he mean including the OS and hardware? Because no matter how complex, a pure program is still pure.
- simonh 8y ago
  Ok so run up an embedded OS and application on a system with limited resources so that all the memory is being used. Now run your pure functional program. The system crashes. Using memory is a side effect. Consuming CPU time is a side effect. Heating up the environment and drawing power due to that CPU usage is a side effect[0]. These are not trivial either, actual real systems used for critical activities fall prey to this sort of thing all the time. It just depends on what you are willing to consider as a side effect. [0]https://xkcd.com/1172/ https://xkcd.com/1172/
  - jcora 8y ago
    That's not what purity refers to! We're talking about a mathematical property of the language itself. The real issue is that people don't understand that `putStrLn "hello"` _is literally just as pure as `2*x`_. They are both like mathematical expressions in that they evaluate to a value and _nothing else_. The name "putStrLn" _suggests_ that this is similar to a print statement but it is emphatically not. You can evaluate it a billion times and nothing gets printed.
    - matt_kantor 8y ago
      Hang on a minute. The only difference is that the languages you are talking about have captured "doing I/O" as something that can be statically reasoned about, but not "consuming memory" (for example). From a mathematical perspective, one is part of the axioms while another is not. One could imagine a language where all memory allocation must be done explicitly via a monad, just like how in Haskell all I/O is performed inside an IO monad. If that were the case, you could have additional static guarantees about how memory is used. That doesn't mean that languages which don't do this are somehow inherently "impure"; they are simply "pure with respect to a certain set of axioms" (which don't talk about memory usage). "The system crashed" example is fun too. All pure functions must return a value, right? Well, that's obviously not gong to be the case if the computer blows up halfway through executing a pure function. "Blowing up" might not be something your type system talks about—Haskell does to some degree (with _|_ inhabiting every type), but Idris for example has total functions which at runtime could most definitely be interrupted by a sudden explosion. They are "total" only with respect to a set of axioms which imply an execution model where computers do not explode mid-program.
      - jcora 8y ago
        This can be done, for example ST in Idris which lets you reason about resources (check out linear types). However, if you are thinking more in the direction of "you have to reason about where and how exactly your values and functions are stored", you're moving back to C, because the entire point is to disentangle the formal description of computation, from it's actual execution in the real world. If you want to deal with that, you have to do it explicitly and _by reasoning about it_ (with ST, for example). Which is what purity means. > They are "total" only with respect to a set of axioms which imply an execution model where computers do not explode mid-program "There is a chance that the computer blows up" is one of those things that have little bearing when reasoning about programs, it's just not in the domain of discourse. It certainly has no formal bearing on the notion of totality, mathematics just doesn't deal with cases such as "what if everyone who counted to 5 suddenly died", it deals with the counting itself. When the chance is actually high, for example radiation in space flipping bits, I'm pretty sure you want to handle that elsewhere. It's not hard to imagine a fault-tolerance system gaining a lot from dependent types, however, with their ability to prove that your code follows a defined protocol.
- rujuladanh 8y ago
  Yes, yes, of course. All my C programs are pure too! They are a simple mapping of a tuple (hardware state, queue of world events) onto itself! Truly marvelous! Vive la pureté! PS. I am now working on abstracting this further, and I just realized the universe itself is pure too; but somehow I got some strange behaviors when I started to look into particles too closely... will report back soon.
  - DonHopkins 8y ago
    Weren't all Java programs supposed to be "100% Pure" a while back? Whatever happened to Sun Microsystems' "100% Pure Java" [TM] Initiative? https://www.oracle.com/technetwork/java/100percentpurejavacookbook-4-1-1-150165.pdf https://www.oracle.com/technetwork/java/100percentpurejavaco... >[...] 100% Pure Java, JavaStar, JavaPureCheck, [...] JavaSpin, HotJava, The Network Is The Computer, and JavaStation are trademarks or registered trademarks of Sun Microsystems, Inc. in the U.S. and certain other countries. Registering purity as your trademark and insisting that all of your users rewrite every bit of their existing legacy code in your pure language, and never use or talk to any other languages ever again, always seemed like separatist linguistic supremacy to me. Apparently, C#'s P/Invoke is an evil impure cross-language conspiracy to dilute our linguistic purity and sap our precious bodily fluids, breeding caravans of mongrel coders who will swarm across our open borders and steal our jobs. That's why JNI and NDK are only used by unpatriotic second class citizens with divided loyalties, so they don't deserve to be well supported or maintained. https://www.zdnet.com/article/100-pure-java-initiative-wins-100-supporters/ https://www.zdnet.com/article/100-pure-java-initiative-wins-... >"Keep Java pure" is the message behind Sun Microsystems' 100% Pure Java initiative which has already won support from 100 developers but will lock out programs such as Visual J++. The move is an attempt on behalf of the Californian firm to maintain integrity of Java code and build awareness. https://www.cnet.com/news/100-pure-java-watered-down/ https://www.cnet.com/news/100-pure-java-watered-down/ >Viewers of cable news network MSNBC may recently have seen a commercial for Sun Microsystems (SUNW) in which a man tells a priest that he's been thinking "pure" thoughts. When the beatific man exits the confessional, he passes a queue of anxious programmers--one wearing a Visual Basic shirt--ready to admit their sins. >The commercial, which touts Sun's "100 percent pure Java" campaign, is not your usual television ad. But Sun has in many ways shown an almost religious determination to spread the gospel of Java to the far reaches of the globe, even sponsoring a worldwide educational tour for programmers with the support of Netscape Communications, IBM, and Novell.
- mastor 7y ago
  wow. I find it very sad that most people don't grok what pure means. The statement "no one writes pure functional programs. I mean, because they don't exist." is just wrong by any stretch of the imagination. But at the same time, it's not that surprising, it's not something that comes to us humans naturally. The only way to learn it is to do it. This is something I highly recommend to everyone, you'll find the experience incredibly rewarding.

jcora 8y ago

This is actually not at all pedantic but a very fundamental, if subtle at first glance, point about purity. Once you start doing more advanced monadic programming it stops being subtle at all. Many people, yes "even on HN", are totally fooled by do notation and the imperative nomenclature, but there is nothing similar. You misunderstand it as well: it has nothing to do with evaluation mode. Idris is eagerly evaluated, for example, and _that function is still pure_! `f x = putStrLn x` gets "finally" evaluated and yes there is still no side effect. It is so evaluated that you can bind it to a variable and apply another function on it. Just like 2^100 is a pure expression, so is `putStrLn "hello"`. > It is clear OP meant a program as in an entire non-trivial system, not individual functions; even if they are programs themselves. It is not clear. Does he mean including the OS and hardware? Because no matter how complex, a pure program is still pure.

simonh 8y ago
Ok so run up an embedded OS and application on a system with limited resources so that all the memory is being used. Now run your pure functional program. The system crashes. Using memory is a side effect. Consuming CPU time is a side effect. Heating up the environment and drawing power due to that CPU usage is a side effect[0]. These are not trivial either, actual real systems used for critical activities fall prey to this sort of thing all the time. It just depends on what you are willing to consider as a side effect. [0]https://xkcd.com/1172/ https://xkcd.com/1172/
- jcora 8y ago
  That's not what purity refers to! We're talking about a mathematical property of the language itself. The real issue is that people don't understand that `putStrLn "hello"` _is literally just as pure as `2*x`_. They are both like mathematical expressions in that they evaluate to a value and _nothing else_. The name "putStrLn" _suggests_ that this is similar to a print statement but it is emphatically not. You can evaluate it a billion times and nothing gets printed.
  - matt_kantor 8y ago
    Hang on a minute. The only difference is that the languages you are talking about have captured "doing I/O" as something that can be statically reasoned about, but not "consuming memory" (for example). From a mathematical perspective, one is part of the axioms while another is not. One could imagine a language where all memory allocation must be done explicitly via a monad, just like how in Haskell all I/O is performed inside an IO monad. If that were the case, you could have additional static guarantees about how memory is used. That doesn't mean that languages which don't do this are somehow inherently "impure"; they are simply "pure with respect to a certain set of axioms" (which don't talk about memory usage). "The system crashed" example is fun too. All pure functions must return a value, right? Well, that's obviously not gong to be the case if the computer blows up halfway through executing a pure function. "Blowing up" might not be something your type system talks about—Haskell does to some degree (with _|_ inhabiting every type), but Idris for example has total functions which at runtime could most definitely be interrupted by a sudden explosion. They are "total" only with respect to a set of axioms which imply an execution model where computers do not explode mid-program.
    - jcora 8y ago
      This can be done, for example ST in Idris which lets you reason about resources (check out linear types). However, if you are thinking more in the direction of "you have to reason about where and how exactly your values and functions are stored", you're moving back to C, because the entire point is to disentangle the formal description of computation, from it's actual execution in the real world. If you want to deal with that, you have to do it explicitly and _by reasoning about it_ (with ST, for example). Which is what purity means. > They are "total" only with respect to a set of axioms which imply an execution model where computers do not explode mid-program "There is a chance that the computer blows up" is one of those things that have little bearing when reasoning about programs, it's just not in the domain of discourse. It certainly has no formal bearing on the notion of totality, mathematics just doesn't deal with cases such as "what if everyone who counted to 5 suddenly died", it deals with the counting itself. When the chance is actually high, for example radiation in space flipping bits, I'm pretty sure you want to handle that elsewhere. It's not hard to imagine a fault-tolerance system gaining a lot from dependent types, however, with their ability to prove that your code follows a defined protocol.
rujuladanh 8y ago
Yes, yes, of course. All my C programs are pure too! They are a simple mapping of a tuple (hardware state, queue of world events) onto itself! Truly marvelous! Vive la pureté! PS. I am now working on abstracting this further, and I just realized the universe itself is pure too; but somehow I got some strange behaviors when I started to look into particles too closely... will report back soon.
- DonHopkins 8y ago
  Weren't all Java programs supposed to be "100% Pure" a while back? Whatever happened to Sun Microsystems' "100% Pure Java" [TM] Initiative? https://www.oracle.com/technetwork/java/100percentpurejavacookbook-4-1-1-150165.pdf https://www.oracle.com/technetwork/java/100percentpurejavaco... >[...] 100% Pure Java, JavaStar, JavaPureCheck, [...] JavaSpin, HotJava, The Network Is The Computer, and JavaStation are trademarks or registered trademarks of Sun Microsystems, Inc. in the U.S. and certain other countries. Registering purity as your trademark and insisting that all of your users rewrite every bit of their existing legacy code in your pure language, and never use or talk to any other languages ever again, always seemed like separatist linguistic supremacy to me. Apparently, C#'s P/Invoke is an evil impure cross-language conspiracy to dilute our linguistic purity and sap our precious bodily fluids, breeding caravans of mongrel coders who will swarm across our open borders and steal our jobs. That's why JNI and NDK are only used by unpatriotic second class citizens with divided loyalties, so they don't deserve to be well supported or maintained. https://www.zdnet.com/article/100-pure-java-initiative-wins-100-supporters/ https://www.zdnet.com/article/100-pure-java-initiative-wins-... >"Keep Java pure" is the message behind Sun Microsystems' 100% Pure Java initiative which has already won support from 100 developers but will lock out programs such as Visual J++. The move is an attempt on behalf of the Californian firm to maintain integrity of Java code and build awareness. https://www.cnet.com/news/100-pure-java-watered-down/ https://www.cnet.com/news/100-pure-java-watered-down/ >Viewers of cable news network MSNBC may recently have seen a commercial for Sun Microsystems (SUNW) in which a man tells a priest that he's been thinking "pure" thoughts. When the beatific man exits the confessional, he passes a queue of anxious programmers--one wearing a Visual Basic shirt--ready to admit their sins. >The commercial, which touts Sun's "100 percent pure Java" campaign, is not your usual television ad. But Sun has in many ways shown an almost religious determination to spread the gospel of Java to the far reaches of the globe, even sponsoring a worldwide educational tour for programmers with the support of Netscape Communications, IBM, and Novell.
mastor 7y ago
wow. I find it very sad that most people don't grok what pure means. The statement "no one writes pure functional programs. I mean, because they don't exist." is just wrong by any stretch of the imagination. But at the same time, it's not that surprising, it's not something that comes to us humans naturally. The only way to learn it is to do it. This is something I highly recommend to everyone, you'll find the experience incredibly rewarding.