Is operational really isomorphic to a free monad?

问题:

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?

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

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

回答3:

The answer is no, you cannot prove that the operational one ignores the rest of the program on exitSuccess. Contrast TeletypeI with TeletypeF to see why. I'll rewrite TeletypeF in GADT notation for easier comparison

data TeletypeF x where                     | data TeletypeI x where
  PutStrLn :: String -> x  -> TeletypeF x  |   PutStrLn :: String -> TeletypeI ()
  GetLine :: (String -> x) -> TeletypeF x  |   GetLine :: TeletypeI String
  ExitSuccess ::              TeletypeF x  |   ExitSuccess :: TeletypeI ()

Using TeletypeF, we can build actual programs right away:

GetLine (\str -> PutStrLn (map toUpper str) ExitSuccess)

TeletypeI does not come with a way to refer to "the rest of the program" in the same way that TeletypeF does.

-- TeletypeF:
GetLine (\str -> "rest of program" goes here)
-- or
PutStrLn someString ("rest of program" goes here)
-- or
ExitSuccess -- there is no "rest of program" slot provided

Since TeletypeI lacks this "rest of the program" information, you can no longer gain any knowledge when you come across ExitSuccess.

-- TeletypeI
PutStrLn someString -- no information about "rest of program"
-- or
GetLine -- no information about "rest of program"
-- or
ExitSuccess -- no information about "rest of program"

What is permissible to come as the "rest of the program" is entirely up to the Program type, which doesn't know anything about the instruction set it is being applied to. It simply allows you to bind instructions together, and terminate via Return.