Moggi's computational metalanguage

Question

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

Answer 1

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

Answer 2

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)

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.