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

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?

I have one question: are there differences between resources and mutable references? Are resources superior to mutables or not?

Resources are slightly more general. You can implemented references using resources, but you can also use resources for other "state-like" things. You can impement lazy values using resources, as well as persistent data structures and self-modifying structures, such as splay trees. Of course, you can do all of this if you have references, too. So in some sense resources and references are equally expressive. Note that there can also be primitive (builtin) resources that actually interact with the environment, such as streams of randomness, or communication channels.