Tue Jan 18 18:49:06 EST 2011

Using the SC monad

The next step in [1] 3.4 is to specialize the monad so that let
insertion can be used.  First we need to figure out which type is
exactly specialized, and define monad laws.

Why are the value and answer types not always the same in the rules
described in 3.4 [1]?

As I understand it, the specialized returnN operation can't be used as
a generic return, simply because it is not generic enough:

returnN :: Expr -> SC Integer Expr Expr
returnN x = SC f where
    f s k = Let n x (k s' (Var n)) where
                    (n, s') = allocVar s

The type of `x' is fixed.  This should be possible to solve by
generalizing the functionality of the Let from a concrete data type to
an abstract operation.  In [1] the operations are made ``smart'' to
avoid duplication of simple expressions such as literals.  This
smartness should not be part of the definition of `return'.

A straightforward rewrite is to just lift out the whole return

maybeBind x s k =
    Let n x (k s' (Var n)) where
            (n, s') = allocVar s

returnN = SC . maybeBind


  * Why are the expression and result types different in [1]?  Maybe
    it was a different paper that explained this, but I do remember
    clearly that there was a specific reason.

To simplify I'm going to take that out as I see no reason for it now
apart from complicating the types.

The explanation in [2] is a bit less dense and easier to follow.

[1] http://www.cs.rice.edu/~taha/publications/conference/pepm06.pdf
[2] http://www.cas.mcmaster.ca/~carette/publications/scp_metamonads.pdf