Adding an Effect System to OCaml [video] | Hacker News Reader

Adding an Effect System to OCaml [video]

janestreet.com

152 pointstosh21 comments

If someone wants to try running `ocaml-multicore` there is an opam repository available [1].

I am currently doing the exercises from the "ocaml-effects-tutorial"[2]. This is the first introduction i've had to algebraic affects and the exercises are a fun way to play around with some code as I try to improve my understanding of how one might use the effect system.

[1] https://github.com/ocamllabs/multicore-opam

[2] https://github.com/ocamllabs/ocaml-effects-tutorial

I'm glad to see effect systems getting so much attention lately. I think they are a far better alternative to monads (and monad transformers) in terms of cognitive load. They commute, for example.

Apart from the sibling conmment pointing out that effect monads are one type of effect system, almost all effect systems I know of (algebraic effects included) have a monadic interface. The only one I can think of that doesn't is the family of uniqueness/linear/affine types (to the extent that those model certain kinds of effects).

Maybe you were mainly just thinking of monad transformers or combining discrete monads?

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.

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.

>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.

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.

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.

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.

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.

Definitely not as popular, but Arrow-ized effect systems are an interesting area that I've seen people exploring more lately.

Jake Keuhlen spoke about it at LambdaConf this year [0] [1], and John De Goes spoke a bit on the notion of Arrow-ized IO in the `zio` library for Scala that offers an alternative interface for `IO` effects [2].

Will Fancher has also written a bit on the concept of "Free Arrows", but it's a much deeper dive (IMO) than the previous resources [3].

[0] Keuhlen's Repo: https://github.com/jkeuhlen/talks/tree/master/extensibly-fre...

[1] Keulen's Slides: https://github.com/jkeuhlen/talks/blob/master/Extensibly%20F...

[2] https://github.com/scalaz/scalaz-zio/blob/master/core/shared...

[3] https://elvishjerricco.github.io/2017/03/10/profunctors-arro...

I don’t understand what you mean by “monadic interface.” Could you elaborate on that please?

I just meant that you usually still end up using the equivalent of bind to compose things and pure to lift non-effectful code. I was thinking mainly of the free and freer monad here, but I think it applies generally.

You mean algebraic effects? Monad transformers are an effect system as well.

Can you give an example/link of how they commute?

Eff is a language based on algebraic effects. They show some good examples. It's pretty cool.

https://www.eff-lang.org/

For those interested in effect systems, here is a description of the effect system in Nim: https://nim-lang.org/docs/manual.html#effect-system

I'm very interested in Nim's effect system. I have a few questions about it:

* Does it have a way to define effect handlers in a decoupled way from the effects? I'm looking for something like this: https://koka-lang.github.io/koka/doc/kokaspec.html#sec-a-pri...

* Are all standard library procs marked with all their actual effects?

* How complete is compile-time effect tracking right now? For example, the following doesn't raise a compile error:

    proc testEffects() {.tags: [].} = "hi".echo
    testEffects()

* Is there a 'strict effect' mode, that would implicitly add `{.tags: [].}` to all proc types without an explicit tags pragma? That would make effect tracking more, well, effective.

Ooo... Interesting! Are these significantly different from Java's checked exceptions (the reader and writer ones look interesting, but unfortunately are not yet implemented)?

Here are some recent (June 2018) slides about multicore OCaml that provide some extra information about effect handlers: http://kcsrk.info/slides/mcocaml_gallium.pdf

I'm excited to see that effect handlers are gaining popularity. I read the original papers that introduced them, and I think that they have a lot of potential.

Reply on news.ycombinator.com