Mogensen–Scott encoding

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

Lambda calculus allows data to be stored as parameters to a function that does not yet have all the parameters required for application. For example,

${\displaystyle ((\lambda x_{1}\ldots x_{n}.\lambda c.c\ x_{1}\ldots x_{n})\ v_{1}\ldots v_{n})\ f}$

May be thought of as a record or struct where the fields ${\displaystyle x_{1}\ldots x_{n}}$ have been initialized with the values ${\displaystyle v_{1}\ldots v_{n}}$. These values may then be accessed by applying the term to a function f. This reduces to,

${\displaystyle f\ v_{1}\ldots v_{n}}$

c may represent a constructor for an algebraic data type in functional languages such as Haskell. Now suppose there are N constructors, each with ${\displaystyle A_{i}}$ arguments;

${\displaystyle {\begin{array}{c|c|c}{\text{Constructor}}&{\text{Given arguments}}&{\text{Result}}\\\hline ((\lambda x_{1}\ldots x_{A_{1}}.\lambda c_{1}\ldots c_{N}.c_{1}\ x_{1}\ldots x_{A_{1}})\ v_{1}\ldots v_{A_{1}})&f_{1}\ldots f_{N}&f_{1}\ v_{1}\ldots v_{A_{1}}\\((\lambda x_{1}\ldots x_{A_{2}}.\lambda c_{1}\ldots c_{N}.c_{2}\ x_{1}\ldots x_{A_{2}})\ v_{1}\ldots v_{A_{2}})&f_{1}\ldots f_{N}&f_{2}\ v_{1}\ldots v_{A_{2}}\\\vdots &\vdots &\vdots \\((\lambda x_{1}\ldots x_{A_{N}}.\lambda c_{1}\ldots c_{N}.c_{N}\ x_{1}\ldots x_{A_{N}})\ v_{1}\ldots v_{A_{N}})&f_{1}\ldots f_{N}&f_{N}\ v_{1}\ldots v_{A_{N}}\end{array}}}$

Each constructor selects a different function from the function parameters ${\displaystyle f_{1}\ldots f_{N}}$. This provides branching in the process flow, based on the constructor. Each constructor may have a different arity (number of parameters). If the constructors have no parameters then the set of constructors acts like an enum; a type with a fixed number of values. If the constructors have parameters, recursive data structures may be constructed.

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}}$.

The Scott encoding coincides with the Church encoding for booleans. Church encoding of pairs may be generalized to arbitrary data types by encoding ${\displaystyle c_{i}}$ of D above as

${\displaystyle \lambda x_{1}\ldots x_{A_{i}}.\lambda c_{1}\ldots c_{N}.c_{i}(x_{1}c_{1}\ldots c_{N})\ldots (x_{A_{i}}c_{1}\ldots c_{N})}$

compare this to the Mogensen Scott encoding,

${\displaystyle \lambda x_{1}\ldots x_{A_{i}}.\lambda c_{1}\ldots c_{N}.c_{i}x_{1}\ldots 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 (no parameters).

Concerning the practicality of using either the Church or Scott encoding for programming, there is a symmetric trade-off:[5] 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.

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.[6]

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

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

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

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

Combining these twos fact yields the System F type of the Scott encoding:

${\displaystyle \forall X.(((\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 \forall X.X\to (X\to X)\to X}$

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

• Church encoding
• System F
• Lambda cube

• Stump, A. (2009). Directly reflective meta-programming. Higher-Order and Symbolic Computation, 22, 115-144.
• Mogensen, T.Æ. (1992). Efficient Self-Interpretations in lambda Calculus. J. Funct. Program., 2, 345-363.