3 ms·

I disagree. I think reasoning in a programming language that limits effects with types and promotes partitioning them from the rest of your logic is dramaticall

by sink 11y ago

I disagree. I think reasoning in a programming language that limits effects with types and promotes partitioning them from the rest of your logic is dramatically simpler than in languages where mutation and effects can happen anywhere.

mpweiher 11y ago
> mutation and effects can happen anywhere. That's a red herring and a scare-story that FPers tell each other. They can't happen "anywhere". They happen where you tell them to happen. Do you have any evidence that actual reasoning is simpler? "At the end you usually get a tight loop that is easy to follow. It is also much more imperative/operational than before, which may bug Haskell-style people." -- Jonathan Blow https://twitter.com/jonathan_blow/status/588007366618062848 https://twitter.com/jonathan_blow/status/588007366618062848 "I wanted to see how hard it was to implement this sort of thing in Go, with as nice an API as I could manage. It wasn't hard. Having written it a couple of years ago, I haven't had occasion to use it once. Instead, I just use "for" loops. You shouldn't use it either." -- Rob Pike https://github.com/robpike/filter https://github.com/robpike/filter This matches my experience pretty well. When I first created Higher Order Messaging, I was also really into creating chained higher order ops. After a little while, I noticed that a small for-loop was actually more readable than the really cool filter-chains I had created. Less cool, but more readable, comprehensible, easier to reason about, not least because of named intermediate values, something that tends to get lost in point-free style (and trust me, having been a heavy user + implementor of Postscript, I know a little about point-free style).
- sink 11y ago
  In a strongly typed functional program I can prove that side effects only happen in specific places that are designated by the types. I have no such assistance in say Java, or Python. That is what I mean that side effects can happen anywhere. I would call referential transparency, which gives rise to equational reasoning, very strong evidence that reasoning becomes simpler.
  - mpweiher 11y ago
    You're still conflating "prove" with "reason". I don't need to prove things about my code in order to reason about it. For example, I can just look at the code in question to know whether it has side effects, and most code doesn't. In fact, most proofs I have seen don't particularly help me reason about the code in question. On the other hand, a simple imperative execution model does help me reason about the code.
    - sink 11y ago
      I don't think I am doing any such conflating. Being able to reason about things equationally makes my code easier to reason about. Having a type system and a compiler assist me makes my code easier to reason about. Having fewer variants makes my code easier to reason about. Not needing to know the order in which functions have been invoked to know their return values makes my code easier to reason about. However, I will make the statement -- and this is indeed conflating! -- If I can prove something about my code, then it is easier to reason about. The proof can be simple or complex.
      - mpweiher 11y ago
        Again, you are just repeating your assertions and somehow think that simply asserting them makes them true. It does not, and I don't think I can make you understand the difference between assertions and evidence, so let's call it a day.
        deleted 11y ago
        [deleted]
        sink 11y ago
        I think my assertions are pretty well accepted virtually ... everywhere, so it didn't really occur to me THOSE specifically were what you were calling into question. But if THAT is what we are arguing about, I agree, this is all rather cyclical and pointless.

by sink 11y ago

mpweiher 11y ago

> mutation and effects can happen anywhere. That's a red herring and a scare-story that FPers tell each other. They can't happen "anywhere". They happen where you tell them to happen. Do you have any evidence that actual reasoning is simpler? "At the end you usually get a tight loop that is easy to follow. It is also much more imperative/operational than before, which may bug Haskell-style people." -- Jonathan Blow https://twitter.com/jonathan_blow/status/588007366618062848 https://twitter.com/jonathan_blow/status/588007366618062848 "I wanted to see how hard it was to implement this sort of thing in Go, with as nice an API as I could manage. It wasn't hard. Having written it a couple of years ago, I haven't had occasion to use it once. Instead, I just use "for" loops. You shouldn't use it either." -- Rob Pike https://github.com/robpike/filter https://github.com/robpike/filter This matches my experience pretty well. When I first created Higher Order Messaging, I was also really into creating chained higher order ops. After a little while, I noticed that a small for-loop was actually more readable than the really cool filter-chains I had created. Less cool, but more readable, comprehensible, easier to reason about, not least because of named intermediate values, something that tends to get lost in point-free style (and trust me, having been a heavy user + implementor of Postscript, I know a little about point-free style).

sink 11y ago
In a strongly typed functional program I can prove that side effects only happen in specific places that are designated by the types. I have no such assistance in say Java, or Python. That is what I mean that side effects can happen anywhere. I would call referential transparency, which gives rise to equational reasoning, very strong evidence that reasoning becomes simpler.
- mpweiher 11y ago
  You're still conflating "prove" with "reason". I don't need to prove things about my code in order to reason about it. For example, I can just look at the code in question to know whether it has side effects, and most code doesn't. In fact, most proofs I have seen don't particularly help me reason about the code in question. On the other hand, a simple imperative execution model does help me reason about the code.
  - sink 11y ago
    I don't think I am doing any such conflating. Being able to reason about things equationally makes my code easier to reason about. Having a type system and a compiler assist me makes my code easier to reason about. Having fewer variants makes my code easier to reason about. Not needing to know the order in which functions have been invoked to know their return values makes my code easier to reason about. However, I will make the statement -- and this is indeed conflating! -- If I can prove something about my code, then it is easier to reason about. The proof can be simple or complex.
    - mpweiher 11y ago
      Again, you are just repeating your assertions and somehow think that simply asserting them makes them true. It does not, and I don't think I can make you understand the difference between assertions and evidence, so let's call it a day.
      - deleted 11y ago
        [deleted]
      - sink 11y ago
        I think my assertions are pretty well accepted virtually ... everywhere, so it didn't really occur to me THOSE specifically were what you were calling into question. But if THAT is what we are arguing about, I agree, this is all rather cyclical and pointless.