Mogensen–Scott encoding

History

Scott encoding appears first in a set of unpublished lecture notes by Dana Scott. Torben Mogensen later extended Scott encoding for the encoding of Lambda terms as data.

Discussion

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,

May be thought of as a record or struct where the fields x 1 … x n have been initialized with the values v 1 … v n . These values may then be accessed by applying the term to a function f. This reduces to,

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

Each constructor selects a different function from the function parameters f 1 … 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.

Definition

Let D be a datatype with N constructors, { c i } i = 1 N , such that constructor c i has arity A i .

Scott encoding

The Scott encoding of constructor c i of the data type D is

Mogensen–Scott encoding

Mogensen extends Scott encoding to encode any untyped lambda term as data. This allows a lambda term to be represented as data, within a Lambda calculus meta program. The meta function mse converts a lambda term into the corresponding data representation of the lambda term;

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

For example,

Comparison to the Church encoding

The Scott encoding coincides with the Church encoding for booleans. Church encoding of pairs may be generalized to arbitrary data types by encoding c i of D above as

compare this to the Mogensen Scott encoding,

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).

Type definitions

Church-encoded data and operations on them are typable in system F, but Scott-encoded data and operations are not obviously typable in system F. Universal as well as recursive types appear to be required, and since strong normalization does not hold for recursively typed lambda calculus, termination of programs manipulating Scott-encoded data cannot be established by determining well-typedness of such programs.