A bridge between nominal and positional information

Many developers have been faced with the design trade-offs around nominal versus positional access. Nominal access allows one to be noncommittal about shape information of data types. For example, if the only access to data is via a collection of functions called cons, head, rest, ... many, many shapes support valid and useful interpretations. On the other hand, this sort of specification doesn't play well with traditional pattern-matching. That is, pattern-matching -- which is traditionally a form of positional access -- nails down the shape of data.

Recently, i found myself writing Scala code in the following pattern.

trait T[P1,...,Pm] {
def location1 : Type1[P1,...,Pm]
...
def locationN : TypeN[P1,...,Pm]
}

abstract class C[P1,...,Pm](
location1 : Type1[P1,...,Pm],
...,
locationN : TypeN[P1,...,Pm]
) extends T[P1,...,Pm]

case class CC(
location1 : Type1[K1,...,Km],
...,
locationN : TypeN[K1,...,Km]
) extends C[K1,...,Km]

This spells out a clear relationship between nominal and positional access, but it made me wonder if one could have a tighter, clearer relationship. Could you insist, for example, that all nominal types (the types of things that represent names, variables, etc) encoded positional information?

Before showing how simply this can be done, let me provide a little additional motivation through chemistry -- literally. Walter Fontana once remarked to me that one of the real dividing lines between the practice of alchemy and chemistry was the development of the periodic table. Before the periodic table the names of the elements didn't (obviously) encode structural information about the elements and hence nominal information about mixtures of elements had no predictive power over the properties or behavior of said mixture. After the periodic table the names of elements effectively became their positions in the periodic table which reflected structural information about the elements they named. This enabled the practitioner to write equations of the form

Na + Cl => NaCl

2H + O => H₂O

and make a formal theory of their meaning that had predictive properties of the physical world. That was a big step.

In my mind software development suffers because so much rests in the informal or contextual information encoded in nominal access to information -- such as variable names or function names. In point of fact many pieces of code are behaviorally equivalent and not recognized as such because they are encoded via nominal access that obscures this fact. On the other hand, purely positional access can be prohibitively inexpressive. Higher-level languages are clearly more understandable to humans than machine code precisely because of the ability to add contextual information in nominal access -- such as variable names or function names. Therefore, finding better relationships between nominal and positional access -- in particular understanding what the possible set of relations are -- seems like a worthy goal. Is there the equivalent of a transition from software-as-alchemy to software-as-chemistry?

McBride, et al's, recent work on the derivative of regular data types turns out to provide a step in that direction. Let me illustrate the idea via the lambda calculus. We can write down a domain equation for the terms in lambda calculus.

T[N] = N + N x T[N] + T[N] x T[N]

This domain equation can be viewed as a transcription of the standard syntactical presentation of the lambda calculus

T[N] ::= variable N | abstraction N T[N] | application T[N] T[N]

each summand in the top equation corresponds to it's labeled choice in the second. Ironically, reflecting the topic at hand, the first equation is purely structural while the second allows some nominal information to sneak in to help the human understand the contextual relevance of each structural option: the first choice of terms that are just names are variables; the second choice of terms that are functions from names to terms are lambda abstractions; the third choice of pairs of terms are applications.

The corresponding Scala code might look like

// Lambda terms are parametric in a notion of name
trait LambdaTerm[N]

// Variables are a kind of lambda term
case class Variable[N]( n : N )
extends LambdaTerm[N]

// Abstractions are a kind of lambda term
case class Abstraction[N](
formal : N, body : LambdaTerm[N]
) extends LambdaTerm[N]

// Applications are a kind of lambda term
case class Application[N](
fn : LambdaTerm[N], actual : LambdaTerm[N]
) extends LambdaTerm[N]

Note that we have acknowledged the data type is parametric in the notion of name. Whatever type supports the constraints of a nominal theory for the variables in the lambda calculus can be supplied. Now, given this parametric type, T[N], you can calculate the data type of contexts. This data type provides context and path information to allow "plugging in" of term to context. We write this ∂T[N] and refer to McBride's paper as an excellent resource for the reader who wishes to calculate this type for themselves. The key point is that this type represents positional information in type of lambda terms. So, to make a bridge between nominal and positional information all we have to do is to tie the recursive knot.

T[N] = N + N x T[N] + T[N] x T[N] ¹
N = ∂T[N]

Note this step is not the end of the story, but rather the beginning. In particular, there are several desiderata.

• What ties the particular use of a position as a name to something that is coherent or consistent? Specifically, what additional constraints are necessary to ensure that a nominal points to a location in the structure it uses?
• Without specific additional term structure to make use of the positional information available in the nominal entity this is little more than another method of generating tokens. However, the recursive relationship makes nominal structure sensitive to modification of term structure.

In the rho-calculus, a π-calculus-like theory of processes in which the names of channels are quotations of processes, Radestock and i added the de-quotation of a name as a term. This form addresses the second concern and is easily adapted to the setting here. However, the first concern is really quite new. Of the many directions this question leads i'm captivated by the following.

• How do DeBruijn indices relate to the solution to these recursive equations?
• Can the contextual positional information be used to construct a better encoding of ambient calculus into π-calculi?
• Can the correlation of nominal and positional information give a better way to correlate gravitation to metric?

<sub>[1] The reason we consider the data type

T[N] = N + NxT[N] + T[N]xT[N]

where we take a strictly syntactic view of lambda terms as opposed to say

T[N] = N + [N => T[N]] + T[N]xT[N]

is to keep clearly in the regular types differentiable in McBride's original paper.</sub>