Skip to main content

Monads and Asynchronous Ajax with Javascript


Monads are often seen as a very basic part of the language for haskellers and something completely obscure for programmers which use other, especially non-functional, languages. Even lispers and schemers tend not to use them consciously to any great extent, even though they can help with a number of common problems that occur - perhaps most obviously with functions returning nil in a chain of compositions.

Monads, or Kleisli triples have a formal mathematical meaning which requires satisfaction of a few basic axioms. However, we can understand them fairly simply as a pattern which involves a bind operator which allows us to compose our monad objects, and a unit operator which allows us to lift a value up into one of monad objects.

MonadPlus extends this pattern and allows us a new type of composition +, and a new unit, called mzero that is somewhat like "plus" in the sense that + doesn't do anything when composed mzero.

MonadPlus turns out to be an excellent setting for conveniently dealing with concurrency. So it was that after playing with ajax for a while I found myself irritated with the way in which I had to wrap up continuations in order to get the sequencing behaviour I wanted. It occurred to me that what I really wanted was a MonadPlus.

I started writing one myself and realised that since my knowledge of javascript arcana was somewhat thin (one needs not simply implement them - they also have to be convenient to use!), I'd be better off finding out if someone else had already done it, and hence came to Douglas Crockford's video of javascript monads.

In this video Crockford demonstrates how to roll up a monadPlus object which he calls a vow. In his framework, he has a single composition function when which acts as a combination of bind and +. In order to lift a value into the monad, we use vow.keep(data). Since he doesn't use a strongly typed language, he's able to be a bit more flexible in what actually gets put in his when. In the example functions below, I always return a promise, which can be used by the next function in the chain - this is the standard way that bind works, composing functions (f : a → M b). However, the plumbing written by Crockfort will also automatically lift a function (f: a → b) into the monad, in the event that you have an immediate value and not a promise. Similarly, instead of composition with alternatives, we have our failure function in the right hand side.

This conveniently expresses a combination of "and/or" type asynchronous operators in a single convenient framework. We don't need to worry about when the asynchronous calls return - we are guaranteed that if they do, the next positive function in the chain will be called. If they don't return, we will fall over to our first error handler.

I wrote a quick application that demonstrates how you might use Crockfort's vows:

var iphost = "http://api.hostip.info/get_json.php";
  var countryhost = "http://api.hostip.info/get_json.php?ip=";
  function getIP(){ 
      var vow = VOW.make(); 

      var ajs = { 
          type : 'GET', 
          url : iphost, 
          dataType: 'json', 
          success : function(data){ 
              vow.keep(data.ip);
          }, 
          error: function(x,e){ 
              vow.break([x,e]);
          }
      }
      $.ajax(ajs);
      return vow.promise;
  }
  
  function countryOf(ip){ 
      var vow = VOW.make(); 

      var ajs = { 
          type : 'GET', 
          url : countryhost + ip, 
          dataType: 'json', 
          success : function(data){ 
              vow.keep(data.country_name);
          }, 
          error: function(x,e){ 
              vow.break([x,e]);
          }
      }
      $.ajax(ajs);
      return vow.promise;
  }

  function display(data){ console.log(data);}
  function showError(data){console.log("Error "+data);}

  $(document).ready(function (){
      getIP()
          .when(countryOf)
          .when(display, showError)
      
  });


UPDATE: Much to my surprise, all of this behaviour is already implemented with deferred ajax calls, using "then". It even manages to lift functions which don't return a promise into a promise automatically.

Comments

Popular posts from this blog

Generating etags automatically when needed

Have you ever wanted M-. (the emacs command which finds the definition of the term under the cursor) to just "do the right thing" and go to the most current definition site, but were in a language that didn't have an inferior process set-up to query about source locations correctly (as is done in lisp, ocaml and some other languages with sophisticated emacs interfaces)?

Well, fret no more. Here is an approach that will let you save the appropriate files and regenerate your TAGS file automatically when things change assuring that M-. takes you to the appropriate place.

You will have to reset the tags-table-list or set it when you first use M-. and you'll want to change the language given to find and etags in the 'create-prolog-tags function (as you're probably not using prolog), but otherwise it shouldn't require much customisation.

And finally, you will need to run etags once manually, or run 'M-x create-prolog-tags' in order to get the initia…

Decidable Equality in Agda

So I've been playing with typing various things in System-F which previously I had left with auxiliary well-formedness conditions. This includes substitutions and contexts, both of which are interesting to have well typed versions of. Since I've been learning Agda, it seemed sensible to carry out this work in that language, as there is nothing like a problem to help you learn a language.

In the course of proving properties, I ran into the age old problem of showing that equivalence is decidable between two objects. In this particular case, I need to be able to show the decidability of equality over types in System F in order to have formation rules for variable contexts. We'd like a context Γ to have (x:A) only if (x:B) does not occur in Γ when (A ≠ B). For us to have statements about whether two types are equal or not, we're going to need to be able to decide if that's true using a terminating procedure.

And so we arrive at our story. In Coq, equality is som…

Formalisation of Tables in a Dependent Language

I've had an idea kicking about in my head for a while of making query plans explicit in SQL in such a way that one can be assured that the query plan corresponds to the SQL statement desired. The idea is something like a Curry-Howard in a relational setting. One could infer the plan from the SQL, the SQL from the plan, or do a sort of "type-checking" to make sure that the plan corresponds to the SQL.

The devil is always in the details however. When I started looking at the primitives that I would need, it turns out that the low level table joining operations are actually not that far from primitive SQL statement themselves. I decided to go ahead and formalise some of what would be necessary in Agda in order get a better feel for the types of objects I would need and the laws which would be required to demonstrate that a plan corresponded with a statement.

Dependent types are very powerful and give you plenty of rope to hang yourself. It's always something of…