Mogensen–Scott encoding

History

Scott encoding appears first in a set of unpublished lecture notes by Dana Scott whose first citation occurs in the book Combinatorial Logic, Volume II. Michel Parigot gave a logical interpretation of and strongly normalizing recursor for Scott-encoded numerals, referring to them as the "Stack type" representation of numbers. Torben Mogensen later extended Scott encoding for the encoding of Lambda terms as data.

Discussion

Partially applying a lambda term results in data received as arguments corresponding to its parameters to be "stored" in the resulting term. A term

${\displaystyle \begin{array}{cc}R& \equiv (\lambda x_1\dots x_n.\lambda c.c{x}_1\dots x_n)v_1\dots v_n\\ & \equiv \lambda c.c{v}_1\dots v_n\end{array}}$

can be regarded as a lambda calculus representation of an nary tuple ${\displaystyle ⟨v_1\dots v_n⟩}$. Thus, the term

${\displaystyle \begin{array}{c}(\lambda x_1\dots x_n.\lambda c.c{x}_1\dots x_n)\end{array}}$

can be seen as an nary tuple constructor. In fact, for ${\displaystyle n=2}$ it coincides with the Church encoding for pairs, or 2-tuples.

Tuples are natural representation of products. In the algebraic data types discipline of seeing types as sums of products, each alternative is a product, and can be represented as a tuple of corresponding arity.

Such data are processed, or "handled", by applying them to functions of matching arity, that will thus receive the original individual constituents of a tuple as arguments:

${\displaystyle \begin{array}{c}(\lambda c.c{v}_1\dots v_n)f\\ \equiv f{v}_1\dots v_n\end{array}}$

Now suppose there are N alternatives in the sum, N product constructors, each with ${\displaystyle a_{i=\mathrm{1..}N}}$ arguments;

${\displaystyle \begin{array}{ccc}\text{Alternative}& \text{Given arguments}& \text{Result}\\ ((\lambda x_1\dots x_{a_1}.\lambda c_1\dots c_N.c_1{x}_1\dots x_{a_1})v_1\dots v_{a_1})& f_1\dots f_N& f_1{v}_1\dots v_{a_1}\\ ((\lambda x_1\dots x_{a_2}.\lambda c_1\dots c_N.c_2{x}_1\dots x_{a_2})v_1\dots v_{a_2})& f_1\dots f_N& f_2{v}_1\dots v_{a_2}\\ ⋮& ⋮& ⋮\\ ((\lambda x_1\dots x_{a_N}.\lambda c_1\dots c_N.c_N{x}_1\dots x_{a_N})v_1\dots v_{a_N})& f_1\dots f_N& f_N{v}_1\dots v_{a_N}\end{array}}$

Each alternative belonging to the same type, its encoding expects the same number ${\displaystyle N}$ of handler functions ${\displaystyle c_1\dots c_N}$. Thus all these alternatives are used in the same way, by applying to ${\displaystyle N}$ handler functions ${\displaystyle f_1\dots f_N}$, so all of them together constitute the sum data type's representation as a set of lambda terms, shown in the table above.

Each alternative selects a different handling function from the function parameters ${\displaystyle f_1\dots f_N}$ it is given. This provides branching in the process flow, based on the constructor, akin to type-based pattern matching. Each constructor may have a different arity (number of parameters) but the resulting encodings all expect the same number ${\displaystyle N}$ of observer / handler functions. If a constructor's arity ${\displaystyle a_i=0}$, the corresponding handler receives no arguments. For example a "maybe pair or nothing", in other words, an "optional pair," can be represented by the set of two lambda terms,

${\displaystyle \begin{array}{cc}nil\equiv & (\lambda n.\lambda c.n)\\ cons\equiv \lambda ad.& (\lambda n.\lambda c.cad)\end{array}}$

corresponding to the two possible alternatives. The question of whether either of the ${\displaystyle cons}$ pair constituents is also a pair or not is disregarded here. What's addressed by this encoding is just that there are two constituents in a non-empty pair, and no constituents in the empty pair (also known as nil). This type consists of two alternatives: one contains no data, the other contains two.

If all the constructors have no parameters then the set of such constructors acts like an enum, a sum type of (tagged) 0-tuples, or a type with a fixed number of values. If the constructors have parameters, whether they correspond recursively to the same data type's alternatives is ignored. Recursion can be explicitly performed as usual in lambda calculus, through the use of fixed points, or self-reference via self-application.

Definition

Let D be a datatype with N constructors, ${\displaystyle \{c_i{\}}_{i=1}^N}$, such that constructor ${\displaystyle c_i}$ has arity ${\displaystyle a_i}$.

Scott encoding

The Scott encoding of constructor ${\displaystyle c_i}$ of the data type D is

${\displaystyle \lambda x_1\dots x_{a_i}.\lambda c_1\dots c_N.c_i{x}_1\dots x_{a_i}}$

Mogensen–Scott encoding

Mogensen extends Scott encoding to encode the lambda term data type. This allows a lambda term to be represented as data, within lambda calculus itself. The meta function mse converts a lambda term into the corresponding Scott representation of it as a datum. A lambda term data type consists of three alternatives – variable, application, and abstraction:

${\displaystyle \begin{array}{cc}\mathrm{mse}[x]& =\lambda abc.ax\\ \mathrm{mse}[MN]& =\lambda abc.b\mathrm{mse}[M]\mathrm{mse}[N]\\ \mathrm{mse}[\lambda x.M]& =\lambda abc.c(\lambda x.\mathrm{mse}[M])\end{array}}$

The "lambda term" is represented as a tagged union with three cases:

• Case 1 (handler a) - a variable (arity 1, not recursive)
• Case 2 (handler b) - function application (arity 2, recursive in both arguments),
• Case 3 (handler c) - lambda-abstraction (arity 1, recursive).

For example,

${\displaystyle \begin{array}{l}\mathrm{mse}[\lambda x.f(xx)]\\ \equiv \lambda abc.c(\lambda x.\mathrm{mse}[f(xx)])\\ \equiv \lambda abc.c(\lambda x.\lambda abc.b\mathrm{mse}[f]\mathrm{mse}[xx])\\ \equiv \lambda abc.c(\lambda x.\lambda abc.b(\lambda abc.af)(\lambda abc.b\mathrm{mse}[x]\mathrm{mse}[x]))\\ \equiv \lambda abc.c(\lambda x.\lambda abc.b(\lambda abc.af)(\lambda abc.b(\lambda abc.ax)(\lambda abc.ax)))\end{array}}$

Comparison to the Church encoding

Type recursion is ignored in Scott but is directly addressed in Church encoding, which is the type's folding on its recursive component(s). Thus, for any non-recursive type Scott encoding coincides with its Church encoding, up to the arguments order. But recursive types differ, since Scott encodes only the surface syntax of the data type definition.

In Scott any constituent can be of any type, whether the same as the type itself, or not

${\displaystyle \begin{array}{cc}nil\equiv & (\lambda n.\lambda c.n)\\ cons\equiv \lambda ad.& (\lambda n.\lambda c.cad)\end{array}}$

Church cons-pairs with the second field assumed to also be a cons-pair, treat it differently and perform a recursive processing (thus, folding) on it:

${\displaystyle \begin{array}{cc}nil\equiv & (\lambda c.\lambda n.n)\\ cons\equiv \lambda ad.& (\lambda c.\lambda n.ca(dcn))\end{array}}$

Church encoding of pairs may be generalized to arbitrary data types by encoding ${\displaystyle c_i}$ of D above as

${\displaystyle \lambda x_1\dots x_{a_i}.\lambda c_1\dots c_N.c_i{x}_1\dots (x_{j_i}{c}_1\dots c_N)\dots x_{a_i}}$

with ${\displaystyle x_{j_i}}$ applied to all the handlers ${\displaystyle c_1\dots c_N}$ like that for all the ${\displaystyle j_i}$s such that each ${\displaystyle x_{j_i}}$ belongs to the same main type ${\displaystyle D}$.

Compare this with the Scott encoding,

${\displaystyle \lambda x_1\dots x_{a_i}.\lambda c_1\dots c_N.c_i{x}_1\dots x_{a_i}}$

With this generalization, the Scott and Church encodings coincide on all enumerated datatypes (such as the Boolean datatype) because each constructor is a constant (has no parameters).

Thus Scott encodings have raw access to every component of the data type, e.g. predecessor for numerals and list tail for lists. But Church encodings have access to the results of processing for the recursive components, and thus must rebuild any recursive component, if so desired, by a clever folding which usually has a cost with regards to efficiency.

Concerning the practicality of using either the Church or Scott encoding for programming, there is a symmetric trade-off: Church-encoded numerals support a constant-time addition operation and have no better than a linear-time predecessor operation; Scott-encoded numerals support a constant-time predecessor operation and have no better than a linear-time addition operation.

Type definitions

Church-encoded data and operations on them are typable in system F, as are Scott-encoded data and operations. However, the encoding is significantly more complicated.

The type of the Scott encoding of the natural numbers is the positive recursive type:

${\displaystyle \mu X.\mathrm{\forall }R.R\to (X\to R)\to R}$

Full recursive types are not part of System F, but positive recursive types are expressible in System F via the encoding:

${\displaystyle \mu X.G[X]=\mathrm{\forall }X.((G[X]\to X)\to X)}$

Combining these two facts yields the System F type of the Scott encoding:

${\displaystyle \mathrm{\forall }X.(((\mathrm{\forall }R.R\to (X\to R)\to R)\to X)\to X)}$

This can be contrasted with the type of the Church encoding:

${\displaystyle \mathrm{\forall }X.X\to (X\to X)\to X}$

The Church encoding is a second-order type, but the Scott encoding is fourth-order!