Implementing Algebraic Effects in C | Hacker News Reader

Implementing Algebraic Effects in C

microsoft.com

150 pointsnecrodome21 comments

This is super interesting and I'm still going through the paper. For folks with a "Cool, but why" reaction, the introduction elaborates:

  For example, the P language [10] is a language for describing verifiable asyn-
  chronous state machines, and used for example to implement and verify the core
  of the USB device driver stack that ships with Microsoft Windows 8. Compiling
  to C involves a complex CPS-style transformation [19, 26] to enable async/await
  style programming [5] with a receive statement – using the effects library this
  transformation is no longer necessary and we can generate straightforward C
  code instead. Similarly, we hope to integrate this library with libuv [29] (the
  asynchronous C library underlying Node [43]) and improve programming with
  libuv directly from C or C++ using async/await style abstractions [12, 27]

Since the linked abstract doesn't actually mention this practical application, consider this comment as a goad to encourage more people to click through to the paper :)

It should be noted that the previous sentence before your quote is: "For now, we mainly see the library as a target for library writers or compilers."

Your caveat is well-taken, but you can learn a lot from what is done in these fields.

Couldn't these kind of goals also be reached with the upcoming C++ coroutines (also pioneered by Microsoft)? I remember some presentation that those (or at the least the LLVM implementation underneath it) could also be used for C.

A little off-topic, but the author of this paper (Daan Leijen) is also the author of Koka[1], a programming language with algebraic effects.

IMO, Koka (or something similar) has more potential to become a mainstream language than "traditional" FP languages (Haskell, OCaml, Idris, etc.).

Effects seem to be easier to understand than monads (at least on a superficial level) and more modular (I don't have a lot of experience with Haskell, so take that with a grain of salt).

Its syntax is also very close to C-like languages.

Taken from the Koka book[2]:

  fun square1(x : int) : total int {
    return x*x
  }

  fun square2(x : int) : io int {
    println( "a not so secret side-effect" )
    return x*x
  }

`square1` is a pure mathematical function, so its effect is `total`. `square2` has a side-effect because of `println`, so its effect is `io`. This means that `square2` can raise exceptions, not terminate, be non-deterministic, read and write to the heap, and do any input/output operations.

Note that Koka can infer effects, so these annotations are optional.

[1]: https://www.microsoft.com/en-us/research/project/koka/?from=...

[2]: https://koka-lang.github.io/koka/doc/kokaspec.html#sec-effec...

Fwiw, OCaml algebraic effects are being implemented: http://kcsrk.info/ocaml/multicore/2015/05/20/effects-multico...

(And then there's https://reasonml.github.io, which I work on)

Hey there, Reason is a great project! Thanks for working on it!

I actually tried to use it very recently in a new project at my workplace, but unfortunately I decided not to. I found some fundamental things were lacking.

I didn't find documentation about how to interact with npm libraries (e.g. how do I use a websockets library in Reason? Do I have to create my own bindings? If so, how?).

There also seemed to be nothing similar to async/await in Reason/Bucklescript yet and I couldn't find out how to use promises.

I'll definitely reevaluate it in the future. I think it is an awesome project with great potential (along with Bucklescript which is awesome too).

Late reply, but we have such guide here: https://reasonml.github.io/guide/javascript/converting

You can also check the community's work: https://reasonml.github.io/community/

My dream for a language is a type system that can enforce runtime semantics, preferably at import.

  import 'mod::memcmp': O(1);

where O(1) is big O notation.

https://en.wikipedia.org/wiki/Hume_(programming_language)

That would be a very restrictive programming environment, or type checking might fail or produce ridiculously large runtime bounds. It is not decidable whether a given Turing machine has runtime O(n^k) for a particular k, even if you're given the promise that such a k exists.

Could you make it an attribute of the symbol being exported, part of the contract, and use that to derive an estimated cost of the program?

I could see this being used to choose between allocators or schedulers given specific requirements.

I find monads much much more easy to reason about, because they give you a "plain old values" perspective as well as an effectful perspective; most of the time you work like you would with effects, but if you ever get confused you can drop down to seeing what the values are doing. The one mainstream example of something effect-like is Java checked exceptions, which are widely regarded as a failure (and I think for good reason).

Cool talk by Leijen about Koka and algebraic-effects: https://youtu.be/hrBq8R_kxI0

Hi, I am the author of this report -- thank you for the interest :-)

Just wanted to add that you can find the library at: https://github.com/koka-lang/libhandler

The `dev` branch contains a sample of `libuv` integration. There is still a lot to be done in terms of creating a better interface and providing implementations of standard effects but the core is working quite well by now.

Enjoy!

the authors cite Matija Pretnar who has an introduction on [algebraic effects](http://www.eff-lang.org/handlers-tutorial.pdf). I'm reading through it now as I have no idea what is going on :)

Thanks for the link! I'm in the same boat.

If all you want is generators and co-routines, then there's a lot of literature on this for C.

The original Icon compiler compiled to CPS C. That was pretty cool.

One can do much of what Icon did using GCC local functions and computed gotos to get something much closer to not-CPS.

There's Simon Tatham's PuTTY, which uses his co-routine macros, which are an extravagant meta-programming macros around a Duff's device. He also has an extensive set of meta-programming macros as well, not related to co-routines.

Some Schemes compile to C code where all functions always return immediately, but what they return is a continuation, and the top-level is a for(;;) { next = next(); }.

EDIT: I'm particularly fond of PuTTY. Its SSHv2 implementation all the way up to the end of authentication is a single, huge function. It looks completely synchronous, but it's not, because it's actually a co-routine. As a result, and in spite of being a single huge function, it's actually quite readable.

I tried to cite much related work on co-routines and threading libraries in C -- including Simon Tatham's page on co-routines in C [1] -- But I was not yet aware of the work on Icon nor did I know co-routines were used in PuTTY -- thanks! Although now that I reread Simon's page I see he actually mentions PuTTY explicitly :-)

As an aside, I feel algebraic effect handlers are safer to use than most coroutine or shift/reset implementations because they offer more structure. As put by others: "Algebraic Effects+Handlers" are to "delimited continuations" as "while" is to "goto"

[1]: https://www.chiark.greenend.org.uk/~sgtatham/coroutines.html

Algebraic effects are a hot topic. The name sounds fancy but maybe this intuition helps: an effect is like an exception where the exception handler receives enough information to resume the computation from where it was called. Just like exceptions, effects are dynamically scoped: the handler is always found up in the call stack.

Cue smug lispers.

Reply on news.ycombinator.com