"From AHOS to HOAS (or, duality for fun AND profit)"

To be, or to do: that is the question.  One of the important lessons
of linear logic is that connectives come in two flavors: *positive*
connectives (like * and +) are in a sense defined by what they are,
*negative* connectives (like & and -o) are defined by what they do.
Computationally, it turns out this distinction is intimately related
to pattern-matching, and can be formalized through "abstract
higher-order syntax" (POPL '08).  After defining the syntax of
*constructor* patterns for positive types (like strict products and
sums), we can define the syntax of continuations for those types
abstractly, as maps from constructor patterns to expressions.  Dually,
we define *destructor* patterns for negative types (like lazy products
and functions), and then define negative values abstractly, as maps
from destructor patterns to expressions.  From a practical
perspective, AHOS has the advantage of being easily encoded in type
theories based on iterated inductive definitions (such as Coq and
Agda2), allowing us to reuse their pattern coverage-checkers.  We can
also prove a modular type safety theorem.

In recent work with Licata and Harper, we extended this analysis to a
new account of traditional, LF-style higher-order abstract syntax.
The intuition boils down to this: if it is possible to pattern-match
against a value of higher-order type (e.g., as done by Twelf), then
the function space should be positive.  This lead us to introduce an
unusual, positive *representational arrow*, in addition to the
ordinary, negative *computational arrow*.  I will describe some of our
(preliminary) experience with this new approach to representing HOAS,
and with programming with HOAS encodings using AHOS.