27

Supposedly, all monads can be expressed using Free (if this isn't true, what is a counter-example and why)? How can the continuation monad or its corresponding transformer be expressed using Free or FreeT - what would be the corresponding functor? Or if they can't, what's the reason why?

Update: By expressed I mean basically isomorphic to Free F where F is a functor we're looking for, like for example Writer w is isomorphic to Free ((,) w).

Petr
  • 62,528
  • 13
  • 153
  • 317
  • 1
    maybe you should move this to the computer science section (https://scicomp.stackexchange.com/) - most likely you will get an answer there – Random Dev Sep 16 '14 at 20:04
  • 2
    But `Writer w` isn't isomorphic to `Free ((,) w)`, merely a quotient of it. After all, `Writer w` *is* `((,) w)`. Furthermore, `Cont r` is isomorphic to a quotient of `Free (Cont r)` as I demonstrated below. Can you clarify further? – Tom Ellis Sep 17 '14 at 18:45
  • @TomEllis Good point, I'll need to think about it. – Petr Sep 17 '14 at 19:04

4 Answers4

16

The continuation monad is the counterexample you are looking for. I'm not knowledgeable enough to provide a full proof but I'll give you a couple of references to look up.

The idea is that monads have a concept of "rank" associated with them. "Rank" roughly means the number of operations needed to provide the full functionality of the monad.

I suspect that, with the exception of continuation-derived monads, all the monads we deal with in Haskell have rank, e.g. Identity, Maybe, State s, Either e, ..., and their combinations through their transformers. For example, Identity is generated by no operations, Maybe is generated by Nothing, State s by get and put s and Either e by Left e. (Perhaps this shows they all in fact have finite rank, or perhaps put s counts as a different operation for each s, so State s has the rank of the size of s, I'm not sure.)

Free monads certainly have rank because Free f is explicitly generated by the operations encoded by f.

Here is a technical definition of rank, but it's not very enlightening: http://journals.cambridge.org/action/displayAbstract?aid=4759448

Here you can see the claim that the continuation monad does not have rank: http://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf. I'm not sure how they prove that, but the implication is that the continuation monad is not generated by any collection of operations and thus cannot be expressed as (a quotient of) a free monad.

Hopefully someone can come along and tidy up my technicalities, but this is the structure of the proof you want.

Tom Ellis
  • 9,224
  • 1
  • 29
  • 54
  • 1
    The second paper certainly asserts that the continuations monad does not have rank, and that you cannot make the monad-sum of the continuations monad with many others, but I can't find an argument that it is therefore not the image/quotient of a free monad. To call the first paper "not very enlightening" regarding rank seems an understatement to me! Can you help out a little? – AndrewC Sep 14 '14 at 13:54
  • 1
    Hello Andrew. The needed component should be that a quotient of a monad has no greater rank than the original. I don't know how to demonstrate this though. On the specifics of rank I'm afraid I can't really provide any more information. References are very hard to come by and I only have an intuitive understanding as "the number of operations required to generate". I don't actually know if this is correct, though I think it is close to correct. – Tom Ellis Sep 14 '14 at 15:29
  • I would be wary of transporting this kind of cardinality argument from Set to Hask. After all Hask admits such things like the type `newtype X = X (X -> Bool)` which satisfies the isomorphism `X ~ (X -> Bool)`, which is not possible for any set for cardinality reasons. – Reid Barton Sep 18 '14 at 18:18
  • Well, I'm wary of my whole argument, but I'm pretty sure it can be made honest. Additionally, I don't think the kind of behaviour you demonstrate with `X` can happen with functorial datatypes can it? I think you need non-positivity for that kind of thing. – Tom Ellis Sep 18 '14 at 19:47
  • The same situation exists with `newtype X = X ((X -> Bool) -> Bool)` which is the fixed point of a functor. For the fixed point to exist in Set the functor needs to be strictly positive (or more generally, accessible). – Reid Barton Sep 21 '14 at 17:56
  • Interesting example. Anyway, as you will see from the linked paper, rank is a concept defined for any functor regardless of the categories it is defined on. But still, there are plenty of holes in the argument that need to be filled in. – Tom Ellis Sep 21 '14 at 19:41
  • I looked up the notion of having rank in that paper and it is the same as accessibility; older terminology I guess. Just because the continuation monad *on Set* does not have rank does not mean the continuation monad *on Hask* does not have rank. For instance `Cont Bool` on Hask has a fixed point, my type `X` above, but `Cont Bool` on Set does not; and every functor with rank has an initial fixed point, so this is hardly unrelated. – Reid Barton Sep 23 '14 at 20:35
  • It's hard to pick apart this argument without a mathematical definition of "Hask", but you make the following claims: Cont r does not have rank (for r nontrivial); Free f has rank; a quotient of a monad with rank has rank. But Cont r is a quotient of Free (Cont r), so one of these claims must be wrong. – Reid Barton Sep 23 '14 at 20:37
  • Reid: You are correct that there is an error. That's why I made my follow up post: http://stackoverflow.com/a/25888318/997606 The error is that `Free f` need not have rank. Presumably it has rank if and only if `f` has rank, though I caution readers again about my lack of familiarity with this subject! – Tom Ellis Sep 24 '14 at 16:52
  • I see what you mean now about transporting the argument from Set to Hask. I thought you meant the concept of rank did not carry over to Hask. Instead you mean that `Cont` in Hask may have rank even if it doesn't in Set. Well, I would be *very* suprised if a paper by Hyland, Levy, Plotkin and Power would claim the non-existence of rank for continuations if they *did* have rank in System F (say). They don't specifically reference a proof though so I can't check. By the way, which reference for the definition of rank did you find? Would you mind sharing? – Tom Ellis Sep 24 '14 at 17:04
  • I looked up the definition of rank in the Kelly paper you referenced. The HLPP paper is clearly talking about the continuation monad on Set, see the last sentence of section 1 and references to Set throughout the paper. – Reid Barton Sep 24 '14 at 17:25
  • The terminology is "For *simplicity of exposition*, we generally restrict attention to monads on Set" (my emphasis). That language suggests to me the result holds more generally. But it's worth a MathOverflow question, which I'll write up when I get around to it. – Tom Ellis Sep 24 '14 at 18:05
  • I'm not sure what "System F" is supposed to mean as a category, but it sounds like a small category (having only a set of objects and morphisms). I'm pretty sure that any functor between small categories has rank. Having rank is fundamentally about the difference between small and large things. Anyways, this doesn't really seem to be going anywhere without a more precise formulation of what the question actually is... – Reid Barton Sep 24 '14 at 19:09
  • Probably, in a "syntactic" context like System F, the moral equivalent of having rank is strict positivity. – Reid Barton Sep 24 '14 at 19:12
  • I was thinking of something like the models of System F described in "Polymorphism is Set Theoretic, Constructively" (Pitts). They are, as you say, small categories. However, I don't see that functors between small categories should have rank. Why should they preseve co-products, let alone larger colimits? Anyway, I am now very much out of my depth, so I shall bow out. – Tom Ellis Sep 24 '14 at 19:50
3

Here's a silly answer that shows that both your question and my earlier answer need work.

Cont can easily be expressed using Free:

import Control.Monad.Free
import Control.Monad.Trans.Cont

type Cont' r = Free (Cont r)

quotient :: Cont' r a -> Cont r a
quotient = retract

Cont is a (quotient of) the free monad on itself (of course). So now you have to clarify precisely what it is you mean by "express".

Tom Ellis
  • 9,224
  • 1
  • 29
  • 54
  • By _expressed_ I meant basically isomorphic to `Free f`, like `Maybe` is isomorphic to `Free MaybeF` where `data MaybeF a = MaybeF` etc. I'll update the question. – Petr Sep 17 '14 at 13:48
  • `Maybe` isn't isomorphic to `Free MaybeF`, but merely a quotient of it. – Tom Ellis Sep 17 '14 at 18:47
  • 1
    `Maybe` is isomorphic to `Free MaybeF` if `data MaybeF a = Nada`. – Reid Barton Sep 18 '14 at 20:45
  • @ReidBarton: Ah yes, you and Petr are correct about `Maybe`. What I was trying to indicate is that a monad is not generally `Free f`, where `f` is some functor of generating operations, but merely a quotient of it. You made the same point in this answer with the example of `State`: http://stackoverflow.com/a/24918234/190376 – Tom Ellis Sep 19 '14 at 08:57
2

See my answer to a question of yours from last year. Let's consider r = Bool (or more generally any type r which admits a nontrivial automorphism).

Define m (up to newtype wrappers) as m :: (() -> Bool) -> Bool; m f = not (f ()). Then m is nontrivial but m >> m is trivial. So Cont Bool is not isomorphic to a free monad.

The full computation in Haskell:

rwbarton@morphism:/tmp$ ghci
GHCi, version 7.8.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> import Control.Monad.Cont
Prelude Control.Monad.Cont> let m :: Cont Bool (); m = ContT (\f -> fmap not (f ()))
Loading package transformers-0.3.0.0 ... linking ... done.
Prelude Control.Monad.Cont> runCont m (const False) -- m not trivial
True
Prelude Control.Monad.Cont> runCont (m >> m) (const False)
False
Prelude Control.Monad.Cont> runCont (m >> m) (const True) -- (m >> m) trivial
True
Community
  • 1
  • 1
Reid Barton
  • 14,951
  • 3
  • 39
  • 49
  • Indeed this is a rigorous answer to my question. I probably will need to think it over, if my question even makes sense, or get deeper understanding of the problem. As you said, most monads can't have a `Free` representation that'd be isomorphic to them. On the other hand as @TomEllis pointed out, each monad is an image of `Free m` using `retract`. So I'm looking for how a monad `M` can represented using `Free F` such that `M` is a homomorphic image of `Free F` and where the functor `F` is in some sense minimal. – Petr Sep 19 '14 at 14:15
1

Here's a couple tiny proofs that there doesn't exist a Functor f such that for all a :: * and m :: * -> * FreeT f m a is equivalent to ContT r m a using the normal interpretation of FreeT.

Let m :: * -> * such that there is no instance Functor m. Due to instance Functor (ContT r m) there is an instance Functor (ConT r m). If ContT r and FreeT f are equivalent, we would expect Functor (FreeT f m). However, using the normal interpretation of FreeT, instance (Functor f, Functor m) => Functor (FreeT f m), there is no Functor (FreeT f m) instance because there is no Functor m instance. (I relaxed the normal interpreation of FreeT from requiring Monad m to only requiring Functor m since it only makes use of liftM.)

Let m :: * -> * such that there is no instance Monad m. Due to instance Monad (ContT r m) there is an instance Monad (ConT r m). If ContT r and FreeT f are equivalent, we would expect Monad (FreeT f m). However, using the normal interpretation of FreeT, instance (Functor f, Monad m) => Monad (FreeT f m), there is no Monad (FreeT f m) instance because there is no Monad m instance.

If we don't want to use the normal interpretation of Free or FreeT we can cobble together monsters that work just like Cont r or ContT r. For example, there is a Functor (f r) such that Free (f r) a can be equivalent to Cont r a using an abnormal interpretation of Free, namely Cont r itself.

Cirdec
  • 24,019
  • 2
  • 50
  • 100