Mogensen-Scott encoding

https://en.wikipedia.org/wiki/Mogensen-Scott_encoding

Scott encoding is a way to represent recursive data types in the LC. In an encoding, the data and operators form a mathematical structure which is embedded in the LC.

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

Mogensen-Scott encoding extends and slightly modifies Scott encoding by applying the encoding to meta-programming. This encoding allows the representation of LC terms, as data, to be operated on by a meta program.