Lambda calculus encodings of algebraic data types

From apm
Jump to navigation Jump to search

Disclaimer: Parts of this page have been generated with supervised LLM-AI assistance.
Encodings not yet checked for correctness. Please take them with a grain of salt.

Overview

Algebraic Data Types (ADTs) can be encoded in untyped lambda calculus in several different ways.
This article documents the main approaches and their trade-offs.

Core Encodings

ADTs are built from two fundamental building blocks:

  • Product types (tuples/records)
  • Sum types (variants/enums)

Each can be encoded in several ways:

Church Encoding

The classical direct approach:

Products: 

pair = λx.λy.λf.(f x y)
fst = λp.(p λx.λy.x)
snd = λp.(p λx.λy.y)

Sums: 

inl = λx.λl.λr.(l x)
inr = λx.λl.λr.(r x)
case = λs.λl.λr.(s l r)

Properties:

  • Eager evaluation
  • Direct construction and elimination
  • Most straightforward implementation

Lazy Encoding

Delays evaluation through thunks:

Products: 

pair = λx.λy.λf.(f λk.x λk.y)
fst = λp.(p λx.λy.(x λw.w))
snd = λp.(p λx.λy.(y λw.w))

Sums: 

inl = λx.λl.λr.(l λk.x)
inr = λx.λl.λr.(r λk.x)
case = λs.λl.λr.(s (λx.(x λw.w) l) (λx.(x λw.w) r))

Properties:

  • Components only evaluated when needed
  • Useful for infinite structures
  • Higher memory usage due to closure allocation

Strict Encoding

Forces evaluation through wrapper functions:

Products: 

pair = λx.λy.λf.(f (λk.k x) (λk.k y))
fst = λp.(p λx.λy.(x λw.w))
snd = λp.(p λx.λy.(y λw.w))

Sums: 

inl = λx.λl.λr.(l x)
inr = λx.λl.λr.(r x)
case = λs.λl.λr.(s (λx.l x) (λx.r x))

Properties:

  • Guarantees evaluation order
  • Useful for maintaining invariants
  • Additional function call overhead

Elimination-Focused (Continuation) Encoding

Represents data through its elimination behavior:

Products: 

pair = λx.λy.λk.(k (λf.f x y))
fst = λp.(p λq.(q λx.λy.x))
snd = λp.(p λq.(q λx.λy.y))

Sums: 

inl = λx.λk.(k (λl.λr.(l x)))
inr = λx.λk.(k (λl.λr.(r x)))
case = λs.λl.λr.(s λc.(c l r))

Properties:

  • Centered on pattern matching
  • Natural fit for programming language implementation because:
    • Pattern matching is fundamentally about elimination
    • Aligns with how most programming languages handle data inspection
    • Compiler optimizations often work on elimination forms
  • More complex implementation

Construction-Focused Encoding

Represents data through its construction behavior:

Products: 

pair = λx.λy.(λk.k (λc.c x y))
fst = λp.(p (λq.q λx.λy.x))
snd = λp.(p (λq.q λx.λy.y))

Sums: 

inl = λx.(λk.k (λl.λr.l x))
inr = λx.(λk.k (λl.λr.r x))
case = λs.λl.λr.(s (λc.c l r))

Properties:

  • Dual to elimination-focused encoding
  • Emphasizes data construction paths
  • Less common in practice

Composition Patterns

Nesting Structure

ADTs typically use:

  • Disjunctive Normal Form (DNF): Sum of Products
  • Conjunctive Normal Form (CNF): Product of Sums

DNF is preferred in practice because:

  • Maps naturally to constructors with fields
  • More efficient pattern matching
  • Better cache locality for related fields
  • Matches programmer intuition

Example in DNF: 

data Tree = Leaf Int 
          | Node Tree Int Tree

Encoding Consistency

Best practices for combining encodings:

  • Use the same encoding style throughout (Church with Church, etc.)
  • Stick to one nesting structure (typically DNF)
  • Consider using elimination-focused style for programming language implementations

Implementation Considerations

Performance Characteristics

  • Church encoding: Simple but eager
  • Lazy encoding: Memory overhead but supports infinite structures
  • Strict encoding: Predictable evaluation but extra calls
  • Elimination-focused: Complex but good for pattern matching
  • Construction-focused: Similar complexity to elimination-focused

Language Implementation

Most programming languages use:

  • DNF structure
  • Elimination-focused approach
  • Optimized representations at lower levels

Type System Implications

  • All encodings work in untyped lambda calculus
  • Simply-typed lambda calculus cannot encode proper product types of different types
  • Sum types are encodable in simply-typed lambda calculus

Advanced Topics

Related to the afire mentioned limit for product types.
There may interesting connections of these encodings to things like GADTs and dependent types.
The relationship between continuation-based encodings and categorical semantics (particularly through the continuation monad)
suggests deeper connections to Cartesian closed categories and type theory.

Notice the duality:
– Corecursive construction of ADTs via type constructors
– Recursive deconstructions via pattern matching in case … of … statements
The case … of … statements are where branching happens which is what makes control flow rich and interesting.

Related

External links

Retrieved from "https://apm.bplaced.net/w/index.php?title=Lambda_calculus_encodings_of_algebraic_data_types&oldid=17201"