A new term language for monads

Taking a break from posting at the end of Lent has left me somewhat backlogged; but, before i get back on the main thread i wanted to document a little gem that flashed by the other day. Since monad tutorials are now a cottage industry i felt i ought to do the obligatory tut' via a little pedagogical device: monads as colored braces. This is essentially the Eilenberg-Moore take on Wadler's comprehending monads. It seems a natural thing to do because XML is essentially colored braces. Along the way, however, i started asking myself what constitutes the "color" set for coloring the braces. i realized that you can color the braces with terms.

Moreover, there is this Godelian trick to achieve what Haskell achieves with typeclasses + do-notation. Specifically, the do-notation works because the ad hoc polymorphism support in typeclasses allows programmers to provide definitions for unit and bind for a given color of brace. i realized that with a little reflection you can achieve the same thing by making the color of a given brace be the term that implements unit and mult-or-bind.

Below is a little BNFC code which will generate Haskell data types and a parser for the term language.

Application . Term ::= "(" Term [Term] ")" ;
Abstraction . Term ::= "lambda" [Variable] "." Term ;
Reference . Term ::= Variable ;
Zero . Term ::= "0" ;
Embracing . Term ::= Embrace ;

Quotation . Variable ::= "@" "{" Term "}" ;
Variation . Variable ::= Ident ;

Unity . Embrace ::= "{" Color "|" Term "|" Color "}" ;
Multiplicity . Embrace ::= "*" "{" Color "|" Embrace "|" Color "}";
Interchange . Embrace ::= "~" "{" Color "|" Embrace "|" Color "}";

Coloring . Color ::= Variable ;

[] . [Variable] ::= ;
(:). [Variable] ::= Variable [Variable] ;

[]. [Term] ::= ;
(:). [Term] ::= Term [Term];

i'm going to have to do the detailed unpacking a little later as i'm getting hungry... But, these are the essential elements of the approach.

• Use the idea of injecting the λ-calculus into a term language for monad expressions
• The term language of expressions is essentially
  • unit for the monad associated to color k is written: {k| t |k}
  • mult for the monad associated to color k is written: *{k| {k| t |k} |k}
  • and, because we want to demand distributivity over our monads we ask for an interchange expression #{j| {k| t |k} |j}
    
• Finally, we use terms themselves as colors, k.