# Eff 3.0

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!

## 4 thoughts on “Eff 3.0”

1. Dan Doel says:

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?

2. @Dan: you raise an important question, and it is important to understand the answer: the equations have no place in Eff. The equations are about what is expected of 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.