up vote 23 down vote favorite
16

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?

share|improve this question
1  
That example was for operational. – Dag Jan 10 '13 at 17:34
7  
Note operational is effectively Free (Coyoneda f), Coyoneda f is isomorphic to f, so Free (Coyoneda f) is isomorphic to Free f. – Edward KMETT Jan 12 '13 at 21:26
1  
@EdwardKmett: I'm confused. I find that Coyoneda Const a ~= Identity a, which is not isomorphic to Const a. – Heinrich Apfelmus Jan 13 '13 at 9:41
2  
Coyoneda (Const m) a is isomorphic to Const m a which is isomorphic to m. – Edward KMETT Jan 17 '13 at 17:35
2  
If by Const you mean the trivial data Foo a = Foo functor then Coyoneda Foo a = exists b. (b -> a, Foo) which doesn't give you an extra element, since you don't have a b to call the function with. – Edward KMETT Jan 17 '13 at 17:48
up vote 16 down vote accepted

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

share|improve this answer
2  
You can also point out that the law for Free is independent of the observation function. It's actually just exitSuccess >>= f = exitSuccess. – Gabriel Gonzalez Jan 12 '13 at 17:21
1  
Indeed, but I wanted to emphasize the point that laws don't need to hold until you apply interpret. A law is true iff there is no observation that can falsify it. – Heinrich Apfelmus Jan 13 '13 at 19:47
1  
Right. I just meant that you could use that to drive home that Free bakes certain laws into the type instead of the interpreter. – Gabriel Gonzalez Jan 14 '13 at 1:13
    
"However, this doesn't work for other laws that can be baked into free monads, for instance the distributive law for the mplus instruction." Can you expand on that? – Gavin Wahl Aug 17 '15 at 16:33
    
@GavinWahl I meant that the distributive law cannot be baked into a monad built from operational via the type system, in contrast to the nice trick that is possible with ExitSuccess. – Heinrich Apfelmus Aug 18 '15 at 13:12
up vote 11 down vote

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.

share|improve this answer
1  
"As always we'll have to ignore undefined here" - you don't have to ignore undefined with the TeletypeF formulation in order to make the guarantee. This is why "the answer is no" and "the answer is yes" are both correct. :) – Dan Burton Jan 11 '13 at 16:23
1  
I'm sure undefined can mess up the proof for TeletypeF as well, you just have to be a bit more devious. – Sjoerd Visscher Jan 11 '13 at 21:02
    
Yes, both your answers would seem to be correct, and SO only lets me choose one accepted answer right? Although you both missed my question about laziness, but I guess I shouldn't ask two questions in one post. :-) Thank you both for your answers anyway. – Dag Jan 12 '13 at 14:38
1  
@SjoerdVisscher As Heinrich and Gabriel pointed out, using the FreeT monad instance guarantees that exitSuccess >>= k === exitSuccess. I don't see how undefined can possibly mess that up. – Dan Burton Jan 12 '13 at 19:25
3  
@DanBurton Define run (Free ExitSuccess) = loop where loop = loop for example. – Sjoerd Visscher Jan 13 '13 at 13:57
up vote 5 down vote

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.

share|improve this answer
    
Does your answer also imply that we don't lose laziness with the free monad version? I guess I should try writing a free state monad to see for myself, though I'd have to figure out a translation for the state function... – Dag Jan 10 '13 at 21:05
    
@Dag it practically writes itself: hpaste.org/80607 . Are you implying that the operational approach loses laziness? I don't see how that is the case. (The state function is easily written in terms of get and put). – Dan Burton Jan 11 '13 at 16:55
1  
Consider the example at the bottom of my post, from the operational monad tutorial. It evaluates to an infinite list that you can for example take 10 from, no problem with mtl/transformers. With operational and free, it hangs. So unless I'm doing something wrong, I've answered my own question: yes, the free monad suffers the same laziness issue as operational. – Dag Jan 11 '13 at 17:43

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.