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 typethey 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) inverseness 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.
