ExpandCollapseNext Index

+ 1.1 Felix for monadic programming

"In plain terms, a monad is a set of rules that enforce regular behavior but broad enough to allow most computational processes to be expressed as a monad." --http://c2.com/cgi/wikiMonadicProgramming"

+ 1.1.1 The maybe monad

If a is a type variable and M a is a type, then the characteristic property of M if it is a monad, is that, there exists a function bind of type M a -> (a -> M b) -> M b for b another type variable (perhaps but not at all neccessarily the same as a). I suggest that perhaps a helpful interpretation of M a is that of M as a type function applied to a type a.

It seems that one of the easier monads to start with in the study of monadic programming is the "maybe" monad built over something like the Felix opt[T] types (see http://felix-lang.org/lib/std/option.flx and http://felix-lang.org/test/regress/monad-01.flx). Here's something equivalent applied to the problem of "safe integer arithmetic". By "safe" we simply mean trying to evaluate expressions while watching out for division by zero and under/overflow.

To get going first define the sum success[T] to which later will be imbued monadic properties.

  union success[T] = 
    | Success of T
    | Failure of string
    ;

Instances of success[T] are values. There are two possibile patterns against which to match a given value : Success a and Failure[a] s (in the nomenclature of Haskell and Ocaml, Success and Failure are "data constructors", success[T] is a type constructor.). Consider for example the function str for any x:success[T]:

  instance[T with Str[T]] Str[success[T]]
  {
    //success[T] satisfies the requirements of the typeclass Str (if the
    //same can be said of T)
  
    fun str (x:success[T]):string =>
      match x with 
        | Success t => "Success " + (str t)
        | Failure s => "Failure " + s
      endmatch
      ;
  }

Here is where things get interesting:

  typedef fun Fallible (t:TYPE) : TYPE => success[t] ;

This is a type function. Fallible is a function in one type argument with domain and codomain both TYPE. The type this computation results in specifically is success[t].

The following syntax declares the intent to make a monad out of Fallible:

  instance Monad[Fallible]
  {

Now, the crucial definition for bind (pay particular attention to bind's type and compare it with the type spelled out in the introduction!)

    fun bind[a, b] (x:Fallible a, f: a -> Fallible b):Fallible b =>
      match x with
        | Success a => f a
        | Failure s => Failure[b] s
      endmatch
      ;

One last ingredient is needed to make this (almost) monad useful. We need a function to "lift" values of type a into the monad Fallible a. The usual name for this function is return and is obliged to have type a -> M a. In Felix, the convention is to denote this function ret[T]:

    fun ret[a](x:a):Fallible a => Success x ;
  
  }//instance Monad[Fallible]

That's it for defining the monad. The functions implementing safe arithmetic read as follows.

  //Safe arithmetic. 
  
  const INT_MAX:int requires Cxx_headers::cstdlib ;
  const INT_MIN:int requires Cxx_headers::cstdlib ;
  
  fun madd (x:int) (y:int) : success[int] => 
    if x > 0 and y > (INT_MAX - x) then
        Failure[int] "overflow"
    else
      Success (y + x)
    endif
    ;
  
  fun msub (x:int) (y:int) : success[int] => 
    if x > 0 and y < (INT_MIN + x) then
      Failure[int] "underflow"
    else
      Success (y - x)
    endif
    ;
  
  fun mmul (x:int) (y:int) : success[int] => 
    if x != 0 and y > (INT_MAX / x) then
      Failure[int] "overflow"
    else
      Success (y * x) 
    endif
    ;
  
  fun mdiv (x:int) (y:int) : success[int] => 
      if (x == 0) then 
          Failure[int] "attempted division by zero" 
      else 
        Success (y / x) 
      endif 
      ;

Hopefully the syntax of the functions

fun madd (x:int) (y:int) : success[int] => //... ;

didn't confuse you? madd above is a function in its "curried" form. A function like fun f (x:a)(y:b) is a shorthand for fun f (x:a) => fun (y:b). Looked at this way it's clear that there really isn't any such thing as a multi-argument function in mathematics or Felix. Functions take (at most) one argument! If you find that confusing don't worry - most everyone needs a while to get that idea.

Enabling the monadic interpertation of success[T] is achieved with the directive

  open Monad[Fallible] ;

... and now we're ready to to build and evaluate arithmetic expressions.

  //Evalue some simple expressions.
  
  val zero = ret 0 ;
  val zero_over_one = bind ((Success 0), (mdiv 1)) ;
  val undefined = bind ((Success 1),(mdiv 0)) ;
  val two = bind((ret 1), (madd 1)) ;
  val two_by_one_plus_one = bind (two , (mmul 2)) ;
  
  println$ "zero = " + str zero ;
  println$ "1 / 0 = " + str undefined ;
  println$ "0 / 1 = " + str zero_over_one ;
  println$ "1 + 1 = " + str two ;
  println$ "2 * (1 + 1) = " + str (bind (bind((ret 1), (madd 1)) , (mmul 2))) ;
  println$ "INT_MAX - 1 = " + str (bind ((ret INT_MAX), (msub 1))) ;
  println$ "INT_MAX + 1 = " + str (bind ((ret INT_MAX), (madd 1))) ;
  println$ "INT_MIN - 1 = " + str (bind ((ret INT_MIN), (msub 1))) ;
  println$ "INT_MIN + 1 = " + str (bind ((ret INT_MIN), (madd 1))) ;
  
  println$ "--" ;

It's suprising what looking at things a different way can bring.

  syntax monad //Override the right shift assignment operator.
  {
    x[ssetunion_pri] := x[ssetunion_pri] ">>=" x[>ssetunion_pri] =># "`(ast_apply ,_sr (bind (,_1 ,_3)))";
  }
  open syntax monad;

Here the traditional rshift-assign operator is substituted for bind (I won't pretend to tell you that I understand the details of how!). Now safe arithmetic expressions are so naturally represented as computation chains!

  println$ "zero = " + str (ret 0) ;
  println$ "1 / 0 = " + str (ret 1 >>= mdiv 0) ;
  println$ "0 / 1 = " + str (ret 0 >>= mdiv 1) ;
  println$ "1 + 1 = " + str (ret 1 >>= madd 1) ;
  println$ "2 * (1 + 1) = " + str (ret 1 >>= madd 1 >>= mmul 2) ;
  println$ "INT_MAX = " + str (INT_MAX) ;
  println$ "INT_MAX - 1 = " + str (ret INT_MAX >>= msub 1) ;
  println$ "INT_MAX + 1 = " + str (ret INT_MAX >>= madd 1) ;
  println$ "INT_MIN = " + str (INT_MIN) ;
  println$ "INT_MIN - 1 = " + str (ret INT_MIN >>= msub 1) ;
  println$ "INT_MIN + 1 = " + str (ret INT_MIN >>= madd 1) ;
  println$ "2 * (INT_MAX/2) = " + str (ret INT_MAX >>= mdiv 2 >>= mmul 2 >>= madd 1) ; //The last one since we know INT_MAX is odd and that division will truncate.
  println$ "2 * (INT_MAX/2 + 1) = " + str (ret INT_MAX >>= mdiv 2 >>= madd 1 >>= mmul 2) ;

As an aside, I understand these constructions are called "workflows" in the F# community?

In the next section we will examine arguably one of the harder monads to understand. As you will see, Felix type notations make it not that much harder than the maybe monad and help deepen one's understanding considerably!

+ 1.1.2 The state monad

Revenge of the monads is coming. Only the code for the example is here right now now... Check back soon!

  
  //State monad.
  
  union state[s, a] =
   | State of (s->a*s)
   ;
  
  fun run_state[s, a] (x:state[s, a]):(s->a*s) =>
   match x with
     | State u => u
   endmatch
    ;
  
  typedef fun StateGen (s:TYPE) (a:TYPE) : TYPE => state[s, a] ;
  
  instance[s] Monad[StateGen s]
  {
   fun bind[a,b](x:StateGen s  a, f:a->StateGen s b):StateGen s  b =
   {
     val run0:(s->a*s) = run_state x ;
     fun run1 (state0:s):(b*s) =
     {
       val t:a*s = run0 state0 ;
       return (run_state (f t.0)) t.1;
     }
  
     return State run1 ;
   }
  
   fun ret[a](x:a):StateGen s a =
   {
     return State (fun (st:s):a*s => (x, st)) ;
   }
  }
  
  //--
  //
  //Test.
  
  struct counter
  {
   value : int ;
   number_of_increments : int ;
  };
  
  instance Str[counter]
  {
   fun str (c:counter):string =>
     "Counter (value = " + str (c.value) +
     ", number_of_increments = " + str (c.number_of_increments) + ")"
     ;
  }
  
  fun increment_counter (c:counter):(int*counter) =>
   (c.value, counter (c.value+1, c.number_of_increments+1))
   ;
  
  val increment_counter_state : state[counter, int] = State increment_counter ;
  
  open Monad[StateGen counter] ;
  
  val increment_counter_twice_state =
   bind (increment_counter_state, (fun (x:int):state[counter,int] => increment_counter_state)) ;
  
  println $ str ((run_state increment_counter_twice_state) (counter (24, 3))) ;
  
  syntax monad //Override the right shift assignment operator.
  {
     x[ssetunion_pri] := x[ssetunion_pri] ">>=" x[>ssetunion_pri] =># "`(ast_apply ,_sr (bind (,_1 ,_3)))";
  }
  open syntax monad;
  
  val g = increment_counter_state >>= (fun (x:int):state[counter,int] => increment_counter_state) ;
  println $ str ((run_state g) (counter (24, 3))) ;