One often cited benefit of pure functional programming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions with the outside world. Haskell solves this problem using monads to capture details of possibly side-effecting computations â it provides monads for capturing State, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects.
Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.
> monad transformers for combining multiple effects.
This is a Haskell problem, not the fundamental one.
doFiles::forall e. Eff (fs::FS, console::CONSOLE|e) Unit doHttp::forall e. Eff (http::HTTP, console::CONSOLE|e) Unit
doStuff::forall e. Eff (fs::FS, console::CONSOLE, http::HTTP|e) Unit doFiles <<< doHTTP
You can also handle effect, which means you remove the effect from the row and once you get to the Eff () you can runPure and transform the effectful computation into the pure one. Bingo.
More like IO with refinement on top of it, innit? But there are other encodings of effects that do not involve monads and, according to rumour, are composable (for some values thereof). I believe F* featured something like that, they even had Div or somesuch for divergence.
Yes, parameterized by list (set?) of effects that occurred. I think this should be possible in Haskell too, with some existing or plausible extension. Need to think about it.
DataKinds and friends should be enough methinks, at least for a rough approximation of this. Is type inference for this decidable, though? Type checking should be.
Yes, it does. But it is parametrized with either an open or closed row of effects and thus Eff (console::CONSOLE) doesn't compose with Eff (fs::FS). By opening and closing the row and adding and removing effects I can control the composability. This is also not fine-grained enough (esp. with the "inflation of effects" when everybody and their grandmother invents new type of effect which implicitly may include others) but it's much, MUCH, more fine-grained than IO() which is just "some IO" who knows what it does.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
juan_gandhi) wrote2016-08-17 01:10 pm
no subject
Ðе знаÑ, можно ли поÑÑиÑаÑÑ ÑÑ
One often cited benefit of pure functional programming is that pure code is easier to test and reason about, both formally and informally.
However, real programs have side-effects including state management, exceptions and interactions with the outside world.
Haskell solves this problem using monads to capture details of possibly side-effecting computations â it provides monads for capturing State, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects.
Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use
this approach to reason about states in effectful programs.
Re: Ðе знаÑ, можно ли поÑÑиÑаÑÑ Ñ
Re: Ðе знаÑ, можно ли поÑÑиÑаÑÑ Ñ
Monads do not, but effects perfectly do as soon as you get effect rows.
Re: Ðе знаÑ, можно ли поÑÑиÑаÑÑ Ñ
This is a Haskell problem, not the fundamental one.
doFiles::forall e. Eff (fs::FS, console::CONSOLE|e) Unit
doHttp::forall e. Eff (http::HTTP, console::CONSOLE|e) Unit
doStuff::forall e. Eff (fs::FS, console::CONSOLE, http::HTTP|e) Unit
doFiles <<< doHTTP
You can also handle effect, which means you remove the effect from the row and once you get to the Eff () you can runPure and transform the effectful computation into the pure one. Bingo.
RE: Re: Ðе знаÑ, можно ли поÑÑиÑаÑÑ
no subject
no subject
no subject
Re: Re: Ðе знаÑ, можно ли поÑÑиÑаÑÑ
Re: Re: Ðе знаÑ, можно ли поÑÑиÑаÑÑ