Is operational really isomorphic to a free monad?

Question

Proofs

In this blog post, Tekmo makes the point that we can prove that ExitSuccess exits because (I presume) it's like the Const functor for that constructor (it doesn't carry the x so fmap behaves like const).

With the operational package, Tekmo's TeletypeF might be translated something like this:

data TeletypeI a where     PutStrLn :: String -> TeletypeI ()     GetLine :: TeletypeI String     ExitSuccess :: TeletypeI () 

I've read that operational is isomorphic to a free monad, but can we prove here that ExitSuccess exits? It seems to me that it suffers from exactly the same problem as exitSuccess :: IO () does, and in particular if we were to write an interpreter for it, we'd need to write it like as if it didn't exit:

eval (ExitSuccess :>>= _) = exitSuccess 

Compare to the free monad version which doesn't involve any pattern wildcard:

run (Free ExitSuccess) = exitSuccess 

Laziness

In the Operational Monad Tutorial apfelmus mentions a drawback:

The state monad represented as s -> (a,s) can cope with some infinite programs like

evalState (sequence . repeat . state $ \s -> (s,s+1)) 0 

whereas the list of instructions approach has no hope of ever handling that, since only the very last Return instruction can return values.

Is this true for free monads as well?

Answer 1

(Allow me to scoop the grand prize by boldly combining the previous answers. ;-))

The key observation is this: Prove what exactly? The formulation in terms of Free TeletypeF allows us to prove the following:

Every interpreter for programs of type Free TeletypeF a must exit when it encounters the ExitSuccess instruction. In other words, we automatically get the algebraic law

 interpret (exitSuccess >>= k) = interpret exitSuccess 

Thus, the Free monad actually allows you to bake certain algebraic laws into the type.

In contrast, the operational approach does not constrain the semantics of ExitSuccess, there is no associated algebraic law that pertains to every interpreter. It is possible to write interpreters that exit when encountering this instruction, but it is also possible to write interpreters that don't.

Of course, you can prove that any particular interpreter satisfies the law by inspection, for instance because it uses a wildcard pattern match. Sjoerd Visscher observes that you can also enforce this in the type system by changing the return type of ExitSuccess to Void. However, this doesn't work for other laws that can be baked into free monads, for instance the distributive law for the mplus instruction.

Thus, in a confusing turn of events, the operational approach is more free than the free monad, if you interpret "free" as "the least amount of algebraic laws".

It also means that these data types are not isomorphic. However, they are equivalent: every interpreter written with Free can be transformed into an interpreter written with Program and vice versa.

Personally, I like to put all of my laws into the interpreter, because there are a lot of laws that cannot be baked into the free monad, and I like to have them all in one place.

Answer 2

The answer is yes, but only if you use a different translation of TeletypeF:

data TeletypeI a where     PutStrLn :: String -> TeletypeI ()     GetLine :: TeletypeI String     ExitSuccess :: TeletypeI Void 

The argument of TeletypeI is what the operation will/must provide to the rest of the program. It is the type of the argument of the continuation k in

eval (ExitSuccess :>>= k) = ... 

Since there are no values of type Void, we can be sure that k will never be called. (As always we'll have to ignore undefined here.)

An equivalent type is:

data TeletypeI a where     PutStrLn :: String -> TeletypeI ()     GetLine :: TeletypeI String     ExitSuccess :: TeletypeI a 

Now we would have to provide a value to k that matches any type, and we can't do that either. This can be more practical since singleton ExitSuccess now has the flexible type Program TeletypeI a.

Similarly, exitSuccess could be fixed by giving it the type IO Void, or IO a.