5 ms·

I should have indeed said algebraic effects instead of effects system. Algebraic effects are a restriction on monads, but a restriction that still allows for t

by cultus 8y ago

I should have indeed said algebraic effects instead of effects system. Algebraic effects are a restriction on monads, but a restriction that still allows for the vast majority of use cases. In return, you get composability and a clear separation of effectful operations and effect handling. The default of using monads for everything produces too much cognitive complexity for little benefit.

dwohnitmok 8y ago
Hmm... What do you mean by a restriction on monads? Algebraic effects basically mean that you live in a single monad that can be either widened or narrowed via new effects or new handlers respectively. I'm also not sure what you mean by "using monads for everything." Monads are basically just flatten and map. It sounds kind of like "you're using map for everything" to which the answer seems something along the lines of, well in a lot of places where you use map, if you didn't use map, you'd probably just reinvent it.
- cultus 8y ago
  >Algebraic effects basically mean that you live in a single monad that can be either widened or narrowed via new effects or new handlers respectively. Yep, it is a restriction as I said. Algebraic effects basically live inside the free monad, so that's what I meant by that. This restriction, versus using separate Writer, IO, etc, monads, is far more easy to reason about. Types in Haskell become insane with monad transformers. It produces code that is difficult to understand and reuse. edit: Algebraic effects can also be derived from delimited continuations.
  - dwohnitmok 8y ago
    Maybe I'm just getting hung up on the word restriction. In particular is there any monad that cannot be expressed as a pair of algebraic effects and handlers? I think the answer is no (potentially barring especially magical monads such as IO in its full generality), but I'm not sure. Totally agree about the brittle and type-soup nature of transformer-heavy code.
- dan-robertson 8y ago
  Algebraic effects (at least in multi core ocaml) are a restriction on monads because the function passed to bind in a monad may be run multiple times whereas the equivalent continuation after some effect may only be run once. Therefore one cannot use algebraic effects to eg do the equivalent of what the list monad does.
  - dwohnitmok 8y ago
    Hmm... Maybe I need to look at multi-core OCaml more closely, but I don't think it's true in general of algebraic effects (or at least its freer monad variants), as in I'm pretty sure I can emulate a list using them. In particular I'm pretty sure I can do that with `Cont` alone.
    - fmap 8y ago
      You're right, the linearity restriction on the handler continuation is a peculiarity of multi-core OCaml and really more of an implementation detail. However, it is also true that you cannot encode, e.g., the continuation monad using (typed) algebraic effects. The precise relationship isn't that simple, but this paper: https://arxiv.org/abs/1610.09161 analyzes a particular setting in detail.

by cultus 8y ago

dwohnitmok 8y ago

Hmm... What do you mean by a restriction on monads? Algebraic effects basically mean that you live in a single monad that can be either widened or narrowed via new effects or new handlers respectively. I'm also not sure what you mean by "using monads for everything." Monads are basically just flatten and map. It sounds kind of like "you're using map for everything" to which the answer seems something along the lines of, well in a lot of places where you use map, if you didn't use map, you'd probably just reinvent it.

cultus 8y ago
>Algebraic effects basically mean that you live in a single monad that can be either widened or narrowed via new effects or new handlers respectively. Yep, it is a restriction as I said. Algebraic effects basically live inside the free monad, so that's what I meant by that. This restriction, versus using separate Writer, IO, etc, monads, is far more easy to reason about. Types in Haskell become insane with monad transformers. It produces code that is difficult to understand and reuse. edit: Algebraic effects can also be derived from delimited continuations.
- dwohnitmok 8y ago
  Maybe I'm just getting hung up on the word restriction. In particular is there any monad that cannot be expressed as a pair of algebraic effects and handlers? I think the answer is no (potentially barring especially magical monads such as IO in its full generality), but I'm not sure. Totally agree about the brittle and type-soup nature of transformer-heavy code.
dan-robertson 8y ago
Algebraic effects (at least in multi core ocaml) are a restriction on monads because the function passed to bind in a monad may be run multiple times whereas the equivalent continuation after some effect may only be run once. Therefore one cannot use algebraic effects to eg do the equivalent of what the list monad does.
- dwohnitmok 8y ago
  Hmm... Maybe I need to look at multi-core OCaml more closely, but I don't think it's true in general of algebraic effects (or at least its freer monad variants), as in I'm pretty sure I can emulate a list using them. In particular I'm pretty sure I can do that with `Cont` alone.
  - fmap 8y ago
    You're right, the linearity restriction on the handler continuation is a peculiarity of multi-core OCaml and really more of an implementation detail. However, it is also true that you cannot encode, e.g., the continuation monad using (typed) algebraic effects. The precise relationship isn't that simple, but this paper: https://arxiv.org/abs/1610.09161 analyzes a particular setting in detail.