Lambda the Ultimate

The whole point of this paper is that reflect and reify somehow improve the encapsulation of monad operations. These they define as macros:

(define-syntax reify
  (syntax-rules ()
    ((reify (?var ?producer1)
       ?producer2)
     (bind (?var (unit ?producer1))
       ?producer2))))


(define-syntax reflect
  (syntax-rules ()
    ((reflect (?var) ?expression)
     (mult (return (lambda (?var) ?expression))))))

The thing is that, because of the monad laws, one has: (bind (V (unit E1)) E2) = (let ((V E1)) E2) and (mult (return E)) = E. Consequently, reify is essentially sugar for let, and reflect is sugar for lambda.

"Where's the beef?"

Filinski, in Representing Monads, defines reify and reflect by the following rules (quoting Moggi):

For any expression E of type Ta, reflect(E) is a computation that returns the value of type a and does the effect described by the monad constructor T. For any general computation E of type a, reify(E) is a "pure" value of type Ta.

  reify(reflect(V)) === V
  reflect(reify(E)) === E

Thus, according to Filinski, both reify and reflect apply to expressions. In the Sobel et al. paper, reify and reflect are binding forms. Furthermore, according to Filinski, reify and reflect must be inverses. In the Sobel et al. paper, reify and reflect don't even compose! One can't avoid the impression that reify and reflect in the paper are mis-named: the reflect form in the paper yields a lambda-expression -- a pure value. That's the job of reify!

In Scheme, the examples of reify and reflect are delay and force.

I contend that it is more insightful to view the running example of the paper (and other examples in Section 2.2) as combinator parsing. We have simple parsers (digit, empty) from which we can build more complex parsers with sequencing and alteration combinators. The fact that sequencing looks like 'bind' is just a coincidence (Monad is a sufficiently general concept, so appears in many places. It is not always insightful). Combinators neatly hide the plumbing details -- the input and the output streams. If we consider the parsing problem in the paper to be an instance of combinator parsing, the issue of monadic grammar disappears. We simply have a set of combinators, which may combine parsing expressions of particular types. In a typeful language, the type system reinforces the conventions. Instead of monad laws, we have combinator laws, which are generally richer.

The paper will confuse the reader about monadic reflection and reification.

The reader was already confused about monadic reflection and reification :)

I'm not so sure that Sobel et. al. got it wrong. If you go back to Filinski, you'll see

Then reflect(E) (writing "reflect" for "mu") expresses the value of E:alpha + exn as a computation: we get an exception raising construct by raise E === reflect(inr E)

His type rule is:

   Gamma |- E:T(alpha)
----------------------


Gamma |- reflect(E):alpha

But he's really using T(alpha) here as an abbreviation for alpha + exn (notice how his example is reflect(inr E), and we don't expect to be able to explicitly construct computations in the monad using something so mundane as inr). And the result type of reflect(E) is "a computation", so it's surely of a monadic type. Like in Moggi's metalanguage, all the types tau on the right hand side of the turnstile will be interpreted as T(tau).

In fact, if you go back to Moggi, you'll see that the semantics of reflect is g;mu_[alpha], where mu is the multiplication of the monad. Then, mu_[alpha] is an arrow from T(T(alpha)) -> T(alpha), so clearly no matter what g it's composed with, it will yield a T(alpha) in the semantics.

And likewise for reify ([.]), where Filinski does an explicit case on the value of a reified expression. We don't expect case to be able to see inside values of monadic type---they type T(alpha) in the rule is an abbreviation for alpha + exn.

Sobel et. al. are trying to say that we gain something by being explicit about the distinction between the left and right hand sides of

T(alpha) = alpha + exn

and using reflect to go from right to left and reify to go from left to right (even in combinators that are "in the know" about the monad, like orelse). Namely, what we gain is the ability to implement T(alpha) as something other than alpha + exn.

I'm pretty sure that you can get back the (sort of) inverse-ness of reify and reflect using the definitions from the Sobel paper if you write:

(reify (x (reflect (y) E)) x) ===> (lambda (y) E) as a parser value

(reify (x E) (reflect (y) (x y))) ===> (lambda (y) (E y)) as a parser value

Note that reflect has an extra lambda in its expansion (that could have been, but wasn't, written by the programmer), because otherwise "lambda" would have to be part of the syntax of reflect (for this monad).

In the Sobel et al. paper, reify and reflect are binding forms.

Weren't they in the Moggi paper too, where terms in the meta language and programs in the programming language all had a single free variable?

Frank Atanassow is right, I think. (The first definition of) reify is just a let that blesses the bound variable as something that can be applied to a token stream yielding a pair of new stream and either result or failure. And reflect is just sugar for a lambda, but they need to reflect macro form as a hook to add extra arguments later in the paper.

Later, they will eliminate a bunch of closure creation. And then they will implement reflect as a macro generating macro, and reify as a let (becuase the token stream is always available). But, (they claim that) they couldn't have done this without reify and reflect.

Anyway, what I think about this paper is that it is an interesting way to "discover" monads. Just write a bunch of functional programs that contain an encoding of imperative effects, and abstract the common patterns out.

Ah, that explains a few things. It looks like Sobel's page has not been updated since Sep. 2002, and probably not for a while before that. CiteSeer says his last publication was in 1999.

Kevin: Sobel et. al. are trying to say that we gain something by being explicit about the distinction between the left and right hand sides of T(alpha) = alpha + exn

That is the only sense I could make out of it too. But it's a trivial observation, and has nothing to do with monads or reflection. In Haskell, it just amounts to an admonition to make T (more) abstract:

data T alpha = T (Either alpha Exn)

which is standard practice anyway. There is not much point in defining two new operators for this, since they both factor through the data constructor T.