Mogensen–Scott encoding
In computer science, Scott encoding is a way to represent (recursive) data types in the lambda calculus. Church encoding performs a similar function. The data and operators form a mathematical structure which is embedded in the lambda calculus.
Whereas Church encoding starts with representations of the basic data types, and builds up from it, Scott encoding starts from the simplest method to compose algebraic data types.
Mogensen–Scott encoding extends and slightly modifies Scott encoding by applying the encoding to Metaprogramming. This encoding allows the representation of lambda calculus terms, as data, to be operated on by a meta program.
History
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]
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 have been initialized with the values . 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 arguments;
Each constructor selects a different function from the function parameters . 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, , such that constructor has arity .
Scott encoding
The Scott encoding of constructor 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:
- Constructor a - a variable (arity 1, not recursive)
- Constructor b - function application (arity 2, recursive in both arguments),
- Constructor c - lambda-abstraction (arity 1, recursive).
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 of D above as[citation needed]
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).
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.
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,.[6] As strong normalization does not hold for unrestricted recursive types ,[7] establishing termination of programs manipulating Scott-encoded data by determining well-typedness requires the type system provide additional restrictions on the formation of recursively typed terms.
See also
Notes
- ^ Scott, Dana, A system of functional abstraction (1968). Lectures delivered at University of California, Berkeley, (1962)
- ^ Curry, Haskell (1972). Combinatorial Logic, Volume II. North-Holland Publishing Company. ISBN 0-7204-2208-6.
- ^ Parigot, Michel (1988). "Programming with proofs: a second order type theory". European Symposium on Programming. Lecture Notes in Computer Science. 300: 145–159. doi:10.1007/3-540-19027-9_10. ISBN 978-3-540-19027-1.
- ^ Mogensen, Torben (1994). "Efficient Self-Interpretation in Lambda Calculus". Journal of Functional Programming. 2 (3): 345–364. doi:10.1017/S0956796800000423.
- ^ Parigot, Michel (1990). "On the representation of data in lambda calculus". International Workshop on Computer Science Logic. Lecture Notes in Computer Science. 440: 209–321. doi:10.1007/3-540-52753-2_47. ISBN 978-3-540-52753-4.
- ^ See the note "Types for the Scott numerals" by Martín Abadi, Luca Cardelli and Gordon Plotkin (February 18, 1993).
- ^ Mendler, Nax (1987). "Recursive types and type constraints in second-order lambda calculus". Symposium on Logic in Computer Science (2): 30–36.
References
- 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.