I'm sure we've all used the Writer monad from time to time when we want to yield a value which will propagate up several levels of a recursive call tree "behind the scenes". And we've all been annoyed at having to rewrite the whole function in monadic style. WriterT is less intrusive, but not much so, since we have to pepper the code with calls to "lift". I think there's a better solution. It should be possible to turn the idea of linear implicit parameters upside-down, to get values which are automatically propagated upwards and merged as necessary. We would need a class "Mergeable", a counterpart to "Splittable". But we already have such a class (Monoid). Here's a possible syntax. An expression like (123, ^x = "foo") would have the type (Integer, ^x :: String), which is like a tuple but with all but one of the elements having a name. An expression like (123, ^x="foo") - (45, ^x="bar", ^y="baz") would be converted by the compiler to (123 - 45, ^x=("foo" `mappend` "bar"), ^y="baz"), even if the two values passed to (-) were returned from a recursive call and not written out explicitly as I've done here. These return values could then be extracted by matching against the pattern (a, ^x = b), which would return the value of ^x in b, and the scrutinee with ^x removed in a. The semantics seems very simple -- virtually identical to implicit parameters. Implicit return values are dual to exceptions-as-values in some sense: they use an implicit product return type instead of a sum. It should be possible to implicitly return values which are not instances of Monoid: the compiler errors out if it ever needs to merge such a type. Wouldn't this provide a form of uniqueness typing a la Clean? In fact, couldn't we implement safe state threads on top of this, instead of the ST monad? In fact, couldn't we work within several state threads at once? -- Ben