15 ms·

Because how else would you implement Agda? Hah! The idea of managing side effects as a type (monads) still hasn't seemed compelling to me in terms of developme

by codemac 13y ago

Because how else would you implement Agda? Hah! The idea of managing side effects as a type (monads) still hasn't seemed compelling to me in terms of development time. Here I agree with Liskov in saying that it's a bit over the top[0]. Most of the quality I see with Haskell has to do with strict types, not the handling of I/O errors as types themselves. Not that I want to bash it.. Learning haskell has actively changed how I approach all my C/C++ development, and gotten me far far far into the weeds of now learning Agda as a prototyping language for designs/semantics[1]. The world may or may not need Haskell. However it's certainly a better place now that it has it. [0]: She said this at a talk she gave at work.. It was similar or the same as her "The Power of Abstraction" talk, dunno if she makes the same comment in every presentation though. [1]: http://www.youtube.com/watch?v=vy5C-mlUQ1w http://www.youtube.com/watch?v=vy5C-mlUQ1w

deleted 13y ago
[deleted]
tmoertel 13y ago
The big win of "managing side effects as a type" is not that effectful code gets an IO type but that everything else does not. Thus the lack of IO in a function's type assures you, reliably, that the function does not cause side effects or depend upon the state of the outside universe. This lets you corral effectful code and keep the bulk of your code "pure" and easy to reuse and reason about.
- spullara 13y ago
  I would love to use Haskell for the algorithmic part of my code and some other language for the rest of it. I think that is what he is trying to get across. Just get rid of the IO monad and allow only call calls to Haskell from this other language — similar separation but without all the weirdness (IMHO).
  - Tuna-Fish 13y ago
    Umm, doesn't Haskell sort of provide this with do notation? This is how programming simple things in Haskell feels like to me -- I build a lot of simple pure functions, and then bring them together in do blocks, which feel like a completely different, imperative language.
    - spullara 13y ago
      The fact that you have to use the IO monad, to me, feels like something completely ugly and different from what I get from haskell algorithm wise. IMHO.
      - chongli 13y ago
        I happen to find the IO monad incredibly beautiful and elegant. Haskell lets me define my own control structures for combining IO actions in a far more powerful and elegant manner than other languages.
- lobster_johnson 13y ago
  While that is true, you could have accomplished the same thing through a special syntax that marked a function as "pure", and establishing the constraint that impure functions cannot be called by pure ones. And then only allowed I/O through a set of impure base functions.
  - mwotton 13y ago
    What benefit does that have over what's actually there?
    - lobster_johnson 13y ago
      My point was not to argue that something like that would be better solution, but since you're asking: Having a special syntax would make the learning curve a little shallower for newcomers. And it would simplify certain constructs -- instead of having to lift IO values or using mapM_ or whatever, you could actually deal with the results from impure functions directly, no unwrapping or rewrapping needed. While using the type system to implement an effects system is theoretically elegant, I think it's a beautiful hack that has made the language fussier and more obtuse in practice.
      - fusiongyro 13y ago
        That would certainly be true if purity enforced by monadic I/O were the end of the story, but it isn't. While new users create a lot of hot air about monads and I/O, intermediate-experienced Haskell users just use them for various different purposes and get on with life. At the end of the day most of us have differing opinions on what constitutes simplicity and elegance. It's certainly true that a "pure" annotation like you're proposing is a much smaller change to introduce in an imperative setting. I recollect D or Rust or something is doing this. But in the functional programming context the monadic solution is more general, and a two-function type class with 3 (IIRC) algebraic laws is not considered an overbearing amount of complexity, though there are of course interesting alternatives with their own merits.
        13y ago
- laureny 13y ago
  > Thus the lack of IO in a function's type assures you, reliably, that the function does not cause side effects No. IO is not the only monad encoding side effects.
  - tmoertel 13y ago
    Indeed. To be precise, I should have written that the lack of X in a function's type assures you that the function does not cause X effects.
- dschiptsov 13y ago
  How it so significantly better than using, say, Erlang or CL with a strict self-discipline (separation of impure functions, using appropriate naming conventions, etc.?
  - implicit 13y ago
    Discipline is great, but it's finite and has to come not just from you, but from everyone else on your team as well. The compiler remains vigilant and uncompromising forever. It's best to automate everything you can, and ask your team for discipline only as a last resort.
    - dschiptsov 13y ago
      OK, let's say that it is better first to learn how to make trees with conses and traverse them using maps and folds with null? as a base case, and then enjoy a compiler which won't allow you to "cons" improper element to it.)
      - nightski 13y ago
        Why is this better? I see no obvious reason. Just Cons Nothing values.
seanmcdirmid 13y ago
Tmoertel, your comment is dead for some reason and you might want to talk to the admins.
ghswa 13y ago
I don't agree that managing effects is over the top per se however the use of monads feels over the top for pretty much everything! It's always struck me as strange that value (as in a typical type system) and effects would be controlled through the same system. The type signature of a function and it's effects seem very much orthogonal to me. If we want to be controlling side effects then we really ought to be using a separate effect system[1]. There's a scala plugin demonstrating this (although I've not tried it)[2]. With separate type and effect systems I should be able to define a pure function fib(n) and call it like this fib(getValueFromUser()) that is without having to use special operators to get at the value which can only be used in certain contexts a la Haskell. [1] http://en.wikipedia.org/wiki/Effect_system http://en.wikipedia.org/wiki/Effect_system [2] https://github.com/lrytz/efftp/wiki https://github.com/lrytz/efftp/wiki
- gohrt 13y ago
  x = fib(getValueFromUser()) x is not pure, but fib is. OK, the compiler can figure that out without requiring the programmer to write a special "bind" operator. How about this: dofib(argumentProvider) = fib(argumentProvider()) dofib(lambda: 1) // pure difib(getValueFromUser) // effectful Is dofib pure or not? That depends on the value of argumentProvider cannot be determined statically.
  - ghswa 13y ago
    Using the mechanic employed by the scala plugin I linked to[1], dofib would be annotated with pure(argumentProvider). dofib itself is pure however, at each call site, it has the effect of its argument for that call. This is consistent with your example. [1] https://github.com/lrytz/efftp/wiki/Relative-Effects https://github.com/lrytz/efftp/wiki/Relative-Effects edit: That's effectively (sorry!) higher-order effects, behaving just as you'd expect.
  - Silhouette 13y ago
    Is dofib pure or not? Food for thought: 1. The easy but limited solution is that this code doesn't compile, because argumentProvider must have a single type/effect and you couldn't have both a pure and an impure function with that type/effect. 2. Is purity that important? Ultimately we care about avoiding our programs doing unintended things, and often effects are just fine as long as they don't misbehave in some way. Purity is a means to an end. 3. It's fascinating to extend the ideas of generic programming from mainstream type systems to effect systems. I suspect there is a lot of potential benefit to be had if we can figure out how to do this without introducing a lot of boilerplate code, in the same way that we can write code using generic types to various degrees today but have type inference spare us a lot of keyboard bashing.
nilkn 13y ago
Monads don't really have much to do with IO. It's up in the air whether IO really even is a monad. See Conal Elliot's answer on SO and the link he provides: http://stackoverflow.com/a/16444789/65799 http://stackoverflow.com/a/16444789/65799
- marshray 13y ago
  You mean...all this time... ! Reminds me of the story of the old monk who emerges from the basement of the monestary holding an ancient parchment. Tears are streaming down his face. The student asks "What's wrong?" The old monk replies "All this time! We were supposed to be celebRate!"
- duaneb 13y ago
  I just assumed IO meant mutation.
- Zak 13y ago
  A thing that people are often unaware of when trying to understand how the IO type works in Haskell is that you cannot define the IO type in Haskell.
  - kenko 13y ago
    Sure you can: http://hackage.haskell.org/packages/archive/ghc-prim/0.2.0.0/doc/html/src/GHC-Types.html#IO http://hackage.haskell.org/packages/archive/ghc-prim/0.2.0.0... You can't define RealWorld, though, nor (IIRC) is IO really a state monad.
    - Zak 13y ago
      I used "define" imprecisely. You cannot, so far as I know, implement `>>=` for the IO type defined in the above link within Haskell, which means you can't actually use it to do IO.
      - kenko 13y ago
        http://www.haskell.org/ghc/docs/latest/html/libraries/base/src/GHC-Base.html#returnIO http://www.haskell.org/ghc/docs/latest/html/libraries/base/s...
implicit 13y ago
I'm having fantastic success with a custom IO-like monad that lets me statically verify that my unit test suite is totally side effect free. I don't have to resort to documentation or code reviews to ensure that my teammates write fast, reliable tests. This isn't possible in a language that doesn't restrict side effects.

by codemac 13y ago

deleted 13y ago

[deleted]

tmoertel 13y ago

The big win of "managing side effects as a type" is not that effectful code gets an IO type but that everything else does not. Thus the lack of IO in a function's type assures you, reliably, that the function does not cause side effects or depend upon the state of the outside universe. This lets you corral effectful code and keep the bulk of your code "pure" and easy to reuse and reason about.

spullara 13y ago
I would love to use Haskell for the algorithmic part of my code and some other language for the rest of it. I think that is what he is trying to get across. Just get rid of the IO monad and allow only call calls to Haskell from this other language — similar separation but without all the weirdness (IMHO).
- Tuna-Fish 13y ago
  Umm, doesn't Haskell sort of provide this with do notation? This is how programming simple things in Haskell feels like to me -- I build a lot of simple pure functions, and then bring them together in do blocks, which feel like a completely different, imperative language.
  - spullara 13y ago
    The fact that you have to use the IO monad, to me, feels like something completely ugly and different from what I get from haskell algorithm wise. IMHO.
    - chongli 13y ago
      I happen to find the IO monad incredibly beautiful and elegant. Haskell lets me define my own control structures for combining IO actions in a far more powerful and elegant manner than other languages.
lobster_johnson 13y ago
While that is true, you could have accomplished the same thing through a special syntax that marked a function as "pure", and establishing the constraint that impure functions cannot be called by pure ones. And then only allowed I/O through a set of impure base functions.
- mwotton 13y ago
  What benefit does that have over what's actually there?
  - lobster_johnson 13y ago
    My point was not to argue that something like that would be better solution, but since you're asking: Having a special syntax would make the learning curve a little shallower for newcomers. And it would simplify certain constructs -- instead of having to lift IO values or using mapM_ or whatever, you could actually deal with the results from impure functions directly, no unwrapping or rewrapping needed. While using the type system to implement an effects system is theoretically elegant, I think it's a beautiful hack that has made the language fussier and more obtuse in practice.
    - fusiongyro 13y ago
      That would certainly be true if purity enforced by monadic I/O were the end of the story, but it isn't. While new users create a lot of hot air about monads and I/O, intermediate-experienced Haskell users just use them for various different purposes and get on with life. At the end of the day most of us have differing opinions on what constitutes simplicity and elegance. It's certainly true that a "pure" annotation like you're proposing is a much smaller change to introduce in an imperative setting. I recollect D or Rust or something is doing this. But in the functional programming context the monadic solution is more general, and a two-function type class with 3 (IIRC) algebraic laws is not considered an overbearing amount of complexity, though there are of course interesting alternatives with their own merits.
      - 13y ago
laureny 13y ago
> Thus the lack of IO in a function's type assures you, reliably, that the function does not cause side effects No. IO is not the only monad encoding side effects.
- tmoertel 13y ago
  Indeed. To be precise, I should have written that the lack of X in a function's type assures you that the function does not cause X effects.
dschiptsov 13y ago
How it so significantly better than using, say, Erlang or CL with a strict self-discipline (separation of impure functions, using appropriate naming conventions, etc.?
- implicit 13y ago
  Discipline is great, but it's finite and has to come not just from you, but from everyone else on your team as well. The compiler remains vigilant and uncompromising forever. It's best to automate everything you can, and ask your team for discipline only as a last resort.
  - dschiptsov 13y ago
    OK, let's say that it is better first to learn how to make trees with conses and traverse them using maps and folds with null? as a base case, and then enjoy a compiler which won't allow you to "cons" improper element to it.)
    - nightski 13y ago
      Why is this better? I see no obvious reason. Just Cons Nothing values.

seanmcdirmid 13y ago

Tmoertel, your comment is dead for some reason and you might want to talk to the admins.

ghswa 13y ago

I don't agree that managing effects is over the top per se however the use of monads feels over the top for pretty much everything! It's always struck me as strange that value (as in a typical type system) and effects would be controlled through the same system. The type signature of a function and it's effects seem very much orthogonal to me. If we want to be controlling side effects then we really ought to be using a separate effect system[1]. There's a scala plugin demonstrating this (although I've not tried it)[2]. With separate type and effect systems I should be able to define a pure function fib(n) and call it like this fib(getValueFromUser()) that is without having to use special operators to get at the value which can only be used in certain contexts a la Haskell. [1] http://en.wikipedia.org/wiki/Effect_system http://en.wikipedia.org/wiki/Effect_system [2] https://github.com/lrytz/efftp/wiki https://github.com/lrytz/efftp/wiki

gohrt 13y ago
x = fib(getValueFromUser()) x is not pure, but fib is. OK, the compiler can figure that out without requiring the programmer to write a special "bind" operator. How about this: dofib(argumentProvider) = fib(argumentProvider()) dofib(lambda: 1) // pure difib(getValueFromUser) // effectful Is dofib pure or not? That depends on the value of argumentProvider cannot be determined statically.
- ghswa 13y ago
  Using the mechanic employed by the scala plugin I linked to[1], dofib would be annotated with pure(argumentProvider). dofib itself is pure however, at each call site, it has the effect of its argument for that call. This is consistent with your example. [1] https://github.com/lrytz/efftp/wiki/Relative-Effects https://github.com/lrytz/efftp/wiki/Relative-Effects edit: That's effectively (sorry!) higher-order effects, behaving just as you'd expect.
- Silhouette 13y ago
  Is dofib pure or not? Food for thought: 1. The easy but limited solution is that this code doesn't compile, because argumentProvider must have a single type/effect and you couldn't have both a pure and an impure function with that type/effect. 2. Is purity that important? Ultimately we care about avoiding our programs doing unintended things, and often effects are just fine as long as they don't misbehave in some way. Purity is a means to an end. 3. It's fascinating to extend the ideas of generic programming from mainstream type systems to effect systems. I suspect there is a lot of potential benefit to be had if we can figure out how to do this without introducing a lot of boilerplate code, in the same way that we can write code using generic types to various degrees today but have type inference spare us a lot of keyboard bashing.

nilkn 13y ago

Monads don't really have much to do with IO. It's up in the air whether IO really even is a monad. See Conal Elliot's answer on SO and the link he provides: http://stackoverflow.com/a/16444789/65799 http://stackoverflow.com/a/16444789/65799

marshray 13y ago
You mean...all this time... ! Reminds me of the story of the old monk who emerges from the basement of the monestary holding an ancient parchment. Tears are streaming down his face. The student asks "What's wrong?" The old monk replies "All this time! We were supposed to be celebRate!"
duaneb 13y ago
I just assumed IO meant mutation.
Zak 13y ago
A thing that people are often unaware of when trying to understand how the IO type works in Haskell is that you cannot define the IO type in Haskell.
- kenko 13y ago
  Sure you can: http://hackage.haskell.org/packages/archive/ghc-prim/0.2.0.0/doc/html/src/GHC-Types.html#IO http://hackage.haskell.org/packages/archive/ghc-prim/0.2.0.0... You can't define RealWorld, though, nor (IIRC) is IO really a state monad.
  - Zak 13y ago
    I used "define" imprecisely. You cannot, so far as I know, implement `>>=` for the IO type defined in the above link within Haskell, which means you can't actually use it to do IO.
    - kenko 13y ago
      http://www.haskell.org/ghc/docs/latest/html/libraries/base/src/GHC-Base.html#returnIO http://www.haskell.org/ghc/docs/latest/html/libraries/base/s...

implicit 13y ago

I'm having fantastic success with a custom IO-like monad that lets me statically verify that my unit test suite is totally side effect free. I don't have to resort to documentation or code reviews to ensure that my teammates write fast, reliable tests. This isn't possible in a language that doesn't restrict side effects.