Encoding schemes

The Church encoding
The Scott encoding
The Parigot encoding
The Bohm-Berarducci
The Mogensen-Scott encoding
The Barendregt encoding
The Stump's Mendler encoding
The Mendler encoding

An encoding scheme is a set of lambda terms that represent particular data types and data structures.

The Church encoding is the most well-known encoding scheme, given by Alonzo Church himself, which manages to represent many data structures including Boolean values (The Church Booleans), natural numbers (The Church numerals), negative, rational and real numbers, ordered pair (The Church pair), list, tree.

The Scott encoding is a scheme to represent (recursive) data types, which was given by Dana Scott. Whereas Church encoding starts with representations of the basic data types and builds up from there, Scott encoding starts from the simplest method to compose algebraic data types.

The Parigot encoding solves the Church encoding's problem of inefficient predecessor. It can be typed using positive-recursive types, which preserve normalization of the type theory.

The Mogensen-Scott encoding extends and slightly modifies the Scott encoding by applying it to meta-programming, which enables representing lambda terms as data, to be operated on by a meta program.

The Stump's Mendler encoding: Mendler's technique of abstracting out problematic types with new type variables, and how this can yield a lambda encoding where the programmer is in charge of when to make recursive calls (rather than in the Church encoding, where the data represents a programmer's combining functions with results of all possible recursive calls on immediate subdata). (Aaron Stump?)

References

Alternative to the Church, Scott and Parigot encodings of data in LC

PreviousAlternative encodings NextEncoding schemes

Last updated 3 years ago

Was this helpful?