Mogensen–Scott encoding

FEB 10, 15:50 | Blue Room

Mogensen–Scott encoding allows representation of algebraic data types in untyped lambda calculus. Similar to Church encoding, it can be used to regard lambda functions as data and therefore defines an embedded metaprogramming “language”.

This talk explores encoding of several familiar data types and demonstrates the flow control — type duality seen in the consumer functions defined for these types. This formalises the theoretical basis for such functional programming language features as pattern matching, generalised folding and automatic derivation of typeclass instances.