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).
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 _ &lt;- putStr "foo"
   return 42


and

do _ &lt;- 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)
    (&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)


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.