1. Reflection in Logic: Truth Predicates

For simplicity, we assume a positive (no negation), implicational logic with a single predicate T. T-introduction incorporates the fact that if A holds, then the predicate T holds for the name of A. T-elimination affirms that the reverse also holds: if T holds for the name of some sentence A, then A holds.

While extremely simple, the T-biconditionals incorporate our basic intuitions about a meta-level: T is about the base language, and its behavior reflects that of the theory.

2. The Constructive Approach

We take typed l_v-calculus terms as proofs and use standard reductions to extract witnesses. Examples of term construction are: Ù -introduction corresponds to pairing; Ù -elimination to projecting out components of a pair; Ú -introduction to disjoint unions; Ú -elimination to dispatch based on the union; Þ -introduction to procedures; and modus ponens to application and so on. The rules of the logic can be considered to be typing rules of the corresponding operators.

How can we interpret truth predicates this way? We must first introduce operators into the l_v-calculus that correspond to truth predicates. Let us define operators Ý (reify) and ß (reflect) to correspond to (that is, with typing rules) T-introduction and T-elimination. Let us call these operators reflective operators. These operators must be given a computational interpretation consistent with the constructive interpretation of truth predicates. What is the constructive interpretation of truth predicates? Let us look at T-introduction. If we are given a proof p for a sentence A, then Ý p must give a proof of the assertion that a proof for A exists. We can simply take this proof to be p. The proof of T() is witnessed by some representation of p. This is what Ý p must evaluate to. T-elimination can be interpreted similarly. Given a proof p of the existence of a proof of A, ß p must give rise to a witness for A.

Let us take an example. It is often attractive to optimize functions at run time based on information available when all the data to a program are available. No widely used programming language actually supports this. What we would like to write is a function f that takes in the representation of a function g and returns a new representation of g that is optimized based on run-time information. The new g can now be incorporated in the program. Suppose that we have written f. How can we think about a program that uses f ? Let us consider a function R, say of type A Þ A. A run-time optimization of this can be written as follows: ß (f (Ý R)). We take a representation of R using Ý , process it through f, and incorporate the optimized function using ß . Let us try to look at this program as a proof. The way to read the following is that the proposition to the right of the ':' is a formula and the term to its left is a proof of that formula. The horizontal lines represent application of inference rules, and the rule used is written to the right of the line.

This also can be read in another way: as an inference of the type of ß(f(ÝR)). The formula to the right of the ':' is the type of the term to the left of ':'. The horizontal lines are applications of type-inference rules.

3. Establishing the properties of Ý and ß .

Since we are interpreting proofs as programs, our ability to reason about these programs is determined by what programs we consider to be equivalent to one another. For l_v-calculus terms, this equality is given by the calculus itself. With the introduction of reflective operators, our calculus must be augmented with rules about how programs containing reflective operators behave. In this section, we state some desirable properties of these operators, without actually giving a real operational semantics to these operators. In later sections, we instantiate the semantics of these operators with existing ones to evaluate them in the context of these properties.

Our first observation is that the rules T-introduction and T-elimination are symmetric. This suggests that the operators Ý and ß ought to be inverses of each other. Indeed, going back and forth between a proof and its representation does not change either the proof itself or its representation. We propose the following equalities. If p proves A, p=Ý ß p and p=ß Ý p. Let us call these properties Ý ß -inverse and ß Ý -inverse, respectively.

Our second observation is that if we decide that the representations of two proofs are equal, then the proofs must be equal. This gives rise to the following rule: If M and N are equal and give rise to a representation of p, ß M =ß N. Let us call this rule the reflection property. Similarly, we would like to have: if M and N are equal Ý M = Ý N. This is because of the following. Let M and N prove A. The truth of A, T() is witnessed, in essence, by M. Similarly the truth of A is witnessed, in essence, by N. If we thus start out assuming that M and N are equal, it follows that Ý M = Ý N. This is known as the reification property.

Let us start with the simple operators quote and eval present in a language such as Lisp. Lists are used as representations of programs and quote is a mechanism for reifying programs. An added restriction is that quote is not affected by variable bindings; (lambda (x) '(x)) will always return the list (x), regardless of what argument is actually passed to the procedure. Eval takes a quoted program, evaluates it, and returns the result.

Let us see how these operators behave with respect to our rules. For Ý ß -inverse, '(eval exp) is clearly not equal to exp. This is because we use a list-representation for programs. For ß Ý -inverse, (eval 'exp) =exp holds, provided exp is a closed term. It is easy to see that the reflection property also holds for this operational semantics. The reification property, however, fails. This can be seen by taking two equal terms: ((lx. x) 3) and 3, but '((lx. x) 3) is not equal to '3.

Muller [5] develops a theory for these operators and demonstrates that adding these operators affects equational reasoning¾ some things that we think ought to be true turn out not to be so. Clearly, from a reasoning point of view, this operational semantics is unsatisfactory.

Ý and ß are defined in terms of two operators: h and _^*, called inclusion and extension, respectively, and these operators must satisfy the following laws:

Intuitively, h maps a value into a representation of the value and _^* transforms a function that takes a value into a function that takes the representation of that value. By defining h and _^* suitably in the meta-language, the user can control representations of the value. The three laws above guarantee some degree of consistency between a value and its representation. The first law implies that extracting a value from a representation and then mapping it back into the representation is an identity operation. The second law is the opposite of this: Mapping a value and extracting it is an identity operation. The third law says that functions constructed compositionally can be extended compositionally. This allows us to inductively define the extension of inductively constructed functions.

Moggi gives a semantics for the operators Ý and ß through a translation using h and _^*. This translation will be presented in Section 14. Filinski [6] shows that this can be done instead by using the control operators shift and reset. This version is somewhat easier to understand and we present it first.

While a theoretical definition of the operators shift and reset is rather involved, it is easy to explain them in informal terms, using the concept of execution stacks. The operator reset places a marker on the execution stack. The operator shift takes a procedure as an argument. It takes the continuation up to (but not including) the marker closest to the top of the execution stack, converts it to a procedure, and passes it to its argument. The continuation is non-aborting. shift, however, is aborting and pops the execution stack up to (and including) the marker placed on the stack. Operationally, this can be defined as follows:

Filinski defines the operators Ý and ß as follows:

We can thus see that when the representation of a value is reflected into a context, that portion of the context that needs to use the value (that is, up to the closest dynamically enclosing reify) is used as a function that is extended to take a representation instead of a value. This, then is the base-code. The enclosing Ý then presents the representation of the processed value. The meta-code here is the part of the context that receives the value of this reification.

When this model is used, reification is a much more light-weight process. One simply invokes the function h on the value. By describing reflective operators using shift and reset, one obtains the additional benefit of adding continuations to representation of values.

1. Ý ß -inverse:
   
2. ß Ý -inverse: This property is satisfied. The proof is tedious but straightforward, and we omit it here for brevity. Intuitively, however, this can be seen simply by observing that reifying the monad and reflecting it without modification is an identity operation. The proof depends upon the fact that shift and reset are being used in a restricted manner.
3. Reflection and reification properties: It is easy to see that these properties are also satisfied by monadic reflection. h and _^* are defined so that if M=N, then (h M ) = (h N ) and if M=N then M^*=N^*. Moreover, shift and reset also behave similarly.

A consequence of this representation decision is that the theory is not a conservative extension of the lambda calculus¾ things that we think ought to be true turn out not to be so. This follows from the fact that the reification property is not satisfied. Many obvious equivalences between programs are not provable in this theory. The other three properties are satisfied by this theory.

As a trivial example, consider the case where we have a l_v-calculus-based language with reflective operators, but in all our programs, we never use a reflective operator. We can surely use the l_v-calculus to reason about this program. Another example is a restricted use of reflective capabilities wherein we only look at the representation procedures to determine how many variables they need. This might be necessary, for example, when we want to use reflection to build tracing into our procedures. A way to do it would be to take the procedure P in question, determine how many arguments it takes, and construct a wrapper procedure that prints these arguments before passing them on to P. This is a very limited use of reflection. Moreover, only part of the representation information is being used, so we can use (informal) l_v-calculus reasoning mechanisms to reason about programs that use tracing procedures (ignoring the fact that tracing causes characters to be printed on the output stream).

Let us clarify the framework in which we develop reflective monads. In the following, we assume that the underlying calculus is Muller’s M-Lisp calculus [5] l_M. This calculus is the l_v-calculus with added operators for getting the representation of terms and evaluation of terms. We assume the typing rules of the typed l_v-calculus. Representations of terms of type A have the type T(). Consistent with reflective behavior, we differentiate between values and their representations, i.e., l_v |- M=N does not imply that the representations of M and N are the same. As we saw before, this is a crucial ontological assumption which permits us to make finer differentiations between terms. We denote the representation of a term M as . Furthermore, we postulate an operation ¯ such that ¯ =M. We use L_M to denote terms in this language.

The monad structure enables two important properties of reflective languages: separation and regularity. The structural distinction given to _^* allows provides a separation between base code and meta-code. Monad laws, on the other hand, ensure a semantic regularity that allows us to conclude that h and _^* do not affect the base code semantically. This monad structure, however, cannot be used directly in a reflective context where equal terms need not have equal representations. Monad laws could easily fail to hold if the representation chosen is too restrictive.

In order to address this problem, we introduce the concept of a reflective monad that is similar to that of the monad but has the following restrictions. The code for _^* is written L_M. This is the meta-code of the program. Furthermore, this is the only code that is allowed to manipulate representations. All other code is referred to as the base code. The base code is written using L_R. The base code is not allowed to construct term representations, except by using Ý. These restrictions are such that they can be enforced syntactically on a program.

We must also address the question of the nature of representations. The actual representation we choose depends upon the reflective capabilities we want the language to have. Some languages might decide to provide a full representation of the term and its context (as the theory described in Section 8). Others might simply choose to provide a simple interface. An example is call/cc in Scheme, where manipulating the continuation explicitly is not allowed, but a procedure-like interface is available. The assumption we make in the following is that the full representation of a reified context is rarely of any use. It is more important to have detailed representations of what goes into a context.

A reflective monad is a monad where h and _^* have the following behavior. (h M ) returns . Also, h is not defined on open terms. The function _^* is responsible for extending a given function to take a representation of its arguments. This means that depending upon the chosen representation, the monad laws don’t hold a priori. The intent, however, is that there be a structure in place so that the base code that depends on the meta-code in _^* can be assured that it does not semantically affect the base code. That is, if we ignore what the meta-code does with representations and only concentrate on what these manipulations mean semantically, the monad laws hold.

In order to formalize this idea, we introduce a second notion of equivalence » ⁺. Under this equivalence, we unify those terms that evaluate to values that might be different representations of equal terms. Since a key assumption here is that there are no contexts that disinguish representations in L_R we restrict the construction of this equivalence to terms that are only built using the basic lambda calculus syntax and calls to the monad operators h an _^*. Let us denote the set of such terms by L_h,*. The subset of closed terms is denoted by L⁰_h,*. Contexts built from these terms are denoted C_h,*[ ].

This relation captures the notion of evaluation of a term to a value. Here is the notion of reduction in L_M. Whenever we say that converges and denote it as The relation » Ì L⁰_h,* ´ L⁰_h,* is defined to be a set such that:

The idea is that terms are distinguished by contexts only when there exists context which converges with one term and diverges with another. The above definition incorporates the intuition that we are interested only in well-behaved reflective contexts C_h,*[ ]. Let us extend » ⁺ to the relation » that is defined on open terms to be the following. If, for all substitutions s ranging over L⁰_h,* , sM» ⁺sN, then M» N.

does not hold a priori. This is not true in regular monads, where h is assumed to be a function that satisfies the axioms of the l_v-calculus. Note, however, that the following holds by definition of » :

Another difference is that regular monads allow values of the monad type to be constructed explicitly (that is, without invoking Ý). In fact, they sometimes require it. We disallow this in the reflective monad. This is because we want to have a clear idea of where representations are being constructed.

The relation » is reflexive, symmetric and transitive. Moreover, » commutes with =_M. This follows from the definition of » . Under the monad laws, it has other interesting properties that we will examine in the following sections.

(let ((g (reflect (f (reify R)))))
  (g args ...))

This, however, violates our restrictions since we are now using f in base code. In the reflective monad, we write this code a little differently:

(let ((g (reflect (reify R))))
  (g args ...))

The code for _^* is as follows:

(define star
  (lambda (k x)
    (if (run-time-optimizable? x)
        (k (down-arrow (f x)))
        (k (down-arrow x)))))

Here we are assuming the existence of a function that recognizes run-time optimizable functions. This could be done, for instance, by checking for membership in a list of predeclared optimizable functions. Also, note the use of down-arrow to convert from representations to terms.

The way this example works is that when reflect passes on the reified value to its context (denoted in the meta-code by k), it processes it through star. In this example, the context is the binding of the value inside the let form. The meta-code gets a chance to manipulate the reified value when it is processed through star. In our case, this is when the run-time optimization happens. The monad laws, of course, guarantee that this reified value is not changed semantically¾ only representationally.

Let us examine whether star satisfies the monad laws. Assume that the representation property holds. The interesting case is the first law: (h^*) » (h M ). We can see that this holds, because our optimizing function f is an optimizer and does not change its argument semantically.

As an example of reasoning using the inverse property, in the base code, we can use Ý ß -inverse to conclude that this program is semantically equivalent to (R args ...). This is because we know that star satisfies our restrictions.

We have seen how reflective monads are useful in separating out reflective and non-reflective parts of a program. In this section, we develop theoretical results about reflective monads. We are interested in showing that the four desirable properties hold within the framework of reflective monads. We do this by developing a l-theory for it and by showing that this theory is a conservative extension of the (typed) l_v-calculus.

This section takes into account the restrictions placed on reflective programs as given above and forces a rule in the theory that would make all the properties hold for the theory. We show that this is sound by proving that if the restrictions above are satisfied for all reflective programs, the theory is consistent. It is further shown that the theory is a conservative extension of the typed l_v-calculus. The implication of this is that conventional reasoning mechanisms need not be discarded to incorporate reflective capabilities in a language.

Let us define the syntax for our (base) language. The syntax is basically that of the l_v-calculus but also allows (ß term) and (Ý term) as terms, where ß and Ý are as defined for monadic reflection. This set of terms is denoted L_R. The theory l_R is l_v extended to include the four properties discussed earlier.

Define a translation from L_R to L_h,* as follows. This translation "implements" the base language in a meta-language. This is essentially the operational semantics of our base language. (Note that this is identical to Moggi’s translation [3]).

(let ((g (reflect (reify R))))
  (g args ...))

By expanding the let, and applying the above translation for a couple of steps, we get:

The key aspect of the theory l_R is that it reflects the behavior of » . We have the following.

0. Lemma (Substitution).



Proof: (By induction on the structure of P.)

Basis: Then,

Induction: We illustrate with the case for



We can now prove the following theorem:

1. Theorem

l_R |- M=N Þ [M]» [N]

Proof: (By induction on the derivation of l_R |- M=N.)

Basis: We have two cases:

Case 1: The right-hand side is arrived upon using the b_v-axiom. Then we have the following. Let and therefore, . We now have:






Case 2: In the second case, the right-hand side is arrived upon using the inverse properties. The left-hand side then follows from the reflective monad laws.

Induction: The inductive cases are straightforward. The key observation is that in each of the inductive cases, a reflective context C_h,*[ ] remains a reflective context when filled with [M].

What this theorem verifies is that our interpretation of the base language l_R in the meta-language l_M induces an equational theory that is safe to use provided certain properties about the interpretation are satisfied.

We now define a correspondence between the calculi l_R and l_v. We begin by defining an erasure function that replaces all occurrences of (ßM and ÝM ) with These correspond to using an identity monad, where the representation of a value has no additional information beyond the value itself.



 

There is an analogous erasure on types:



 

Note that erasure of terms preserves typing under the above type erasure. An important point to note is that erasure commutes with the substitution operation. We call this the substitution-erasure lemma. The proof is a straightforward induction on the structure of terms.

2. Lemma (Substitution-Erasure).



3. Theorem (Correspondence).

l_R |- M=N Þ l_v |-

This follows immediately from the definition of derivability in l_R and type erasure and substitution-erasure properties. The most interesting case is the base case, where l_R |- M=N using the axiom b. The substitution lemma then applies.

This result is not surprising. In our base language, the operators ß and Ý don’t really do anything. In implementation terms, they are merely "pragmas" to the runtime environment to invoke some special semantically valid processing. We then have the following corollary.

4. Corollary (Consistency)

l_R is consistent.

Proof: The proof of consistency is by contradiction. Take I º (lx.x) and K º (lxy.x) as terms. It is well known that these two terms are not equal in the call-by-value lambda calculus. From the definition of , and . If l_R were inconsistent, l_R |- I=K, and hence l_v |- [I ]=[K], which is a contradiction. Therefore, l_R is consistent.

5. Theorem

l_R is a conservative extension of l_v.

Proof: One direction is given by the correspondence theorem. The other direction follows from the fact that the rules and axioms of l_R contain those of l_v.

From the above theorems, we have established that the addition of the representation rule to the theory is not problematic logically. This also means that the reification property holds for reflective monads. Furthermore, we have established that we can continue to use reasoning mechanisms of the l_v-calculus, because the theory is a conservative extension of the l_v-calculus. Both Ý ß -inverse and ß Ý -inverse hold because reflective monads obey monad laws. The reflection property also holds because of monad laws.

We could try to do this just using regular monads. We could have store the object in a database and return its key, and we could use to unpack this representation. Unfortunately, this does not work because the monad laws do not hold under this implementation. They do, however, hold under reflective monad laws. This can basically be seen by the fact that repeatedly inserting a value in the database will produce different database handles for the value, but each of the handles will be related under » . We can thus use (Ý term) to denote insertion into the database and (ß term) to denote retrieval from the database, and continue to use the reasoning mechanisms of the l_v-calculus.

This paper draws from a large body of literature in constructive logic, l_v-calculus and category theory. It was inspired by Lambek [7] and Scott [8]. Both explore interesting relationships between logic, computation, and category theory, using the Curry-Howard isomorphism as a basis. Constructive theories have been used as theories for program verification and construction for some time now. Martin-Löf's theory of types [9] is one of the most popular of such theories. A good introduction to the Curry-Howard isomorphism is given by Howard [4].

Danvy and Filinski [6] have studied the control operators shift and reset. Plotkin [10] introduces the l_v-calculus. Moggi [3] introduces the notion of monads. Filinski [6] shows how monadic reflection can be achieved with control operators shift and reset. Other work on building calculi for control operators includes that by Felleisen [11] and Sitaram [12]. Talcott [13] presents an intensional theory of function and control abstractions. Wand and Friedman [14] and Danvy and Malmkjaer [15] have presented formal semantics of reflection.

This paper explores connections between computational, logical, and monadic reflection. Using constructive principles, we present a design for reflective facilities in a programming language. One goal of reflection in programming languages is to enhance the power of a programmer to control how a program is implemented. Such a goal loses its appeal if a side-effect of achievGN="J7rmond,l"HELe. An i|- M=N

of a shift and reset. Otsonisacime ntationed to in progbol">lue to usbol">ll_v-.