Sunday, April 03, 2005

What contexts represent

One of my pet peeves is that people always pay lip service to explaining what contexts are, and they always end up saying the same thing, which means absolutely nothing to people who don't already know what contexts are. They always say, "a context is an expression with a hole." This is basically a useless introduction. If you expect your audience to know what a context is, don't waste their time re-explaining it. If you don't expect them to know, then for God's sake, give them a real explanation.

The notion of a program context can be used to describe a number of ideas. So you could approach it from a number of angles.
  1. Compatible closure - the β-reduction rule isn't useful until you extend it to operate within the context of a whole program.
  2. Observational equivalence - even non-PL programmers are familiar with the idea of "substituting equals for equals" -- Liskov made the substitution principle famous to OO programmers, for example. So you can talk about being able to place two different expressions into the same context and observing the results.
  3. Quasiquotation - a quasiquoted code template constructs a term with holes in it where you can splice in code.
  4. Macros - similarly, the template in a syntax-rules macro, for example, is an expression context with named holes for all the pattern variables.
  5. Evaluation order - this goes along with the idea of compatible closure; since understanding how β-reduction applies within the context of a whole program requires knowing how to find the next expression to reduce, the grammar of evaluation contexts is a specification for the algorithm that finds the redex.
In On the Expressive Power of Programming Languages, Felleisen gives a very general definition of contexts (Def. 3.4), where you can have multiple holes with different names. This demonstrates the connection between contexts and macro-expressibility: a macro template is a context with several distinguished holes.

Although I found the phrase "an expression with a hole" opaque as a first year grad student, I do like the metaphor of a hole. But it's important to motivate it with an application. For PL students learning about semantics, it's probably useful to take the compatible closure angle. Otherwise, observational equivalence is probably the most accessible approach.

1 comment:

Kevin Millikin said...

Nice blog, Dave.

You're right that "expression with a hole" is too informal, and not usually much help (though I guess it's more help than turning it around and saying "an expression is a context with an expression in its hole").

I share your peeve, and have a related one: reduction systems that leave decomposition of a term into a context and potential redex implicit; and have not even a sketch of a unique decomposition lemma.