Matija and I are pleased to announce a new major release of the eff programming language.

In the last year or so eff has matured considerably:

- It now looks and feels like OCaml, so you won’t have to learn yet another syntax.
- It has static typing with parametric polymorphism and type inference.
- Eff now clearly separates three basic concepts: effect types, effect instances, and handlers.
- How eff works is explained in our paper on Programming with Algebraic Effects and Handlers.
- We moved the source code to GitHub, so go ahead and fork it!

A question asked in #haskell a few days back sparked some thinking about Eff for me. The question was:

Why can’t we use a free monad over

`F X = Get (S -> X) | Put S X`

for state?The answer is that this isn’t specifying the algebra of a mutable cell precisely, whereas

`S -> S * X`

does. We want Get and Put to interact in certain ways, and the proper algebraic theory is a quotient of the free algebraic theory over the two operations.But, it occurred to me that the free monad is exactly what Eff does. You specify that get and put exist, but there is no relation between them, unless I’m missing something. And presumably the handlers would be able to observe various sequences of gets and puts that would be indistinguishable under the quotient?

So, are there plans to add equations (or some equivalent) to the algebraic theories in Eff. Or is my recollection of what all is possible in Eff just fuzzy, and there is already a way to handle this properly?

@Dan: you raise an important question, and it is important to understand the answer: the equations

have no placein Eff. The equations are about what isexpectedof a correct implementation, i.e., they are specifications. Equations do not tell us how to compute things (except in the lucky case when they can be directed so that they become reduction rules). How is Eff, or any other language, supposed to enforce equations?In your concrete example, the relation between

`Put`

and`Get`

is captured by the handler which handles them. There are many handlers, some of which satisfy the expected equations. Those can be said to be correct for the given equations.I do not undertand your last sentence about fuzziness.

There are plenty of languages that allow you to state and enforce equations. Most dependently typed languages, for instance. Also Maude, I believe. And Neel Krishnaswami has a paper on adding equations to System F. I don’t know that any of that would be suitable for Eff, though.

In the specific example, state algebras are characterized by the typical state monad, and the free state algebra over a type A is S -> S * A. So if handlers are homomorphisms from a free algebra to another algebra, then that should be their source for the equation-incorporating state case. However I don’t know how to determine this from the operations + equations; it doesn’t seems like a tractable problem. And even were that solved, ensuring that the target is an algebra and that the definition is a proper homomorphism probably isn’t automatic.

The fuzziness sentence was just hedging against my having forgotten some feature of Eff that let you specify equations somehow. It’s been a while since I read about it.

Ah yes. Eff is a programming language in the traditional sense of the word, under which Coq, Agda, etc., are proof assistants and not programming languages.

Perhaps it is useful to think of things in the following way: in Eff the valid equations are those induced by handlers. Does that make you happier?