A proof that Promises/A is a Monad

promise-monad-proof.js

//-------------------------------------------------------------
//
// Hypothesis:
//
// Promises/A is a Monad
//
// To be a Monad, it must provide at least:
// - A unit (aka return or mreturn) operation that creates a corresponding
//   monadic value from a non-monadic value.
// - A bind operation that applies a function to a monadic value
//
// And it must satisfy the 3 Monadic Laws:
// 1. unit a >>= f == f
// 2. m >>= unit == m
// 3.(m >>= f) >>= g == m >>= (\x -> f x >>= g)
//
// See:
// http://en.wikipedia.org/wiki/Monad_(functional_programming)
// http://www.haskell.org/haskellwiki/Monad_Laws
// http://mvanier.livejournal.com/3917.html
// http://mvanier.livejournal.com/4305.html
//
// Author: Brian Cavalier ([email protected])
//
//-------------------------------------------------------------

var when, PromiseMonad, a, b, leftResult, rightResult;

// Promise manager
// Used to create Promises/A promises and to help in implementing
// unit and bind for Promises/A

when = require('when');

//-------------------------------------------------------------
//
// Promise Monad
//
// This defines unit and bind, the two fundamental Monad operations
//
//-------------------------------------------------------------

PromiseMonad = {
	// Given a value, return a corresponding monadic value
	// In this case, given a value, return a promise for that value
	unit: when.resolve,

	// Apply a function f to the underlying value of a monadic value
	// In this case, given a promise, apply f to that promise's resolved value
	bind: when,

	// Two promises are equivalent if their resolved values are equivalent
	// This helper observes two promises and compares their underlying
	// values, and is used to validate the monadic laws for Promises/A below.
	compare: function(left, right, msg) {
		return when.all([left, right], function(results) {
			var eq = results[0] === results[1];
			console.log(msg + ': ' + eq);
			return eq;
		}).otherwise(function(e) {
			console.error(e);
			throw e;
		});
	}
};

// Other helpers and setup

// Simple helper to produce a monadic value *without* using unit()
function m(x) {
	var d = when.defer();
	d.resolve(x);
	return d.promise;
}

// Expected values for validation
a = { name: 'a' };
b = { name: 'b' };

// Simple test functions
function f(x) { return a; }
function g(x) { return b; }

//-------------------------------------------------------------
//
// Proof
//
// Promises/A satisfies the 3 Monadic Laws
//
//-------------------------------------------------------------

//-------------------------------------------------------------
// Law 1
// unit a >>= f == f
// f bound to unit(a) == f(a)

leftResult  = PromiseMonad.bind(PromiseMonad.unit(a), f);

rightResult = f(a);

// A little strange here in that only leftResult is a promise
// so technically only have to observe leftResult, but we'll
// just reuse PromiseMonad.compare anyway.
PromiseMonad.compare(leftResult, rightResult, 'Law 1: unit a >>= f == f');

//-------------------------------------------------------------
// Law 2
// m >>= unit == m
// unit bound to promise value == promise value

leftResult  = PromiseMonad.bind(m(a), PromiseMonad.unit);

rightResult = m(a);

PromiseMonad.compare(leftResult, rightResult, 'Law 2: m >>= unit == m');

//-------------------------------------------------------------
// Law 3
// (m >>= f) >>= g == m >>= (\x -> f x >>= g)
// Or, perhaps more simply: (f >=> g) >=> h == f >=> (g >=> h)
// promise function composition is associative

leftResult = PromiseMonad.bind(PromiseMonad.bind(m(a), f), g);

rightResult = PromiseMonad.bind(m(a), function(x) {
	return PromiseMonad.bind(f(x), g);
});

PromiseMonad.compare(leftResult, rightResult, 'Law 3: (m >>= f) >>= g == m >>= (\\x -> f x >>= g)');

@briancavalier

This is a cursory assessment, but it looks like PromiseMonad is just a functor from some category representing regular JavaScript objects and morphisms to the Promise category where the objects are promises and the morphisms are from promise to promise (lifted by when).

The reason I say that is that there's no join equivalent ( see http://en.wikibooks.org/wiki/Haskell/Category_theory#Monads ). That is no way to wrap a Promise in a Promise.

I've also had another colleague suggest that a Promise is effectively an Identity monad.

Here's a quick take on join, but I'm not as familiar with it, so let me know if this seems like it's in the right direction. Basically, just trying to show that M(M(x)) == M(x) as in that category theory link.

leftResult = PromiseMonad.unit(PromiseMonad.unit(a)); // M(M(x)) ?
rightResult = PromiseMonad.unit(a); // M(x)

// Logs: Join: M(M(x)) == M(x): true
PromiseMonad.compare(leftResult, rightResult, 'Join: M(M(x)) == M(x)');

join should have type M (M a) -> M a -- that is, it's a function that takes a nested monadic value and produces a "flattened" version. @johnbender is right that you can't write this function for Promises because you can't create a nested Promise. You would have to be able to do something like this:

var nested = Promise.unit(Promise.unit(a));
Promise.bind(nested, function (inner) {
  // inner is also a Promise
  Promise.bind(inner, function (val) {
    assert(val === a);
  });
});

In your example, you'd want to show that join(leftResult) == rightResult.

I'm also no expert in monads, but when I saw when and Promises I instantly thought it was monad-ish, which is how I ended up at this gist. It seems like a nesting of the error monad in the continuation monad, in that it handles the plumbing for errors and for CPS, but that's just based on my intuition.

Plus some rules are broken to make it more convenient (for instance, when and resolve take Promises or values, when strictly when should take only Promises and resolve should take only values. It might be interesting to write a strict version of the error+continuation monad and see if it gives the same behavior.

@jonahkagan Ah, thank you for clarifying. I've been debating whether M(M(a)) should even be allowed at all for promises. Part of me feels strongly that for practical reasons, there should be no observable difference between M(a) and M(M(a)), i.e. when.resolve(when.resolve(x)) == when.resolve(x), which raises some interesting question about rejected promises. For example, it would mean:

when.resolve(when.reject(x)) == when.reject(when.resolve(x)) == when.reject(x)

Which seems intuitive to me, but maybe not to others. The idea is that rejected promises must be explicitly handled or the rejection propagates. That sounds like it may fit with your thoughts about Error+Continuation monads. If you have more thoughts on that, I'd be very interested to hear!

Did you know that Douglas Crockford thinks he is the first to have found exactly that, Promises are a monad. The code for this talk is here.
It's fun, as always with Douglas. Take for example only the title: "Monads and Gonads". But, also as always, I was thinking by myself: let us not forget we're all mortal... where "Douglas" ∈ "us" ;)

---

Personally, I strongly believe that the concept (as opposed to Promises/A or a particular implementation like when.js) of Promises or Futures is a monad. I also think that it does incorporate the Error (aka "Exception") monad. This is to say that the Maybe monad wouldn't suffice, because the onReject is passed a reason.

I know that C#'s Tasks are a comonad (a comonad is the categorical dual of a monad; here the difference is roughly that between a "push" model [Promises] and a "pull" model [Tasks]).

Re the Continuation monad I'm not sure. That is because what Promises encapsulate / let you abstract from is the _delay_ or _time consumed_ by a computation. Note that this NOT only pertains to parallel (aka "async") computations. Sure, you pass callback functions that can legitimally be viewed as continuations. But hey, every monad has that. The 2nd argument to bind (aka shove aka >>=) is just that.
The computation time is specific to the platform and a rather low-level property (hence it's a good idea to abstract from it). To me this feels rather like the IO monad. Which, btw, also "hides" from you the actual time it takes to read in, say, a 2GB file. That's not to say that Promises can be built from IO, only that I see more similarity.
But as said, I'm not sure.

Re the Identity monad: this is really only a wrapper, nothing else. In a statically typed language as eg Haskell it can (and actually is) simply "compiled away". So in comparison to Promises it at least lacks the Error aspect (dispatching either to onResolve or onReject as well as, in case of rejection, giving a reason).
Well, it of course depends on how one defines "effectively".
Ask yourself (and your colleague) how "effectively" had to be defined in order to have "Promises are effectively the Identity monad" hold.
I'm afraid that by the same reasoning you could as well end up arguing for programming everything in assembler.
The Identity monad is trivial but that does not keep it from being useful. However, Promises are definitely not trivial.

Re join for the Promises monad: defining unit (aka "return") and bind and have them obey the laws is equivalent to defining unit, fmap and join and have them obey (other) laws. The first is more convenient in a programming context while the latter might be more familiar when you're thinking in categorical terms.
Again, I'm talking about the concept, not when.js.
As has been said, join must have type M(M(a)) -> M(a). Let's first look at another monads' join and then think about what makes sense for Promises:

Maybe a :: Nothing | Just a: think of it as a simplified version of Error (which, as we saw is a key feature of Promises). In the above a is a type variable, so you can have values of type eg Maybe Int or Maybe String or...
This is what people call a type constructor: give Maybe another type and you get a (concrete) type.
To the right of the double colon :: we have value constructors. In this case there's two of them. But that doesn't say that there'll be only two values. Rather (because the type variable also appears on the right) there'll be many possible values BUT each of them belongs to one of two classes. In the case of Maybe the Nothing class has only one inhabitant and the Just class has as many inhabitants as a has.
Now let's just say a is instantiated to Int and see how to construct values of type Maybe(Maybe(Int)). Since only the Just constructor takes a value, there's 3 instead of 4 possibilities, given an Int value x:

Just(Just x)
Just(Nothing)
Nothing

It is important to keep in mind that all 3 are meant to have type Maybe(Maybe(Int)), in particular the last!
Now these are exactly the cases that Maybe's join must cover. The only reasonable way - and in fact the only way if Maybe is to be a monad - is this:

join :: Maybe(Maybe a) -> Maybe a
join Just(Just x) = Just x
join Just(Nothing) = Nothing
join Nothing = Nothing

Again, notice that the right-hand-side type is Maybe a, NOT Maybe(Maybe a). So in the case of Maybe, all that join does is "type-juggling". However, that is NOT true for every monad. For example in the List monad join is a (one-level) flattening operation, and so has to do "real work".

Now for join in Promise. By now you will have guessed where I'm aiming at. Since, as I have claimed, the aspect of computation time is supposed to be "hidden" completely from the user, what's left is the resolve vs rejection aspect.
Wrt that, I claim, the situation is just like with Maybe (setting aside details like a reason, to keep it simple).
Things are, however, not exactly the same, only similar. First and foremost, Promise is not just a simple data type like Maybe. That means in join we cannot simply "look" at which value constructors were used. Rather we have to do "real work". It also means, unfortunately, that I don't have a precise notation. So let's just say

1. Just(Just x) corresponds to neither the inner nor the outer promise rejecting
2. Just(Nothing) corresponds to the inner promise rejecting but not the outer
3. Nothing corresponds to the outer promise rejecting (thus never getting to the inner one ever)

Well, pretty clear which promise join should return:

1. resolves to x
2. rejects, passing on the error reason from the inner promise
3. rejects with just the outer promise's error reason

So in that I slightly disagree with

Part of me feels strongly that for practical reasons, there should be no observable difference between M(a) and M(M(a)), [...]

As you said, it's with rejection where things get interesting (and different).
Again, it depends on the definition of "for practical reasons". If it's only about resolve vs reject then that's somewhat ok.
But still, it's not only about (ignoring) the reason passed in case of rejection. I think you just shouldn't say "no observable difference". I think what you meant is "essentially behave the same". But that is not at all the same as "no observable difference" - and necessarily so.
Let's assume you do have a promise p that (can) resolve to another promise (ie your promise impl does allow this).
How would you get out the final value (without having join)? Something like this:

var finalValue;
p.then(function (p2) {
    p2.then(function (v) {
        finalValue = v;
    }
});

Well, that's just what join would do for you:

join(p).then(function (v) {
    finalValue = v;
}

From that you can see that join can be implemented in terms of bind:

join p = p >>= \x -> x
-- or, more concisely:
join = (>>= id)

In fact this is true for any monad, because defining unit, fmap and join is equivalent to defining unit and bind.
Also note that this implies that join must have type M(M(a)) -> M(a), dictated by the types of bind and id.

I wrote a blog about this last year: http://kybernetikos.com/2012/07/10/design-pattern-wrapper-with-composable-actions/

I'd like to see similar proof for Promises/A+. Notice the case when onFulfilled returns promise. Then works then as flatMap. If returned value is not promise then it works as map.

I don't get why the spec doesn't require a promise to be returned from the then/catch callbacks. Then you wouldn't need to have this annoyingly-complicated 'promise resolution procedure', and you could wrap promises in promises. Seems like they're just overcomplicating and restricting things just for the sake of being able to write return value; instead of return Promise.resolve(value);.

Oh, and to replace the behaviour of passing a thenable to Promise.resolve, new Promise(thenable.then.bind(thenable)).

Unless there is another reason, such as performance?

You can also alias the more common method names (resolve -> of, then -> chain), but here's a quick proof for ES6 Promises.

//Left Identity
(function(){
  var value = 6;
  var p_func = x => Promise.resolve(value+6);
  var left = Promise.resolve(value).then(p_func);
  var right = p_func(value);

  Promise.all([left, right]).then(([lVal,rVal]) => console.log(lVal === rVal, {lVal,rVal}));
}());

//Right Identity
(function(){
  var value = 6;
  var left = Promise.resolve(value);
  var right = Promise.resolve(value).then(x=> Promise.resolve(x));

  Promise.all([left, right]).then(([lVal,rVal]) => console.log(lVal === rVal, {lVal,rVal}));
}());

//Associativity
(function(){
  var f = a => Promise.resolve(a * a);
  var g = a => Promise.resolve(a - 6);
  var m = Promise.resolve(7);
  var left = m.then(f).then(g);
  var right = m.then( x => f(x).then(g) );

  Promise.all([left, right]).then(([lVal,rVal]) => console.log(lVal === rVal, {lVal,rVal}));
}());

Promise.resolve won't work quite like a standard MType.of/return/point, unfortunately, so if you wanted to create an .of method, it wouldn't be a simple alias and you'd have to do something like:

Promise.prototype.of = x => Promise.resolve(x);
Promise.of = Promise.prototype.of;

And as noted, .then is overloaded/too-smart because it checks the result and doubles as .map if it's just a value, instead having explicit map/flatMap methods. The laws don't really care about map though (since it can be derived from flatMap/chain as long it obeys those laws). It's just that doing so with the overloaded .then becomes a bit silly/pointless:

Promise.prototype.map = function(fn){
  return this.then( x=> Promise.resolve(fn(x)) );
};