<p>Previously, I thought I found examples of explicitly defined monads without a transformer, but those examples were incorrect.</p>

<p>The transformer for <code>Either a (z -&gt; a)</code> is  <code>m (Either a (z -&gt; m a)</code>, where <code>m</code> is an arbitrary foreign monad. The transformer for <code>(a -&gt; n p) -&gt; n a</code> is <code>(a -&gt; t m p) -&gt; t m a</code> where <code>t m</code> is the transformer for the monad <code>n</code>.</p>

<ol>
<li>The free pointed monad.</li>
</ol>

<p>The monad type constructor <code>L</code> for this example is defined by</p>

<pre><code>  type L z a  = Either a (z -&gt; a)
</code></pre>

<p>The intent of this monad is to embellish the ordinary reader monad <code>z -&gt; a</code> with an explicit <code>pure</code> value (<code>Left x</code>). The ordinary reader monad's <code>pure</code> value is a constant function <code>pure x = _ -&gt; x</code>. However, if we are given a value of type <code>z -&gt; a</code>, we will not be able to determine whether this value is a constant function. With <code>L z a</code>, the <code>pure</code> value is represented explicitly as <code>Left x</code>. Users can now pattern-match on <code>L z a</code> and determine whether a given monadic value is pure or has an effect. Other than that, the monad <code>L z</code> does exactly the same thing as the reader monad.</p>

<p>The monad instance:</p>

<pre><code>  instance Monad (L z) where
     return x = Left x
     (Left x) &gt;&gt;= f = f x
     (Right q) &gt;&gt;= f = Right(join merged) where
        join :: (z -&gt; z -&gt; r) -&gt; z -&gt; r
        join f x = f x x -- the standard `join` for Reader monad
        merged :: z -&gt; z -&gt; r
        merged = merge . f . q -- `f . q` is the `fmap` of the Reader monad
        merge :: Either a (z -&gt; a) -&gt; z -&gt; a 
        merge (Left x) _ = x
        merge (Right p) z = p z
</code></pre>

<p>This monad <code>L z</code> is a specific case of a more general construction, <code>(Monad m) =&gt; Monad (L m)</code> where <code>L m a = Either a (m a)</code>. This construction embellishes a given monad <code>m</code> by adding an explicit <code>pure</code> value (<code>Left x</code>), so that users can now pattern-match on <code>L m</code> to decide whether the value is pure. In all other ways, <code>L m</code> represents the same computational effect as the monad <code>m</code>.</p>

<p>The monad instance for <code>L m</code> is almost the same as for the example above, except the <code>join</code> and <code>fmap</code> of the monad <code>m</code> need to be used, and the helper function <code>merge</code> is defined by</p>

<pre><code>    merge :: Either a (m a) -&gt; m a
    merge (Left x) = return @m x
    merge (Right p) = p
</code></pre>

<p>I checked that the laws of the monad hold for <code>L m</code> with an arbitrary monad <code>m</code>.</p>

<p>This construction gives the free pointed functor on the given monad <code>m</code>. This construction guarantees that the free pointed functor on a monad is also a monad.</p>

<p>The transformer for the free pointed monad is defined like this:</p>

<pre><code>  type LT m n a = n (Either a (mT n a))
</code></pre>

<p>where <code>mT</code> is the monad transformer of the monad m (which needs to be known).</p>

<ol start="2">
<li>Another example:</li>
</ol>

<p><code>type S a = (a -&gt; Bool) -&gt; Maybe a</code></p>

<p>This monad appeared in the context of "search monads" <a href="https://lukepalmer.wordpress.com/2010/11/17/searchable-data-types/" rel="nofollow noreferrer">here</a>. The <a href="https://arxiv.org/pdf/1406.2058.pdf" rel="nofollow noreferrer">paper by Jules Hedges</a> also mentions the search monad, and more generally, "selection" monads of the form</p>

<pre><code> type Sq n q a = (a -&gt; n q) -&gt; n a
</code></pre>

<p>for a given monad <code>n</code> and a fixed type <code>q</code>. The search monad above is a particular case of the selection monad with <code>n a = Maybe a</code> and <code>q = ()</code>. The paper by Hedges claims (without proof, but he proved it later using Coq) that <code>Sq</code> is a monad transformer for the monad <code>(a -&gt; q) -&gt; a</code>.</p>

<p>However, the monad <code>(a -&gt; q) -&gt; a</code> has another monad transformer <code>(m a -&gt; q) -&gt; m a</code> of the "composed outside" type. This is related to the property of "rigidity" explored in the question <a href="https://stackoverflow.com/questions/39649497/is-this-property-of-a-functor-stronger-than-a-monad?rq=1">Is this property of a functor stronger than a monad?</a> Namely, <code>(a -&gt; q) -&gt; a</code> is a rigid monad, and all rigid monads have monad transformers of the "composed-outside" type.</p>

<ol start="3">
<li>Generally, transformed monads don't themselves automatically possess a monad transformer. That is, once we take some foreign monad <code>m</code> and apply some monad transformer <code>t</code> to it, we obtain a new monad <code>t m</code>, and this monad doesn't have a transformer: given a new foreign monad <code>n</code>, we don't know how to transform <code>n</code> with the monad <code>t m</code>. If we know the transformer <code>mT</code> for the monad <code>m</code>, we can first transform <code>n</code> with <code>mT</code> and then transform the result with <code>t</code>. But if we don't have a transformer for the monad <code>m</code>, we are stuck: there is no construction that creates a transformer for the monad <code>t m</code> out of the knowledge of <code>t</code> alone and works for arbitrary foreign monads <code>m</code>.</li>
</ol>

<p>However, in practice all explicitly defined monads have explicitly defined transformers, so this problem does not arise.</p>

<ol start="4">
<li>@JamesCandy's answer suggests that <strong>for any monad</strong> (including <code>IO</code>?!), one can write a (general but complicated) type expression that represents the corresponding monad transformer. Namely, you first need to Church-encode your monad type, which makes the type look like a continuation monad, and then define its monad transformer as if for the continuation monad. But I think this is incorrect - it does not give a recipe for producing a monad transformer in general.</li>
</ol>

<p>Taking the Church encoding of a type <code>a</code> means writing down the type</p>

<pre><code> type ca = forall r. (a -&gt; r) -&gt; r
</code></pre>

<p>This type <code>ca</code> is completely isomorphic to <code>a</code> by Yoneda's lemma. So far we have achieved nothing other than made the type a lot more complicated by introducing a quantified type parameter <code>forall r</code>.</p>

<p>Now let's Church-encode a base monad <code>L</code>:</p>

<pre><code> type CL a = forall r. (L a -&gt; r) -&gt; r
</code></pre>

<p>Again, we have achieved nothing so far, since <code>CL a</code> is fully equivalent to <code>L a</code>.</p>

<p>Now pretend for a second that <code>CL a</code> a continuation monad (which it isn't!), and write the monad transformer as if it were a continuation monad transformer, by replacing the result type <code>r</code> through <code>m r</code>:</p>

<pre><code> type TCL m a = forall r. (L a -&gt; m r) -&gt; m r
</code></pre>

<p>This is claimed to be the "Church-encoded monad transformer" for <code>L</code>. But this seems to be incorrect. We need to check the properties:</p>

<ul>
<li><code>TCL m</code> is a lawful monad for any foreign monad <code>m</code> and for any base monad <code>L</code></li>
<li><code>m a -&gt; TCL m a</code> is a lawful monadic morphism</li>
</ul>

<p>The second property holds, but I believe the first property fails, - in other words, <code>TCL m</code> is not a monad for an arbitrary monad <code>m</code>. Perhaps some monads <code>m</code> admit this but others do not. I was not able to find a general monad instance for <code>TCL m</code> corresponding to an arbitrary base monad <code>L</code>.</p>

<p>Another way to argue that <code>TCL m</code> is not in general a monad is to note that <code>forall r. (a -&gt; m r) -&gt; m r</code> is indeed a monad for any type constructor <code>m</code>. Denote this monad by <code>CM</code>. Now, <code>TCL m a = CM (L a)</code>. If <code>TCL m</code> were a monad, it would imply that <code>CM</code> can be composed with any monad <code>L</code> and yields a lawful monad <code>CM (L a)</code>. However, it is highly unlikely that a nontrivial monad <code>CM</code> (in particular, one that is not equivalent to <code>Reader</code>) will compose with all monads <code>L</code>. Monads usually do not compose without stringent further constraints.</p>

<p>A specific example where this does not work is for reader monads. Consider <code>L a = r -&gt; a</code> and <code>m a = s -&gt; a</code> where <code>r</code> and <code>s</code> are some fixed types. Now, we would like to consider the "Church-encoded monad transformer" <code>forall t. (L a -&gt; m t) -&gt; m t</code>. We can simplify this type expression using the Yoneda lemma,</p>

<pre><code> forall t. (x -&gt; t) -&gt; Q t  = Q x
</code></pre>

<p>(for any functor <code>Q</code>) and obtain</p>

<pre><code> forall t. (L a -&gt; s -&gt; t) -&gt; s -&gt; t
 = forall t. ((L a, s) -&gt; t) -&gt; s -&gt; t
 = s -&gt; (L a, s)
 = s -&gt; (r -&gt; a, s)
</code></pre>

<p>So this is the type expression for <code>TCL m a</code> in this case. If <code>TCL</code> were a monad transformer then <code>P a = s -&gt; (r -&gt; a, s)</code> would be a monad. But one can check explicitly that this <code>P</code> is actually not a monad (one cannot implement <code>return</code> and <code>bind</code> that satisfy the laws).</p>

<p>Even if this worked (i.e. <strong>assuming that I made a mistake in claiming that <code>TCL m</code> is in general not a monad</strong>), this construction has certain disadvantages:</p>

<ul>
<li>It is not functorial (i.e. not covariant) with respect to the foreign monad <code>m</code>, so we cannot do things like interpret a transformed free monad into another monad, or merge two monad transformers as explained here <a href="https://stackoverflow.com/questions/18364808/is-there-a-principled-way-to-compose-two-monad-transformers-if-they-are-of-diffe">Is there a principled way to compose two monad transformers if they are of different type, but their underlying monad is of the same type?</a></li>
<li>The presence of a <code>forall r</code> makes the type quite complicated to reason about and may lead to performance degradation (see the "Church encoding considered harmful" paper) and stack overflows (since Church encoding is usually not stack-safe)</li>
<li>The Church-encoded monad transformer for an identity base monad (<code>L = Id</code>) does not yield the unmodified foreign monad: <code>T m a = forall r. (a -&gt; m r) -&gt; m r</code> and this is not the same as <code>m a</code>. In fact it's quite difficult to figure out what that monad is, given a monad <code>m</code>.</li>
</ul>

<p>As an example showing why <code>forall r</code> makes reasoning complicated, consider the foreign monad <code>m a = Maybe a</code> and try to understand what the type <code>forall r. (a -&gt; Maybe r) -&gt; Maybe r</code> actually means. I was not able to simplify this type or to find a good explanation about what this type does, i.e. what kind of "effect" it represents (since it's a monad, it must represent some kind of "effect") and how one would use such a type.</p>

<ul>
<li>The Church-encoded monad transformer is not equivalent to the standard well-known monad transformers such as <code>ReaderT</code>, <code>WriterT</code>, <code>EitherT</code>, <code>StateT</code> and so on.</li>
</ul>

<p>It is not clear how many other monad transformers exist and in what cases one would use one or another transformer.</p>

<ol start="5">
<li>One of the questions in the post is to find an explicit example of a monad <code>m</code> that has two transformers <code>t1</code> and <code>t2</code> such that for some foreign monad <code>n</code>, the monads <code>t1 n</code> and <code>t2 n</code> are not equivalent.</li>
</ol>

<p>I believe that the <code>Search</code> monad provides such an example.</p>

<pre><code> type Search a = (a -&gt; p) -&gt; a
</code></pre>

<p>where <code>p</code> is a fixed type.</p>

<p>The transformers are</p>

<pre><code> type SearchT1 n a = (a -&gt; n p) -&gt; n a
 type SearchT2 n a = (n a -&gt; p) -&gt; n a
</code></pre>

<p>I checked that both <code>SearchT1 n</code> and <code>SearchT2 n</code> are lawful monads for any monad <code>n</code>. We have liftings <code>n a -&gt; SearchT1 n a</code> and <code>n a -&gt; SearchT2 n a</code> that work by returning constant functions (just return <code>n a</code> as given, ignoring the argument). We have <code>SearchT1 Identity</code> and <code>SearchT2 Identity</code> obviously equivalent to <code>Search</code>.</p>

<p>The big difference between <code>SearchT1</code> and <code>SearchT2</code> is that <code>SearchT1</code> is not functorial in <code>n</code>, while <code>SearchT2</code> is. This may have implications for "running" ("interpreting") the transformed monad, since normally we would like to be able to lift an interpreter <code>n a -&gt; n' a</code> into a "runner" <code>SearchT n a -&gt; SearchT n' a</code>. This is possibly only with <code>SearchT2</code>.</p>

<p>A similar deficiency is present in the standard monad transformers for the continuation monad and the codensity monad: they are not functorial in the foreign monad.</p>
Is there a monad that doesn't have a corresponding monad transformer (except IO)?
<p>So far, every monad (that can be represented as a data type) that I have encountered had a corresponding monad transformer, or could have one. Is there such a monad that can't have one? Or <strong>do all monads have a corresponding transformer?</strong></p>

<p>By a <em>transformer <code>t</code> corresponding to monad <code>m</code></em> I mean that <code>t Identity</code> is isomorphic to <code>m</code>. And of course that it satisfies the monad transformer laws and that <code>t n</code> is a monad for any monad <code>n</code>.</p>

<p>I'd like to see either a proof (ideally a constructive one) that every monad has one, or an example of a particular monad that doesn't have one (with a proof). I'm interested in both more Haskell-oriented answers, as well as (category) theoretical ones.</p>

<p>As a follow-up question, is there a monad <code>m</code> that has two distinct transformers <code>t1</code> and <code>t2</code>? That is, <code>t1 Identity</code> is isomorphic to <code>t2 Identity</code> and to <code>m</code>, but there is a monad <code>n</code> such that <code>t1 n</code> is not isomorphic to <code>t2 n</code>.</p>

<p>(<code>IO</code> and <code>ST</code> have a special semantics so I don't take them into account here and let's disregard them completely. Let's focus only on "pure" monads that can be constructed using data types.)</p>