# Moggi's computational metalanguage

In Notions of Computation and Monads 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).

• 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 Mar 28 '18 at 20:18
• @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 Mar 28 '18 at 20:47
• 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 Mar 28 '18 at 21:12
• 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 Mar 28 '18 at 22:22

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

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:

1. The Maybe monad: a computation may have a value (Just v), or have no value at all (Nothing).

2. 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?

3. The probability monad: a computation results in a probability distribution of values. Again, in what sense does such a computation "have a value"?

4. 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)

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.