<p>I still don't quite understand what having a value means, but just considering the question of "can we give up the eta rule for monads", the answer is yes, this is an entirely reasonable thing to consider.</p>

<p>As a rule of thumb, having the eta rule in the syntax corresponds to the uniqueness condition on a universal property. So if you want to add natural numbers, but don't want to enforce the eta property for the eliminator, then this corresponds to looking for a weakly initial object in the category of natural number algebras.</p>

<p>I don't know who has studied the theory of weak monads in general (though surely someone must have), but Andy Gordon defined the notion in chapter 8 of his 1992 PhD thesis <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/fpio.pdf" rel="nofollow noreferrer"><em>Functional Programming and Input/Output</em></a> and used it as a model of teletype IO. </p>

<p>One terminological issue: the notion of weakness here is not the opposite of the strong in "strong monad". Moggi models computations using monads with a strength, which is a natural transformation $A \times T(B) \to T(A \times B)$. Dropping the strength gives you an ordinary monad (ie, a model of S4 possibility), but this is not a "weak monad" in the sense of the question (the eta-rule is still validated). </p>

CC BY-SA 3.0
2018-04-03T10:48:20.290Z
2018-04-03T10:48:20.290Z
Neel Krishnaswami
<p>It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For instance, the computations</p>

<pre><code>do _ &lt;- putStr "foo"
   return 42
</code></pre>

<p>and</p>

<pre><code>do _ &lt;- putStr "bar"
   return 42
</code></pre>

<p>both "have" value <code>42</code> but are different, since one prints out <code>foo</code> and the other <code>bar</code>.</p>

<p>The problem really arises elsewhere, namely in the idea that <em>"a computation has a value"</em>. Consider the following monads:</p>

<ol>
<li><p>The <code>Maybe</code> monad: a computation may have a value (<code>Just v</code>), or have no value at all (<code>Nothing</code>).</p></li>
<li><p>The non-determinism monad: a computation results in a set of (possible) values. What does it mean that it "has" a value? Has all of them? One of them?</p></li>
<li><p>The probability monad: a computation results in a probability distribution of values. Again, in what sense does such a computation "have a value"?</p></li>
<li><p>The continuation monad: a computation results in a continuation. What does it mean for a continuation to "have a value"?</p></li>
</ol>

<p>It is best to just forget the idea that in general a computation gives back a value, two values, possible values, or anything like that.</p>

<p>There may be <em>particular</em> monads for which it <em>does</em> make sense to speak about "computations having values", but not for all monads.</p>

<p>The OP also suggests that intensional features of computations (one computation takes a different number of steps than another) should be expressible with monads. This is true, but whatever intensional features you want to capture with the monad (memory usage, time), you have to expose them explicitly in the monad. For instance, we could do this:</p>

<pre><code>data Timed a = Timing (a, Integer)

instance Monad Timed where
    return x = Timing (x, 0)
    (&gt;&gt;=) (Timing (x, n)) f = (let Timing (y, m) = f x in Timing (y, n + m + 1))

x :: Timed Integer
x = do u &lt;- return 14
       v &lt;- return 3
       return (u * v)

y :: Timed Integer
y = do u &lt;- return 14
       v' &lt;- return 1
       v'' &lt;- return 2
       v &lt;- return (v' + v'')
       return (u * v)
</code></pre>

<p>Here <code>x</code> and <code>y</code> both "have" value <code>42</code>, but the timing is different since <code>y</code> takes four steps to compute and <code>x</code> takes just two.</p>

CC BY-SA 3.0
2018-03-31T18:33:52.200Z
2018-03-31T18:46:52.730Z
2018-03-31T18:46:52.730Z
Andrej Bauer
<p>In <a href="https://core.ac.uk/download/pdf/21173011.pdf" rel="nofollow noreferrer">Notions of Computation and Monads</a> Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule:</p>

<p>$$\frac{x: A \vdash a:TB}{x:A \vdash let \,  y \Leftarrow a \, in\, [y] = a}$$</p>

<p>This rule prevents distinct computations having the same value. Is there a weakened notion of a monad that does not yield the $T\eta$ rule? Has this question already been studied? I'm particularly interested in the logic you get when you drop $T\eta$ from Moggi's rules for the simple metalanguage, but keep the other rules in place (table 4 in the pdf).</p>

CC BY-SA 3.0
2018-03-28T20:18:13.277Z
What do you mean by "prevents distinct computations having the same value"? I don't see how this rule, which gives a way to prove two terms *are* equal, could possibly imply that two terms are distinct.
Max New
CC BY-SA 3.0
2018-03-28T20:47:59.547Z
@MaxNew "I don't see how this rule, which gives a way to prove two terms are equal, could possibly imply that two terms are distinct". Not sure why that's relevant: the claim was not a distinctness claim but an injectivity claim -- that distinct programs can't evaluate to the same thing. One way to say that is to say that $[\cdot]$ is a left inverse of evaluation, which of course can be stated equationally (and, indeed, that's what the equation in the question intuitively says).
Andrew Bacon
CC BY-SA 3.0
2018-03-28T21:12:07.090Z
Ok I think I see what you mean, but you may be misunderstanding something. If you have a non-deterministic language, two distinct computations can evaluate to the same value *sometimes*. I.e. the computation that always returns $0$ vs the one that non-deterministically chooses between $0$ and $1$. So in that sense it's not sensible to say that $[\cdot]$ is a post-inverse to evaluation because evaluation is not necessarily a function.
Max New
CC BY-SA 3.0
2018-03-28T22:22:37.587Z
Sure, my gloss on the equation isn't going to apply for every interpretation of $T$. But the application I had in mind was specific: the modelling of (deterministic) computations that differ (e.g., in efficiency) but output the same values. The $T\eta$ rule seems to rule that out.
Andrew Bacon
<ct.category-theory><typed-lambda-calculus><operational-semantics><monad>
Moggi's computational metalanguage
Andrew Bacon
# Moggi's computational metalanguage

(Asked by: username_0 on 2018-03-28)

In [Notions of Computation and Monads](https://core.ac.uk/download/pdf/21173011.pdf) Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule:

$$\frac{x: A \vdash a:TB}{x:A \vdash let \, y \Leftarrow a \, in\, [y] = a}$$

This rule prevents distinct computations having the same value. Is there a weakened notion of a monad that does not yield the $T\eta$ rule? Has this question already been studied? I'm particularly interested in the logic you get when you drop $T\eta$ from Moggi's rules for the simple metalanguage, but keep the other rules in place (table 4 in the pdf).

**Tags:** ct.category-theory, typed-lambda-calculus, operational-semantics, monad
> **Comments:**
> **username_1**: What do you mean by "prevents distinct computations having the same value"? I don't see how this rule, which gives a way to prove two terms *are* equal, could possibly imply that two terms are distinct.  
> **username_0**: @MaxNew "I don't see how this rule, which gives a way to prove two terms are equal, could possibly imply that two terms are distinct". Not sure why that's relevant: the claim was not a distinctness claim but an injectivity claim -- that distinct programs can't evaluate to the same thing. One way to say that is to say that $[\cdot]$ is a left inverse of evaluation, which of course can be stated equationally (and, indeed, that's what the equation in the question intuitively says).  
> **username_1**: Ok I think I see what you mean, but you may be misunderstanding something. If you have a non-deterministic language, two distinct computations can evaluate to the same value *sometimes*. I.e. the computation that always returns $0$ vs the one that non-deterministically chooses between $0$ and $1$. So in that sense it's not sensible to say that $[\cdot]$ is a post-inverse to evaluation because evaluation is not necessarily a function.  
> **username_0**: Sure, my gloss on the equation isn't going to apply for every interpretation of $T$. But the application I had in mind was specific: the modelling of (deterministic) computations that differ (e.g., in efficiency) but output the same values. The $T\eta$ rule seems to rule that out.  

---

## 2 answers

### Answer by username_2 on 2018-04-03. Score: 2 | Accepted answer

I still don't quite understand what having a value means, but just considering the question of "can we give up the eta rule for monads", the answer is yes, this is an entirely reasonable thing to consider.

As a rule of thumb, having the eta rule in the syntax corresponds to the uniqueness condition on a universal property. So if you want to add natural numbers, but don't want to enforce the eta property for the eliminator, then this corresponds to looking for a weakly initial object in the category of natural number algebras.

I don't know who has studied the theory of weak monads in general (though surely someone must have), but Andy Gordon defined the notion in chapter 8 of his 1992 PhD thesis [*Functional Programming and Input/Output*](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/fpio.pdf) and used it as a model of teletype IO.

One terminological issue: the notion of weakness here is not the opposite of the strong in "strong monad". Moggi models computations using monads with a strength, which is a natural transformation $A \times T(B) \to T(A \times B)$. Dropping the strength gives you an ordinary monad (ie, a model of S4 possibility), but this is not a "weak monad" in the sense of the question (the eta-rule is still validated).


---

### Answer by username_3 on 2018-03-31. Score: 5

It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For instance, the computations
do _ <- putStr "foo"
   return 42

and
do _ <- putStr "bar"
   return 42

both "have" value 42 but are different, since one prints out foo and the other bar.
The problem really arises elsewhere, namely in the idea that "a computation has a value". Consider the following monads:

The Maybe monad: a computation may have a value (Just v), or have no value at all (Nothing).
The non-determinism monad: a computation results in a set of (possible) values. What does it mean that it "has" a value? Has all of them? One of them?
The probability monad: a computation results in a probability distribution of values. Again, in what sense does such a computation "have a value"?
The continuation monad: a computation results in a continuation. What does it mean for a continuation to "have a value"?

It is best to just forget the idea that in general a computation gives back a value, two values, possible values, or anything like that.
There may be particular monads for which it does make sense to speak about "computations having values", but not for all monads.
The OP also suggests that intensional features of computations (one computation takes a different number of steps than another) should be expressible with monads. This is true, but whatever intensional features you want to capture with the monad (memory usage, time), you have to expose them explicitly in the monad. For instance, we could do this:
data Timed a = Timing (a, Integer)

instance Monad Timed where
    return x = Timing (x, 0)
    (>>=) (Timing (x, n)) f = (let Timing (y, m) = f x in Timing (y, n + m + 1))

x :: Timed Integer
x = do u <- return 14
       v <- return 3
       return (u * v)

y :: Timed Integer
y = do u <- return 14
       v' <- return 1
       v'' <- return 2
       v <- return (v' + v'')
       return (u * v)

Here x and y both "have" value 42, but the timing is different since y takes four steps to compute and x takes just two.


---

