Decoding the Lexicon of Functions and Sets

Functional programming is not just a style of writing software; it is an application of mathematical logic, specifically set theory, type algebra, abstract algebra, and category theory. Concepts across functional languages (like Haskell, Elm, Nix, or functional Rust) map directly to formal mathematical definitions. This lexicon decodes the mathematical foundations underpinning functional programming: from set operations and function mappings to algebraic structures, category theory, and functional architectural patterns, revealing why functional code is so predictable, testable, and robust.

1. Set Theory & Type Algebra

Set theory forms the foundation of all mathematical structures. In functional programming, types and data models can be understood as sets of possible values.

Set

A set is a well-defined collection of distinct objects, known as elements. For example, the set of all integers (ℤ), or the set of boolean values {true, false}.

# In Nix, a set can be represented as a list of unique elements
colors = [ "red" "green" "blue" ];

# Or represented as an attribute set keys (for O(1) membership checks)
colorSet = {
  red = true;
  green = true;
  blue = true;
};

Set Membership (Element of)

The membership relation symbol is ∈ (and its negation is ∉).

• x ∈ A means “x is an element of set A” (or “x belongs to A”).
• x ∉ A means “x is not an element of set A”.

In functional programming, this corresponds directly to checking if a value exists within a collection or satisfies a type/set validator.

# In Nix, we can check set membership using builtins.elem (for lists)
isMember = element: set: builtins.elem element set;

# For attribute sets (objects), we use the `?` operator to check key membership
isKeyMember = key: set: set ? ${key};

Universal Set

The symbol ξ (or ℰ, representing the Greek letter xi or a stylized E) denotes the Universal Set (sometimes written as U). It represents the set of all possible elements under consideration for a given context or problem.

In functional programming, the Universal Set corresponds to the universe of all possible types or values in the system, or conceptually the “top type” (such as any in TypeScript or the set of all possible Nix values).

# Conceptually, the universal set of all valid values in a dynamically typed language:
isAnyValue = x: true;

Empty Set

The empty set, denoted by ∅ or {}, is the unique set containing no elements.

In functional programming, the empty set corresponds to the Bottom Type (such as never in TypeScript or Void in Haskell). It is a type that has no values and therefore can never be instantiated.

# In Nix, the empty set can be represented as an empty list
emptySet = [ ];

Subset

A set A is a subset of a set B (written A ⊆ B) if every element of A is also an element of B. If A ⊆ B and A ≠ B, then A is a proper subset (written A ⊂ B).

In functional systems, this maps to subtyping or type narrowing. If type Dog is a subset of type Animal, a function accepting an Animal will accept a Dog.

graph TD
    subgraph B ["Set B: Animal"]
        b1["Cat"]
        subgraph A ["Set A: Dog (Subset)"]
            a1["Terrier"]
            a2["Spaniel"]
        end
    end

# In Nix, checking if 'sub' is a subset of 'set'
isSubset = sub: set: builtins.all (x: builtins.elem x set) sub;

Union

The union of two sets A and B (written A ∪ B) is the set of all elements that are members of A, or B, or both.

In functional programming, this corresponds directly to Sum Types (tagged unions or union types) like Result = Success | Error. It models branching possibilities.

graph LR
    subgraph Union ["Union: A ∪ B"]
        subgraph A ["Set A"]
            a1["1"]
            a2["2"]
        end
        subgraph B ["Set B"]
            b1["3"]
            b2["4"]
        end
    end

let
  # Helper to remove duplicates from a list
  unique = list:
    let
      step = acc: x: if builtins.elem x acc then acc else acc ++ [ x ];
    in
    builtins.foldl' step [ ] list;
in
# In Nix, union of two sets
union = a: b: unique (a ++ b);

Intersection

The intersection of two sets A and B (written A ∩ B) is the set of all elements that are members of both A and B.

In functional languages, this corresponds to Intersection Types (or merging schemas). In Nix or TypeScript, this often looks like merging or intersecting two record types or attribute sets.

graph LR
    subgraph SetA ["Set A"]
        a1["Red"]
    end
    subgraph Intersect ["A ∩ B (Shared)"]
        ab1["Green"]
    end
    subgraph SetB ["Set B"]
        b1["Blue"]
    end

# In Nix, intersection of two sets
intersection = a: b: builtins.filter (x: builtins.elem x b) a;

Set Difference

The set difference of A and B (written A \ B or A − B) is the set of all elements that are in A but not in B.

In functional languages, this maps to key removal or type exclusion/omission operations (e.g., Omit in TypeScript, or builtins.removeAttrs in Nix to remove specific keys from an attribute set).

graph LR
    subgraph A_without_B ["A \\ B (Retained in A)"]
        a1["1"]
        a2["2"]
    end
    subgraph B_elements ["Removed Elements in B"]
        b1["3"]
    end

# In Nix, set difference
difference = a: b: builtins.filter (x: !builtins.elem x b) a;

Complement (Absolute Complement)

The complement of a set A (written A^′ or A^c) with respect to a universal set ξ is the set of all elements in the universe that do not belong to A, defined as A^c = ξ \ A = {x ∈ ξ ∣ x ∉ A}.

In functional programming, this corresponds to negating a predicate or selecting the inverse set of options/variants.

graph TD
    subgraph Universe ["Universal Set: ξ"]
        subgraph Complement_Ac ["Aᶜ: Complement"]
            c1["x ∉ A"]
            c2["y ∉ A"]
        end
        subgraph Set_A ["Set A"]
            a1["x ∈ A"]
        end
    end

# In Nix, complement of a set relative to a given universe:
complement = universe: set: builtins.filter (x: !builtins.elem x set) universe;

Disjoint Sets

Two sets A and B are disjoint (or mutually exclusive) if their intersection is the empty set: A ∩ B = ∅.

In functional architecture, disjoint sets represent mutually exclusive states (such as disjoint variants in an algebraic data type where a value cannot be both Loading and Success simultaneously).

graph LR
    subgraph SetA ["Set A: Loading"]
        a1["State 1"]
    end
    subgraph SetB ["Set B: Success"]
        b1["State 2"]
    end
    style SetA fill:#ffffff,stroke:#000000
    style SetB fill:#ffffff,stroke:#000000,stroke-dasharray: 5 5

# Check if two sets are disjoint
areDisjoint = a: b: (builtins.filter (x: builtins.elem x b) a) == [ ];

De Morgan’s Laws

In set theory and propositional logic, De Morgan’s Laws describe the duality between union and intersection under complementation:

1. (A ∪ B)^c = A^c ∩ B^c (“The complement of a union is the intersection of the complements”)
2. (A ∩ B)^c = A^c ∪ B^c (“The complement of an intersection is the union of the complements”)

In functional programming, De Morgan’s Laws are essential for refactoring, simplifying boolean conditionals, and inverting complex filter predicates: !(p || q) == (!p && !q).

let
  p = true;
  q = false;
  # !(p || q) == (!p && !q)
  deMorgan1 = !(p || q) == (!p && !q); # true
  # !(p && q) == (!p || !q)
  deMorgan2 = !(p && q) == (!p || !q); # true
in
deMorgan1 && deMorgan2 # evaluates to true

Equivalence Relation & Partitions

An equivalence relation ∼ on a set S is a binary relation that is:

1. Reflexive: a ∼ a for all a ∈ S.
2. Symmetric: If a ∼ b, then b ∼ a.
3. Transitive: If a ∼ b and b ∼ c, then a ∼ c.

Every equivalence relation partitions the set S into mutually disjoint equivalence classes (subsets of elements that are equivalent to each other). In functional programming, this corresponds to structural equality, custom hashing, and grouping operations like groupBy.

let
  numbers = [ 1 2 3 4 5 6 7 8 9 ];
  # Equivalence relation: having the same parity (both even or both odd)
  # Partitions the list into equivalence classes:
  evenOddPartition = {
    evens = builtins.filter (x: (x / 2) * 2 == x) numbers; # [ 2 4 6 8 ]
    odds = builtins.filter (x: (x / 2) * 2 != x) numbers;  # [ 1 3 5 7 9 ]
  };
in
evenOddPartition

Cartesian Product

The Cartesian product of two sets A and B (written A × B) is the set of all ordered pairs (a, b) such that a ∈ A and b ∈ B.

In functional programming, this corresponds to Product Types (such as tuples, records, or attribute sets). A Nix attribute set { a = 1; b = true; } is a value inhabiting the Cartesian product of Int × Bool.

graph LR
    subgraph Inputs ["Sets A and B"]
        A["Set A: { x, y }"]
        B["Set B: { 1, 2 }"]
    end
    subgraph Product ["A × B (Cartesian Product)"]
        p1["(x, 1)"]
        p2["(x, 2)"]
        p3["(y, 1)"]
        p4["(y, 2)"]
    end
    A --> Product
    B --> Product

# In Nix, Cartesian product represented as a list of attribute sets/pairs
cartesianProduct = a: b:
  builtins.concatMap (x: builtins.map (y: { fst = x; snd = y; }) b) a;

Relation

A relation R between set A and set B is a subset of their Cartesian product: R ⊆ A × B. If an ordered pair (a, b) ∈ R, we say that a is related to b (written a R b).

When A = B, R ⊆ A × A is called a binary relation on A. Relations generalize functions: while a function must assign exactly one output to each input, a general relation can associate an input with zero, one, or multiple outputs.

# In Nix, a binary relation modeled as a list of pairs (e.g. "is child of")
parentChildRelation = [
  { fst = "Alice"; snd = "Bob"; }
  { fst = "Alice"; snd = "Charlie"; }
];

Predicate

A predicate is a function that takes an input and returns a boolean value (true or false), representing a property or condition: P : A → {true, false}

Every predicate P uniquely defines a subset of A (namely, the elements for which P(x) = true). In functional programming, predicates are used everywhere to validate types, filter lists, and branch control flow.

# A predicate testing if a number is positive:
isPositive = x: x > 0;

Cardinality

The cardinality of a set A (written |A|) is a measure of the “number of elements” in the set. For a finite set, it is simply the number of elements it contains.

In functional systems, cardinality helps us understand the number of possible states a type can represent. For example, the cardinality of Bool is 2. The cardinality of a product type is the product of its fields’ cardinalities, whereas the cardinality of a sum type is the sum of its fields’ cardinalities.

# In Nix, cardinality of a set represented as a list
cardinality = set: builtins.length set;

Power Set

The power set of a set A (written 𝒫(A) or 2^A) is the set of all subsets of A, including the empty set and A itself.

graph TD
    S["{ 1, 2 }"]
    S1["{ 1 }"]
    S2["{ 2 }"]
    Empty["∅ (Empty Set)"]

    Empty --> S1
    Empty --> S2
    S1 --> S
    S2 --> S

let
  # Power set computation using recursion
  powerSet = list:
    if list == [ ]
    then [ [ ] ]
    else
      let
        x = builtins.head list;
        xs = builtins.tail list;
        ps_xs = powerSet xs;
      in
      ps_xs ++ builtins.map (subset: [ x ] ++ subset) ps_xs;
in
# powerSet [ 1 2 ] -> [ [ ] [ 2 ] [ 1 ] [ 1 2 ] ]
powerSet

Set-Builder Notation

Set-builder notation is a mathematical notation for describing a set by stating the properties that its members must satisfy. It is written in the form {x ∈ A ∣ P(x)}, which reads: “the set of all x in A such that P(x) is true,” where P(x) is a predicate (a boolean-valued formula).

In functional programming, this corresponds directly to filtering a collection or list comprehensions based on a predicate function.

# Conceptually represents: { x ∈ integers | x > 0 }
isPositive = x: x > 0;
positives = builtins.filter isPositive [ (-1) 0 1 2 ]; # [ 1 2 ]

Type

In functional programming, a type can be understood as a set of all possible values that an expression of that type can evaluate to. For example, the type bool is the finite set of 2 elements {true, false}, integer is the set of all integers ℤ, and string is the infinite set of all valid character sequences.

# In Nix, we can define validator functions (predicates) representing a type.
# A type is the set of inputs that evaluate to true under the validator:
isBool = x: x == true || x == false;

Algebraic Data Types (ADTs) & Polynomial Types

An Algebraic Data Type (ADT) is a composite type formed by combining other types using algebraic operations:

• Sum Types (+): Values representing an alternative choice between types (disjoint union, e.g. Option A = 1 + A, or Either A B = A + B).
• Product Types (×): Values combining multiple fields simultaneously (tuples, records, e.g. Pair A B = A × B).

Recursive data structures can be expressed elegantly as polynomial equations. For example, the type of a linked list L(A) over an element type A satisfies: L(A) ≅ 1 + A × L(A) where 1 is the unit/terminal type (the empty list nil), and A × L(A) is the product of a head element and the tail list (cons).

graph TD
    subgraph ADT ["Algebraic Data Types"]
        direction TB
        subgraph SumType ["Sum Type: A + B (OR / Choice)"]
            s1["Variant Left: A"]
            s2["Variant Right: B"]
        end
        subgraph ProdType ["Product Type: A × B (AND / Conjunction)"]
            p1["Field 1: A AND Field 2: B"]
        end
    end

# Polynomial construction of a linked list: 1 + (A * List A)
nil = { type = "nil"; };
cons = head: tail: { type = "cons"; inherit head tail; };

# List: [ 1 2 ] -> cons 1 (cons 2 nil)
myList = cons 1 (cons 2 nil);

Referential Transparency

An expression is referentially transparent if it can be replaced with its evaluated value without changing the behavior or correctness of the program.

Mathematically, this means equations can be manipulated using standard algebraic substitution (the substitution model of computation). Referential transparency is the defining property that allows compiler optimizations (like common subexpression elimination and memoization) and formal proofs of program correctness.

let
  # Because add is pure and referentially transparent:
  add = a: b: a + b;
  # We can freely replace (add 2 3) with 5 anywhere in our code:
  result = (add 2 3) * (add 2 3); # identically equivalent to: 5 * 5
in
result # 25

2. Functions & Mappings

Functions describe computational transformations that map inputs from a source set (domain) to an allowable output set (codomain).

Function

In set theory, a function f from set A to set B (written f : A → B) is a relation that associates each element in the domain A with exactly one element in the codomain B. In functional programming, a function is a computational rule that maps inputs of type A to outputs of type B.

increment = x: x + 1;

graph LR
    subgraph Domain ["Set A: Domain"]
        a1["a1"]
        a2["a2"]
        a3["a3"]
    end

    subgraph Codomain ["Set B: Codomain"]
        subgraph Range ["Range / Image"]
            b1["b1"]
            b2["b2"]
            b3["b3"]
        end
        b4["b4"]
    end

    a1 -->|"f"| b1
    a2 -->|"f"| b2
    a3 -->|"f"| b3

    style Range fill:#ffffff,stroke:#000000,stroke-dasharray: 5 5

Domain

The domain is the set of all possible inputs for which a function is defined. For a function f : A → B, the domain is the set/type A.

# Domain: any negative or non-negative number (integer or float)
absoluteValue = x: if x < 0 then -x else x;

Codomain

The codomain is the set of all possible outputs that a function is allowed to produce. For a function f : A → B, the codomain is the set/type B.

# Codomain is conceptually the set of all non-negative integers
squareMagnitude = x: x * x;

Range (Image)

The range (or image) of a function is the subset of the codomain containing the values actually produced by the function. It is the set {f(x) ∈ B ∣ x ∈ A}. For example, if a function square : Int → Int maps integers to their squares, the domain and codomain are the set of all integers (Int), but the range is only the subset of non-negative squares ({ 0, 1, 4, 9, 16, ... }).

# Domain: Integers, Codomain: Integers
# Range: { 0, 1, 4, 9, 16, ... } (subset of integers)
square = x: x * x;

Preimage (Fiber)

Under a function f : A → B, the preimage (or inverse image) of a subset Y ⊆ B is the set of all elements in A that map to Y, denoted f⁻¹(Y) = {x ∈ A ∣ f(x) ∈ Y}. If Y contains a single element {y}, the preimage f⁻¹({y}) is called the fiber of y.

In functional programming, computing a preimage or fiber corresponds to filtering a domain collection based on its mapped output.

# Find the fiber of 4 (all inputs mapping to 4 under f(x) = x * x)
# Domain: { -2, -1, 0, 1, 2 }, Codomain: { 0, 1, 4 }
domain = [ (-2) (-1) 0 1 2 ];
f = x: x * x;

fiber = target: builtins.filter (x: f x == target) domain; # [ -2 2 ]

Partial vs. Total Functions

A function can be categorized based on how completely it covers its domain:

• A total function is a function f : A → B that is defined for every element in its domain A. In purely functional programming, total functions are highly preferred because they are safe, predictable, and cannot crash at runtime.
• A partial function is a function f : A → B that is not defined for some inputs in its domain A.

In functional programming, partial functions (like division by zero, or retrieving the head of an empty list) can lead to runtime crashes or exceptions. To make partial functions total, we typically wrap their codomain in a container type like Option or Maybe.

# A partial function: division by zero crashes the program
# partialDivide : Int -> Int -> Int
partialDivide = b: a: a / b;

# A total version of the function wrapping the output in an Option
# totalDivide : Int -> Int -> Option Int
totalDivide = b: a:
  if b == 0
  then { type = "none"; }
  else { type = "some"; value = a / b; };

Injective (One-to-One)

A function f : A → B is injective if it maps distinct inputs to distinct outputs. That is, if f(x) = f(y), then x = y. In terms of types, an injective function preserves information and does not “collapse” different inputs into the same output.

graph LR
    subgraph Domain ["Set A: Domain"]
        a1["a1"]
        a2["a2"]
        a3["a3"]
    end
    subgraph Codomain ["Set B: Codomain"]
        b1["b1"]
        b2["b2"]
        b3["b3"]
        b4["b4 (Unmapped)"]
    end
    a1 -->|"f"| b1
    a2 -->|"f"| b2
    a3 -->|"f"| b3

# Injective: every input x yields a unique output x + 1
successor = x: x + 1;

Surjective (Onto)

A function f : A → B is surjective if its range is equal to its codomain. In other words, for every element y ∈ B, there exists at least one element x ∈ A such that f(x) = y.

graph LR
    subgraph Domain ["Set A: Domain"]
        a1["a1"]
        a2["a2"]
        a3["a3"]
        a4["a4"]
    end
    subgraph Codomain ["Set B: Codomain (All Covered)"]
        b1["b1"]
        b2["b2"]
    end
    a1 -->|"f"| b1
    a2 -->|"f"| b1
    a3 -->|"f"| b2
    a4 -->|"f"| b2

# Surjective onto booleans: both true and false are reachable outputs
isEven = x: (x / 2) * 2 == x;

Bijective (One-to-One Correspondence)

A function that is both injective (one-to-one) and surjective (onto). A bijection establishes a perfect pairing between the elements of domain A and codomain B.

graph LR
    subgraph Domain ["Set A: Domain"]
        a1["a1"]
        a2["a2"]
        a3["a3"]
    end
    subgraph Codomain ["Set B: Codomain"]
        b1["b1"]
        b2["b2"]
        b3["b3"]
    end
    a1 ---|"1-to-1"| b1
    a2 ---|"1-to-1"| b2
    a3 ---|"1-to-1"| b3

# Bijective: 1-to-1 correspondence on boolean values
not = _val: !_val;

Inverse Function

An inverse function f⁻¹ : B → A is a function that perfectly reverses the mapping of a function f : A → B, such that f⁻¹(f(x)) = x for all x ∈ A and f(f⁻¹(y)) = y for all y ∈ B. A function possesses a unique, two-sided inverse if and only if it is bijective.

In functional programming, implementing an inverse function is essential when we need to round-trip data, such as with parsers/pretty-printers or encryption/decryption keys.

graph LR
    A["Domain: Set A"] -->|"f"| B["Codomain: Set B"]
    B -->|"f⁻¹ (Inverse)"| A

# f : Int -> Int
f = x: x + 5;

# f_inverse : Int -> Int
f_inverse = x: x - 5;

Endomorphism

An endomorphism is a morphism (or function) whose domain and codomain are exactly the same set or object, written f : A → A.

In functional programming, endomorphisms are extremely common, often referred to as endofunctions. Examples include string formatting, sorting lists, or updating records, where the input and output types are identical. Endofunctions are particularly powerful because they can be composed indefinitely with themselves or other endofunctions of the same type.

# An endomorphism on the type String (String -> String)
shout = s: s + "!";

Composition

The process of chaining functions together where the output of one function becomes the input of another. If f : A → B and g : B → C, their composition g ∘ f : A → C is defined by (g ∘ f)(x) = g(f(x)). In functional programming, composition is the primary tool for building complex pipelines out of small, reusable functions.

graph LR
    A["Type A"] -->|"f"| B["Type B"]
    B -->|"g"| C["Type C"]
    A -.->|"g ∘ f"| C

let
  addOne = x: x + 1;
  double = x: x * 2;
in
# Composition: g(f(x))
doubleThenAddOne = x: addOne (double x);

Pure Function

A function that has no side effects and, when given the same input, always returns the same output. A pure function corresponds exactly to a mathematical function between sets. Impure functions (which modify global variables or perform unpredictable I/O) cannot be modeled as simple set-theoretic functions.

# Pure: Nix functions are pure by design, having no side effects and being deterministic
add = a: b: a + b;

Idempotence

A function f : A → A is idempotent if applying it multiple times yields the exact same result as applying it once: f(f(x)) = f(x)  for all x ∈ A

In software systems and functional programming, idempotence is crucial for robust architectures:

• Build systems (like Nix): Building a derivation multiple times produces the exact same store path and output without side effects.
• Normalization & Formatting: Formatting a document or sanitizing input string repeatedly has no extra effect after the first run (f(f(s)) = f(s)).
• Network & Distributed Systems: Safe retries of operations without duplicating state changes.

graph LR
    x["Input: x"] -->|"f"| fx["f(x)"]
    fx -->|"f"| ffx["f(f(x)) = f(x) (Stable)"]

# Absolute value is idempotent: abs(abs(x)) == abs(x)
abs = x: if x < 0 then -x else x;
isIdempotent = abs (abs (-5)) == abs (-5); # true

Involution

An involution is a function f : A → A that is its own inverse: f(f(x)) = x  for all x ∈ A

Applying an involution twice restores the original input value. Common examples in programming include boolean negation (not), arithmetic negation (-x), and symmetric encodings (like XOR encryption or array reverse).

graph LR
    x["x"] -->|"f"| fx["f(x)"]
    fx -->|"f"| x_restored["x (Restored)"]

# Boolean negation is an involution: not (not x) == x
not = b: !b;
isInvolution = not (not true) == true; # true

Fixed Point

For a function f : A → A, a fixed point is a value x ∈ A that is mapped to itself by f: f(x) = x

In functional programming, the concept of a fixed point is foundational to recursion theory. Higher-order functions called fixed-point combinators (such as the Y combinator or Nix’s builtins.fix) allow recursion to be defined mathematically without named self-references, enabling lazy dependency resolution and open recursive attribute sets.

graph LR
    x["Fixed Point: x"] -->|"f"| x

# builtins.fix calculates the least fixed point of an open recursive attribute set function
pkgs = builtins.fix (self: {
  base = 10;
  total = self.base + 5; # self references the fixed-point outcome
});
# pkgs.total evaluates to 15

Immutability

The property of an object or value whose state cannot be modified after it is created. In purely functional programming, variables are immutable; once a value is defined, it never changes. This mirrors mathematical variables in set theory, which represent fixed, unchanging values.

let
  x = 42;     # The value bound to x cannot be mutated
  y = x + 1;  # Creating a new environment/scope bindings without mutating x
in
y

First-Class Functions

A language feature where functions are treated as first-class citizens. They can be assigned to variables, passed as arguments to other functions, and returned as values. Mathematically, this corresponds to treating the set of all functions from A to B (denoted B^A or A → B) as a valid set of its own, over which we can define other functions.

let
  square = x: x * x;
  apply = f: val: f val;
in
apply square 5 # Evaluates to 25

Higher-Order Function (HOF)

A function that either takes one or more functions as arguments or returns a function as its result. Examples include map, filter, and fold. Mathematically, these are functions whose domains or codomains are themselves sets of functions.

let
  numbers = [ 1 2 3 4 ];
in
# builtins.map is a higher-order function taking a function and a list
doubled = builtins.map (x: x * 2) numbers; # [ 2 4 6 8 ]

Arity

The arity of a function is the number of arguments or operands that the function takes:

• Nullary (arity 0): A function taking no arguments (a constant or thunk).
• Unary (arity 1): A function taking one argument (f : A → B).
• Binary (arity 2): A function taking two arguments (f : A × B → C).
• n-ary (arity n): A function taking n arguments.

In purely functional languages with currying, every function strictly has an arity of 1 (unary), with multi-argument functions simulated by returning sequences of unary functions.

# Nullary (thunk):
getTimestamp = _: 1726912800;

# Unary (arity 1):
increment = x: x + 1;

# Curried binary function (sequence of unary functions):
add = a: b: a + b;

Currying

The technique of translating a function that takes multiple arguments into a sequence of functions that each take a single argument. A function f : (A × B) → C is curried into f_curry : A → (B → C). In curried form, passing the first argument returns a new function waiting for the second.

graph TD
    subgraph Uncurried ["Uncurried: (A × B) → C"]
        pair["(a, b)"] -->|"f"| c1["Result c"]
    end
    subgraph Curried ["Curried: A → (B → C)"]
        a["Argument a"] -->|"f_curry"| f_b["Function: (b -> c)"]
        f_b -->|"Argument b"| c2["Result c"]
    end

let
  # Nix functions are curried by default: each function takes exactly one argument
  # and returns another function if more arguments are defined.
  curriedAdd = a: b: a + b;
  addFive = curriedAdd 5;
in
addFive 3 # Evaluates to 8

Partial Application

The process of fixing a number of arguments to a multi-argument function, yielding a new function of smaller arity. Because functional languages curry functions by default, partial application is as simple as providing fewer arguments than the function expects.

let
  multiply = a: b: a * b;
  triple = multiply 3;  # Partially applied with a = 3
in
triple 4                # Evaluates to 12

Point-Free (Tacit Programming)

A style of writing functions where the function arguments (the “points” or elements of the domain) are not explicitly named or referenced. Instead, the function is defined purely through the composition of other functions and partial application. For example, instead of writing doubleAndAddOne x = addOne (double x), point-free style defines it as doubleAndAddOne = addOne . double.

let
  # Custom curried filter definition
  filter = pred: list: builtins.filter pred list;
  isPositive = x: x > 0;

  # Point-free: no mention of the list argument
  positives = filter isPositive;
in
positives [ (-2) (-1) 0 1 2 ] # [ 1 2 ]

Recursion

A programming technique where a function calls itself to solve smaller instances of the same problem. Because purely functional programming languages do not have mutable loop variables (like for or while in imperative programming), recursion is the primary mechanism for iteration and processing recursive data structures (like lists and trees).

let
  factorial = n: if n <= 1 then 1 else n * factorial (n - 1);
in
factorial 5 # Evaluates to 120

Parametricity (“Theorems for Free”)

Parametricity is the mathematical property that parametric polymorphic functions (functions operating over generic type variables ∀A) behave uniformly regardless of the concrete type supplied. Because the function cannot inspect or branch on runtime type representations, its behavior is strictly bound by its type signature.

Introduced by Phil Wadler as “Theorems for Free!”, parametricity guarantees fundamental laws without looking at function implementations. For example, any function with signature f : ∀A. [A] → [A] cannot create elements of type A out of thin air: it can only filter, permute, duplicate, or drop elements from the input list.

# Any purely polymorphic function listTransform : forall a. [a] -> [a]
# must satisfy Wadler's naturality condition: map g (transform xs) == transform (map g xs)
reverse = list:
  let
    step = acc: x: [ x ] ++ acc;
  in
  builtins.foldl' step [ ] list;

# This law holds unconditionally for any function g and list xs:
# map (x: x * 2) (reverse [ 1 2 3 ]) == reverse (map (x: x * 2) [ 1 2 3 ])

Strict vs. Non-Strict (Lazy) Evaluation

In programming language semantics and λ-calculus, evaluation strategies describe when expressions and function arguments are reduced:

• Strict Evaluation (Call-by-Value / Eager): Arguments are fully evaluated to values before being passed into a function. If an argument evaluation diverges (⊥, crashes or infinite loops), the entire function call diverges.
• Non-Strict Evaluation (Call-by-Need / Lazy): Arguments are not evaluated until their actual values are demanded by computation. Once evaluated, results are memoized (sharing / graph reduction).

Non-strict evaluation (native to Nix and Haskell) allows defining infinite data structures (corecursion), writing custom control-flow structures as normal functions, and evaluating modular configurations where unused attributes cost zero compute.

# In Nix (lazy by default), unused expressions that would otherwise crash are never evaluated:
lazyIf = cond: thenVal: elseVal: if cond then thenVal else elseVal;

# (throw "error") is never evaluated because cond is true:
result = lazyIf true "success" (throw "error"); # evaluates safely to "success"

3. Order Theory & Abstract Algebra

Abstract algebra and order theory study sets equipped with binary operations or relations satisfying specific algebraic laws (such as associativity, identity, and symmetry).

Divisibility

In mathematics, divisibility is a relation between two integers: an integer a is divisible by b (written b ∣ a) if there exists an integer k such that a = k ⋅ b. In functional terms, divisibility represents a predicate (a function returning a boolean): isDivisibleBy : Int → Int → Bool where isDivisibleBy b a checks if the remainder of a/b is zero. This relation is reflexive (a ∣ a), transitive (if a ∣ b and b ∣ c, then a ∣ c), and anti-symmetric (if a ∣ b and b ∣ a, then a = b or a = −b), making it a partial order on non-negative integers.

# divisibility predicate using integer division check (since Nix has no % operator)
isDivisibleBy = b: a: (a / b) * b == a;

Partially Ordered Set (Poset)

A partially ordered set (or poset) is a set S equipped with a binary relation ≤ (a partial order) that is reflexive (a ≤ a), antisymmetric (if a ≤ b and b ≤ a, then a = b), and transitive (if a ≤ b and b ≤ c, then a ≤ c). Unlike a total order, some elements in a poset may be incomparable.

In functional systems, posets model dependency graphs, subtyping hierarchies, version constraints, or partial ordering in build steps (like Nix derivation dependency trees).

graph TD
    v120["Version 1.2.0"] --> v110["Version 1.1.0"]
    v120 --> v101["Version 1.0.1"]
    v110 --> v100["Version 1.0.0"]
    v101 --> v100

# A partial order checking if version A is compatible-with/less-than-or-equal-to version B
# represented as [major minor] pairs
leVersion = a: b:
  let
    a_major = builtins.elemAt a 0;
    a_minor = builtins.elemAt a 1;
    b_major = builtins.elemAt b 0;
    b_minor = builtins.elemAt b 1;
  in
  a_major < b_major || (a_major == b_major && a_minor <= b_minor);

Lattice (Join & Meet)

A lattice is a poset L in which every pair of elements a, b ∈ L has a unique:

1. Least Upper Bound (supremum, join ∨): the smallest element greater than or equal to both a and b.
2. Greatest Lower Bound (infimum, meet ∧): the largest element less than or equal to both a and b.

If a lattice has a minimum element ⊥ (bottom) and maximum element ⊤ (top), it is called a bounded lattice. In functional programming, lattices are foundational for:

• Type Inference & Subtyping: Finding the least common supertype (join) or greatest common subtype (meet).
• Conflict-Free Replicated Data Types (CRDTs): Distributed synchronization where concurrent edits are merged via deterministic lattice joins (a ∨ b).

graph TD
    Join["Top / Supremum (a ∨ b): Least Upper Bound"]
    Join --- A["Element a"]
    Join --- B["Element b"]
    A --- Meet["Bottom / Infimum (a ∧ b): Greatest Lower Bound"]
    B --- Meet

# A bounded lattice for integer intervals / min-max bounds
meet = a: b: if a < b then a else b; # infimum (min)
join = a: b: if a > b then a else b; # supremum (max)

Distributivity

A binary operation * distributes over another binary operation + if: a * (b + c) = (a * b) + (a * c)  and  (b + c) * a = (b * a) + (c * a)

In Type Algebra, multiplication represents product types (×) and addition represents sum types (+). Distributivity describes the fundamental type isomorphism: A × (B + C) ≅ (A × B) + (A × C)

A record containing a tagged union/sum type contains the exact same information as a tagged union of records.

# Record containing a sum type (A * (B + C)):
leftSide = { id = 1; payload = { type = "text"; value = "hello"; }; };

# Isomorphic to a sum type of records ((A * B) + (A * C)):
rightSide = { type = "text"; id = 1; value = "hello"; };

Associativity

A property of a binary operation where the grouping of parentheses does not alter the final result. For an operation *, associativity means (a * b) * c = a * (b * c) for all elements a, b, c. In functional programming, function composition is associative: (h ∘ g) ∘ f = h ∘ (g ∘ f). Similarly, monadic bind and monoid operations must adhere to associativity laws to ensure computations produce predictable results regardless of how they are nested or grouped.

let
  a = 1;
  b = 2;
  c = 3;
in
# (a + b) + c == a + (b + c)
isAssociative = (a + b) + c == a + (b + c); # evaluates to true

Commutativity

A property of a binary operation where changing the order of the operands does not change the result. For an operation *, commutativity means a * b = b * a for all elements a, b. In programming, while addition (+) and multiplication (*) are commutative, most structures and actions (like string concatenation or monadic computations) are non-commutative; the order of operations matters. If a monoid is commutative, it is called a commutative monoid (or abelian monoid). Similarly, a monad whose bind operation is order-independent is a commutative monad.

let
  a = 5;
  b = 10;

  isCommutative = a + b == b + a;                 # true
  isConcatCommutative = "${"a"}${"b"}" == "${"b"}${"a"}"; # false (string interpolation is non-commutative)
in
isCommutative

Semigroup

In abstract algebra, a semigroup is a set equipped with an associative binary operation. It is a simpler algebraic structure than a monoid because it does not require an identity element. For example, the set of positive integers under addition is a semigroup (but not a monoid, as 0 is not a positive integer). In functional programming, types that implement an associative combine function (like Elm’s List.append or Haskell’s <>) form semigroups.

# Semigroup combine operation for lists (concatenation)
combineList = a: b: a ++ b;

Monoid

In abstract algebra and category theory, a monoid is a semigroup that also has an identity element. That is, a set equipped with an associative binary operation and an identity element e such that e * x = x * e = x for all elements x. For example, the set of integers under addition with identity 0 is a monoid, as is the set of lists under concatenation with the empty list [] as the identity.

# Monoid implementation for lists in Nix
monoidList = {
  empty = [ ];
  combine = a: b: a ++ b;
};

Group

In abstract algebra, a group is a monoid where every element a possesses an inverse element a⁻¹ such that: a * a⁻¹ = a⁻¹ * a = e  (where e is the identity element)

While monoids describe operations that accumulate data (like list concatenation or string appending), groups describe systems where operations are completely reversible (like transactional rollback logs, differential counters, vector geometry rotations, or undo-redo buffers).

# The group of integers under addition:
groupIntAddition = {
  identity = 0;
  combine = a: b: a + b;
  inverse = a: -a; # a + (-a) == 0
};

Abelian Group (Commutative Group)

An abelian group (or commutative group) is a group (G, *, e) whose binary operation is also commutative: a * b = b * a  for all a, b ∈ G

In functional systems, abelian groups guarantee that operations can be executed concurrently and merged in any arbitrary order without lock-step ordering (such as additive counters in distributed CRDTs).

# Integers under addition form an abelian group because a + b == b + a
isAbelian = a: b: (a + b) == (b + a);

Monoid Homomorphism

A monoid homomorphism is a function h : M → N between two monoids (M, ⋅_M, e_M) and (N, ⋅_N, e_N) that preserves both the identity element and the associative binary operation:

1. h(e_M) = e_N
2. h(a⋅_Mb) = h(a)⋅_Nh(b)  for all a, b ∈ M

In functional software engineering and big data processing, monoid homomorphisms are the exact mathematical requirement that makes MapReduce and parallel reduction safe: chunking a dataset into partitions, mapping each partition to a monoid, and combining results across separate CPU cores or cluster nodes yields the exact same answer as sequential processing.

graph TD
    subgraph Source ["Monoid M: (String, ++, '')"]
        s_pair["('foo', 'bar')"] -->|"combine: ++"| s_res["'foobar'"]
    end
    subgraph Target ["Monoid N: (Int, +, 0)"]
        t_pair["(3, 3)"] -->|"combine: +"| t_res["6"]
    end
    s_pair -->|"h: stringLength"| t_pair
    s_res -->|"h: stringLength"| t_res

# String length is a monoid homomorphism from (String, +, "") to (Int, +, 0):
# 1. stringLength "" == 0
# 2. stringLength ("hello" + "world") == (stringLength "hello") + (stringLength "world")
strLength = s: builtins.stringLength s;
isHomomorphism = strLength ("foo" + "bar") == (strLength "foo") + (strLength "bar"); # true

Semiring (Rig) and Ring

A semiring (often called a rig because it is a “ring without negative elements / N”) is an algebraic structure equipped with two binary operations, addition (+) and multiplication (⋅), such that:

• (R, +, 0) is a commutative monoid.
• (R, ⋅, 1) is a monoid.
• Multiplication distributes over addition: a ⋅ (b + c) = (a ⋅ b) + (a ⋅ c).
• Multiplication by 0 annihilates: 0 ⋅ a = a ⋅ 0 = 0.

If every element also has an additive inverse −a (so (R, +, 0) forms an abelian group), the structure is a ring.

In functional programming, semirings model:

• Probabilistic Programming: Addition represents disjoint probabilities; multiplication represents independent joint events.
• Shortest Path & Graph Search: The tropical semiring where “addition” is min(a, b) and “multiplication” is a + b.

# Tropical semiring for shortest path calculations:
tropicalSemiring = {
  zero = 999999; # conceptual infinity (additive identity)
  one = 0;       # multiplicative identity
  add = a: b: if a < b then a else b; # min
  multiply = a: b: a + b;
};

Additive Identity vs. Multiplicative Identity

When an algebraic structure (such as a ring, semiring, or type algebra) has two binary operations, conventionally called addition (+) and multiplication (× or ⋅), each operation is governed by its own respective identity element:

• Additive Identity (0 / e₊ / ⊥): The neutral element for the addition operation, satisfying a + 0 = 0 + a = a. Under multiplication, it acts as an annihilator / absorbing element: a × 0 = 0 × a = 0.
  • Standard Arithmetic: 0 (x + 0 = x and x × 0 = 0)
  • Logic / Booleans: False (p ∨ False = p and p ∧ False = False)
  • Type Algebra (Sum Types): Void / Never (A + Void ≅ A and A × Void ≅ Void)
  • Tropical Semiring (min ): +∞ (min (x, +∞) = x)
• Multiplicative Identity (1 / e_× / ⊤): The neutral element for the multiplication operation, satisfying a × 1 = 1 × a = a.
  • Standard Arithmetic: 1 (x × 1 = x)
  • Logic / Booleans: True (p ∧ True = p)
  • Type Algebra (Product Types): Unit / () (A × Unit ≅ A)
  • Tropical Semiring (+): 0 (x + 0 = x)

# In Type Algebra:
# Additive identity is Void (Bottom type):
# Sum type: Either A Void is isomorphic to A
# Product annihilation: Pair A Void is uninhabited (Void)

# Multiplicative identity is Unit / null:
# Product type: Pair A Unit is isomorphic to A:
pairWithUnit = val: { fst = val; snd = null; };
unwrapFromUnit = pair: pair.fst; # preserves exact value

4. Category Theory

Category theory provides a unified language for structural mathematics, modeling collections of objects (types) and morphisms (functions) along with rules for composing them.

Category

In category theory, a category is a collection of objects (which, in functional programming, map to types) and arrows (morphisms, which map to functions) between those objects. A category must satisfy identity laws (every object has an identity arrow) and associativity (composition of arrows is associative).

# Identity morphism for any Nix value
id = x: x;

Morphism

A morphism (or arrow) f : A → B is a mapping from a source object A (domain) to a target object B (codomain) within a category. In functional programming, morphisms correspond to functions between types.

The set of all morphisms from object A to object B in a category 𝒞 is called the Hom-set, denoted Hom_𝒞(A, B) or 𝒞(A, B).

# Morphism mapping a String to an Integer (representing its length)
stringLength = s: builtins.stringLength s;

Monomorphism and Epimorphism (Monic & Epic)

In category theory, monomorphisms and epimorphisms are the arrow-theoretic generalizations of injective and surjective functions:

• Monomorphism (Monic Arrow): A morphism f : A → B is monic if it is left-cancellable: for any morphisms g, h : X → A, if f ∘ g = f ∘ h, then g = h. In set/type categories, monomorphisms correspond exactly to injective functions.
• Epimorphism (Epic Arrow): A morphism f : A → B is epic if it is right-cancellable: for any morphisms g, h : B → Y, if g ∘ f = h ∘ f, then g = h. In set/type categories, epimorphisms correspond to surjective functions.

# Successor is a monomorphism (injective function on integers)
successor = x: x + 1;

Identity

For every object A in a category, there exists an identity morphism id_A : A → A such that for any morphism f : A → B, we have f ∘ id_A = f = id_B ∘ f.

# Identity function in Nix
id = x: x;

Initial Object

An initial object (often denoted 0 or ∅) in a category is an object such that for every object X, there exists exactly one unique morphism 0 → X. In functional programming, this corresponds to an uninhabited/empty type (such as Void or Never).

graph LR
    Init["Initial Object: 0 (Void)"] -->|"! (Unique morphism: absurd)"| X["Object X"]
    Init -->|"! (Unique morphism: absurd)"| Y["Object Y"]

# In Nix, a conceptual Void type has no valid values.
# The unique morphism from Void to any other type (often called 'absurd') can never be executed:
absurd = voidValue: throw "This is unreachable because Void cannot be instantiated";

Terminal Object

A terminal object (often denoted 1) in a category is an object such that for every object X, there exists exactly one unique morphism X → 1. In functional programming, this corresponds to the unit type () (or Unit), which contains exactly one value.

graph LR
    X["Object X"] -->|"! (Unique morphism: toTerminal)"| Term["Terminal Object: 1 (Unit)"]
    Y["Object Y"] -->|"! (Unique morphism: toTerminal)"| Term

# In Nix, we can model the unit type/terminal object as null.
# For any value x of any type, there is a unique mapping to the terminal object:
toTerminal = x: null;

Product (Category Theory)

The product of two objects A and B is an object A × B equipped with two projection morphisms p₁ : A × B → A and p₂ : A × B → B such that for any other object Y and morphisms f : Y → A and g : Y → B, there exists a unique morphism h : Y → A × B satisfying p₁ ∘ h = f and p₂ ∘ h = g. In functional programming, this is a product type, such as a tuple, record, or attribute set.

graph TD
    Y["Object Y"] -->|"f"| A["Object A"]
    Y -->|"g"| B["Object B"]
    Y -.->|"h (Unique pair mapping)"| Prod["Product: A × B"]
    Prod -->|"p1 (fst)"| A
    Prod -->|"p2 (snd)"| B

# A product type constructor in Nix:
pair = a: b: { fst = a; snd = b; };

# Projections:
p1 = p: p.fst;
p2 = p: p.snd;

Coproduct (Category Theory)

The coproduct (or sum) of two objects A and B is an object A + B equipped with two injection morphisms i₁ : A → A + B and i₂ : B → A + B such that for any other object Y and morphisms f : A → Y and g : B → Y, there exists a unique morphism h : A + B → Y satisfying h ∘ i₁ = f and h ∘ i₂ = g. In functional programming, this represents sum types/tagged unions (e.g. Either or Result).

graph TD
    A["Object A"] -->|"f"| Y["Object Y"]
    B["Object B"] -->|"g"| Y
    A -->|"i1 (left)"| Coprod["Coproduct: A + B"]
    B -->|"i2 (right)"| Coprod
    Coprod -.->|"h (Unique fold mapping)"| Y

# Coproduct constructor in Nix:
left = a: { type = "left"; value = a; };
right = b: { type = "right"; value = b; };

# Morphism mapping (A + B) -> Y:
coproductFold = f: g: x:
  if x.type == "left"
  then f x.value
  else g x.value;

Isomorphism

An isomorphism is a bijective mapping between two structures that preserves their properties. If two types A and B are isomorphic (written A ≅ B), it means they contain the exact same amount of information, and you can convert back and forth between them without losing any data. There exist functions f : A → B and g : B → A such that g ∘ f is the identity on A, and f ∘ g is the identity on B.

graph LR
    A["Type A"] -->|"f"| B["Type B"]
    B -->|"g"| A

# Attribute sets { fst = a; snd = b; } and { fst = b; snd = a; } are isomorphic
forward = pair: { fst = pair.snd; snd = pair.fst; };
backward = pair: { fst = pair.snd; snd = pair.fst; };

Curry-Howard Isomorphism

The Curry-Howard isomorphism (also known as the propositions-as-types and proofs-as-programs correspondence) is the deep mathematical equivalence between formal logic and type theory:

• A logical proposition (statement) corresponds to a type.
• A proof of that proposition corresponds to a program (or expression) that evaluates to that type.
• Logical AND (∧) corresponds to Product Types (A × B).
• Logical OR (∨) corresponds to Sum Types (A + B).
• Logical Implication (A ⟹ B) corresponds to Function Types (A → B).
• Falsity / Contradiction (⊥) corresponds to the Bottom Type (Void / Never).

This isomorphism explains why strongly-typed functional programs can be proven correct: a valid, well-typed program is literally a constructive mathematical proof that the type’s specification holds.

graph LR
    subgraph Logic ["Mathematical Logic"]
        p["Proposition (Formula)"]
        proof["Proof of Proposition"]
        and["Logical AND (∧)"]
        or["Logical OR (∨)"]
    end
    subgraph Types ["Type Theory / FP"]
        t["Type"]
        prog["Program / Expression"]
        prod["Product Type (×)"]
        sum["Sum Type (+)"]
    end
    p <-->|"Equivalent"| t
    proof <-->|"Equivalent"| prog
    and <-->|"Equivalent"| prod
    or <-->|"Equivalent"| sum

# A proof that (A AND B) implies A:
# In logic: (A ∧ B) → A
# In FP: a function extracting the first element from a product type
fstProof = pair: pair.fst;

Adjunction (Currying & Exponential Objects)

An adjunction is a relationship between two functors pointing in opposite directions that captures a weak form of equivalence. In cartesian closed categories, the product functor (− × B) and exponential/function functor (−^B) form an adjunction: Hom(A × B, C) ≅ Hom(A, C^B)

This categorical adjunction is the formal mathematical definition of Currying: a function taking a pair of arguments (A, B) -> C contains the exact same information as a higher-order function A -> (B -> C).

graph LR
    Uncurried["Hom(A × B, C): (A, B) -> C"] <-->|"Adjunction (Curry ≅ Uncurry)"| Curried["Hom(A, Cᴮ): A -> (B -> C)"]

# The natural bijection between uncurried and curried functions:
curry = f: a: b: f { fst = a; snd = b; };
uncurry = f: pair: f pair.fst pair.snd;

Retraction and Section

In a category, for a morphism f : A → B:

• A morphism g : B → A is a left inverse (or retraction) if g ∘ f = id_A. When a retraction exists, f is called a section (and is injective/monic).
• A morphism g : B → A is a right inverse (or section) if f ∘ g = id_B. When a section exists, f is called a retraction (and is surjective/epic).

In programming, this maps directly to the design of codecs (serialization and deserialization). For example, a JSON serializer f : A → String and parser g : String → A form a retraction if parsing a serialized value always yields the exact same starting value (g(f(x)) = x).

graph LR
    A["Type A"] -->|"Section: f (Serialize)"| B["Type B (String)"]
    B -->|"Retraction: g (Deserialize)"| A

# A codec for integers to string representable values
serialize = x: toString x;
deserialize = s: builtins.fromTOML "val = ${s}" .val;

# retraction check: deserialize (serialize x) == x
retraction = x: deserialize (serialize x); # returns x

Lens / Optics

In category theory, a lens is a pair of morphisms that provides bidirectional access to a subpart A of a larger product/record structure S:

1. Getter / View: get : S → A
2. Setter / Update: set : S → A → S

Lenses must satisfy the lens laws:

• Get-Put: set(s, get(s)) = s (setting what you just got changes nothing)
• Put-Get: get(set(s, a)) = a (getting after setting returns the new value)
• Put-Put: set(set(s, a), b) = set(s, b) (two consecutive sets overwrite cleanly)

In functional programming, lenses and optics provide purely functional, composable getter/setter pipelines for deeply nested records and attribute sets.

graph LR
    Record["Whole Record: S"] -->|"get (View)"| Focus["Focused Part: A"]
    Focus -->|"set(s, newA)"| Updated["Updated Record: S"]

# Lens for accessing and updating the 'port' field of a server config:
portLens = {
  get = s: s.port;
  set = s: newPort: s // { port = newPort; };
  modify = s: f: s // { port = f s.port; };
};

config = { host = "localhost"; port = 80; };
updated = portLens.modify config (p: p + 8000); # { host = "localhost"; port = 8080; }

Prism (Optics for Sum Types)

While a Lens operates on Product Types (targeting fields that are guaranteed to exist), a Prism is an optic that operates on Sum Types / Tagged Unions (targeting a specific variant that may or may not be present):

1. Preview / Match: preview : S → Option A (attempts to extract variant A from sum type S)
2. Review / Inject: review : A → S (constructs the whole sum type S from variant A)

Prisms allow safe, composable pattern matching and updates on deeply nested algebraic variants without exhaustive manual switch/case branches.

# Prism for the 'success' variant of a Result sum type:
successPrism = {
  preview = res: if res.type == "ok" then { type = "some"; value = res.value; } else { type = "none"; };
  review = val: { type = "ok"; value = val; };
  modify = f: res: if res.type == "ok" then { type = "ok"; value = f res.value; } else res;
};

result = { type = "ok"; value = 42; };
modified = successPrism.modify (x: x * 2) result; # { type = "ok"; value = 84; }

Traversal (Optics for Collections)

A Traversal generalizes a Lens from a single focus target to 0, 1, or multiple focus targets simultaneously within a data structure or collection.

In functional programming, a Traversal combines the capability of map with composable optics, allowing developers to query, modify, or update every element matching a path inside deeply nested product and sum types.

# Traversal over all elements in a list:
listTraversal = {
  getAll = list: list;
  modifyAll = f: list: builtins.map f list;
};

numbers = [ 1 2 3 ];
doubledList = listTraversal.modifyAll (x: x * 2) numbers; # [ 2 4 6 ]

Opposite Category & Duality (𝒞^op)

For any category 𝒞, its opposite category (or dual category) 𝒞^op has the same objects as 𝒞, but with all morphism arrows reversed: a morphism f : A → B in 𝒞 becomes f^op : B → A in 𝒞^op.

Categorical Duality is the principle that every category-theoretic definition or theorem has a dual counterpart obtained by reversing all arrows. This explains the origin of the prefix “co-”:

• Product ×⇔ Coproduct +
• Initial Object 0⇔ Terminal Object 1
• Monad ⇔ Comonad
• Algebra ⇔ Coalgebra
• Covariant Functor ⇔ Contravariant Functor (𝒞^op → 𝒟)

# Reversing arrow composition order models the opposite category
reverseCompose = f: g: x: f (g x);

Functor

In category theory, a functor is a mapping between categories that preserves structure. In functional programming, a functor is a parameterized type (like List, Maybe, or Result) that implements a mapping function (usually called map or fmap). This mapping function applies a normal function A → B to values wrapped in the functor’s context, yielding a wrapped value of type B while preserving the structure of the container.

let
  # Option constructors
  some = x: { type = "some"; value = x; };
  none = { type = "none"; };

  # Functor map for Option
  optionMap = f: opt:
    if opt.type == "some"
    then some (f opt.value)
    else none;

  opt = some 5;
in
optionMap (x: x * 2) opt # { type = "some"; value = 10; }

Endofunctor

An endofunctor is a functor that maps a category back to itself. In functional programming, because we almost always work within a single category (the category of all types and functions, often called Hask or the category of types in Elm/Nix), every functor we define is actually an endofunctor (mapping types to types, and functions to functions within that same category).

let
  # optionMap maps functions inside the same category of Nix values
  mappedOption = optionMap (s: builtins.stringLength s) (some "hello");
in
mappedOption # { type = "some"; value = 5; }

graph TD
    subgraph Category_X ["Category of Types"]
        direction LR
        A["Type A"] -->|"f"| B["Type B"]
        B -->|"g"| C["Type C"]
        A -->|"g ∘ f"| C
        A -->|"id_A"| A
        B -->|"id_B"| B
    end

    subgraph Category_FX ["Endofunctor Image"]
        direction LR
        FA["Type F A"] -->|"F f"| FB["Type F B"]
        FB -->|"F g"| FC["Type F C"]
        FA -->|"F(g ∘ f)"| FC
    end

    A -. "Functor F" .-> FA
    B -. "Functor F" .-> FB
    C -. "Functor F" .-> FC

Bifunctor

A bifunctor is a functor that takes two object arguments from product categories: F : 𝒞 × 𝒟 → ℰ. In functional programming, a bifunctor is a parameterized type taking two independent type parameters (like Pair A B or Either A B) equipped with a mapping function bimap: bimap : (A → A^′) → (B → B^′) → F(A, B) → F(A^′, B^′)

# Bifunctor bimap for pairs (Product type):
pairBimap = f: g: pair: { fst = f pair.fst; snd = g pair.snd; };

# Bifunctor bimap for Either (Sum type):
eitherBimap = f: g: either:
  if either.type == "left" then { type = "left"; value = f either.value; }
  else { type = "right"; value = g either.value; };

Natural Transformation

A natural transformation α : F ⟹ G is a mapping between two functors F, G : 𝒞 → 𝒟 that preserves category structure. For each object X in 𝒞, it provides a morphism α_X : F(X) → G(X) such that for any morphism f : X → Y, the naturality condition holds: α_Y ∘ F(f) = G(f) ∘ α_X. In functional programming, a natural transformation is a polymorphic/generic function of type forall a. F a -> G a.

graph TD
    FA["F(A)"] -->|"F(f)"| FB["F(B)"]
    FA -->|"alpha_A"| GA["G(A)"]
    FB -->|"alpha_B"| GB["G(B)"]
    GA -->|"G(f)"| GB["G(B)"]

let
  # Option constructors
  some = x: { type = "some"; value = x; };
  none = { type = "none"; };
in
# Natural transformation from Option to List:
optionToList = opt:
  if opt.type == "some"
  then [ opt.value ]
  else [ ];

Yoneda Lemma & Continuation-Passing Style (CPS)

The Yoneda Lemma is one of the deepest results in category theory. It states that for any functor F : 𝒞 → Set and object A, the natural transformations from the Hom-functor 𝒞(A, −) to F are in one-to-one isomorphic correspondence with elements of F(A): Nat(𝒞(A, −), F) ≅ F(A)

In functional programming, the Yoneda Lemma establishes that any data structure or value A is completely characterized by the set of all functions that can observe or consume it: forall R. (A → R) → R ≅ A

This is the exact mathematical foundation of:

• Continuation-Passing Style (CPS): Representing computations as functions waiting for a continuation callback (A -> R) -> R.
• Codensity / Yoneda Optimization: Transforming recursive pipelines into CPS to achieve O(1) function compositions and eliminate intermediate allocations (deforestation).

# Embedding a value into its Yoneda/CPS representation:
toYoneda = a: (k: k a);

# Extracting the value back from its Yoneda representation (using identity morphism as continuation):
fromYoneda = yonedaVal: yonedaVal (x: x);

# toYoneda 42 represents all possible observations; fromYoneda recovers 42:
recovered = fromYoneda (toYoneda 42); # 42

Applicative Functor

An applicative functor is a functor F equipped with two operations: pure : A \rightarrow F(A) (which embeds a value into a context) and `<*> : F(A B) F(A) F(B)$ (sequential application, which applies a wrapped function to a wrapped value). In category theory, an applicative functor is a strong lax monoidal endofunctor.

let
  # Option constructors
  some = x: { type = "some"; value = x; };
  none = { type = "none"; };

  # pure: embeds a value into Option
  pure = some;

  # ap (seq application <*>): applies wrapped function to wrapped value
  ap = fOpt: valOpt:
    if fOpt.type == "some" && valOpt.type == "some"
    then some (fOpt.value valOpt.value)
    else none;
in
# ap (pure (x: x + 1)) (some 5) -> { type = "some"; value = 6; }
ap

Contravariant Functor & Profunctor

While normal (covariant) functors map a function f : A → B to F(A) → F(B) (preserving arrow direction), a contravariant functor F : 𝒞^op → 𝒟 reverses the arrow direction: contramap : (B → A) → F(A) → F(B)

In functional programming, contravariant functors represent consumers or predicates (types that accept or consume values, rather than producing them):

• Predicates (Predicate A = A -> Bool)
• Encoders / Serializers (Encoder A = A -> String)

A profunctor P(A, B) generalizes this by being contravariant in its input type A and covariant in its output type B, mapping (A^′ → A) and (B → B^′) to P(A, B) → P(A^′, B^′).

# Contravariant predicate functor:
isEven = x: (x / 2) * 2 == x;

# contramap: converts a Predicate A into a Predicate B using (B -> A)
contramap = f: pred: x: pred (f x);

# Predicate for strings checking if their length is even:
isStringLengthEven = contramap (s: builtins.stringLength s) isEven;
# isStringLengthEven "hello" -> false, isStringLengthEven "four" -> true

Monad (A Monoid in the Category of Endofunctors of X)

A mathematical structure in category theory that has been adapted into a powerful design pattern in functional programming.

To define this with absolute precision based on Saunders Mac Lane’s classic formulation: “A monad in X is a monoid in the category of endofunctors of X.”

Here is exactly what each piece of this definition means:

1. The Category X: X represents the starting, underlying category of objects and arrows. In general mathematics, X is often the category of sets (Set). In functional programming, X is the category of types in our language (e.g. Hask in Haskell, or the category of Elm/Nix types), where the objects are types (Int, String, Bool) and the arrows are functions between them.
2. An Endofunctor of X: An endofunctor is a functor that maps a category back to itself (i.e. from X to X). In our case, a type constructor like Maybe or List maps any type A in X to another type Maybe A in X, and maps functions in X to corresponding functions over wrapped values.
3. The Category of Endofunctors of X (often denoted [X, X]): This is a functor category where the objects are the endofunctors of X themselves (such as Maybe, List, Result, etc.), and the morphisms (arrows) are natural transformations between these endofunctors (i.e., polymorphic functions that convert one functor container into another, such as safeHead : List A -> Maybe A, without knowing or changing the type A).
4. A Monoid in this Functor Category: A monoid requires a set/object, an associative binary operation, and an identity element. In the category of endofunctors [X, X], the “monoid” is a specific endofunctor M equipped with two natural transformations:
   • The Associative Binary Operation: The natural transformation join (or flatten / μ) which collapses nested contexts: μ : M ∘ M → M (in programming types: M (M A) -> M A). This is associative because for any triply-nested container M (M (M A)), flattening the outer two layers first and then the result yields the exact same outcome as flattening the inner two layers first and then the result.
   • The Identity Element: The natural transformation unit (or return / pure / η) which introduces values into the context: η : I_X → M (in programming types: A -> M A). It acts as the left and right identity because wrapping a value with unit and then flattening with join is a no-op (leaves the structure unchanged): join ∘ unit = id_M.

In daily programming, we use the bind operator (>>= or andThen) to sequence computations. The bind operation is mathematically derived by combining map and join: bind(f, m) = join(map(f, m))

let
  # we reuse the Option functor and constructors from above
  unit = some;

  join = opt:
    if opt.type == "some"
    then opt.value
    else none;

  bind = f: opt: join (optionMap f opt);

  # `join` (flattening nested endofunctors):
  nested = some (some 42);
  flattened = join nested; # { type = "some"; value = 42; }

  # `bind` (sequencing):
  bound = bind (x: if x > 0 then some (x * 2) else none) (some 10);
in
bound # { type = "some"; value = 20; }

Kleisli Arrow (Kleisli Composition)

For a monad M, a Kleisli arrow (or Kleisli morphism) is a function of the form f : A → M(B). While normal functions A → B compose with standard composition (∘), Kleisli arrows do not compose that way because of the monadic wrapper. Instead, they compose using Kleisli composition (often written as >=> or the fish operator), defined as: (g • f)(x) = bind(g, f(x))

In programming, Kleisli composition lets us compose functions that can cause monadic side effects (such as error handling, state tracking, or asynchronous steps) into a single unified pipeline.

let
  # we reuse the Option monad and bind from above
  half = x: if (x / 2) * 2 == x then some (x / 2) else none;
  addTen = x: some (x + 10);

  # Kleisli composition: (f >=> g)
  kleisliCompose = f: g: x: bind g (f x);

  halfThenAddTen = kleisliCompose half addTen;
in
halfThenAddTen 8 # evaluates to { type = "some"; value = 14; }

Monad Transformers (MT)

While Functors and Applicatives compose automatically (F(G(A)) is always an Applicative if F and G are Applicatives), Monads do not compose generically. That is, given two arbitrary Monads M and N, their nesting M(N(A)) is not guaranteed to form a valid Monad with a general join operation.

To combine multiple monadic capabilities (such as combining stateful computations, error handling, and environment reading), functional programming uses Monad Transformers (e.g. ExceptT, ReaderT, StateT). A monad transformer T wraps an underlying base monad M and equips the combined stack with a lift natural transformation: lift : M(A) → T(M)(A)

# An OptionT Monad Transformer wrapping a Reader/Config function monad:
# State monad base: (Config -> A)
# OptionT: (Config -> Option A)
optionT = {
  lift = baseComputation: (config: { type = "some"; value = baseComputation config; });
  bind = f: optTVal: (config:
    let res = optTVal config;
    in if res.type == "some" then (f res.value) config else { type = "none"; }
  );
};

Comonad (The Categorical Dual of Monad)

A comonad is the exact category-theoretic dual of a monad. Where a monad introduces values into a context (unit) and flattens nested contexts (join), a comonad extracts values from a context and duplicates/extends contexts:

1. Extract (Counit / ε): ε : W(A) → A (extracts the focus/value from the current context)
2. Duplicate (Co-join / δ): δ : W(A) → W(W(A)) (duplicates the context)
3. Extend (=>>): extend : (W(A) → B) → W(A) → W(B) (recomputes a local neighborhood over the entire structure)

In functional programming, comonads model context-dependent computation:

• Cellular Automata (e.g. Conway’s Game of Life): Each cell updates its state based on evaluating its local neighborhood context.
• Streams & Zippers: Focusing on a current item while maintaining access to history and future elements.
• Reactive UI Trees: Rendering components based on local focus within a larger global application state.

# A simple 1D Stream Zipper Comonad: focused on a current element with left/right streams
# extract: returns the focused element
extract = zipper: zipper.focus;

# extend: produces a new zipper where each position is the result of evaluating f over that context
extend = f: zipper: {
  focus = f zipper;
  left = builtins.map (l: f (zipper // { focus = l; })) zipper.left;
  right = builtins.map (r: f (zipper // { focus = r; })) zipper.right;
};

F-Algebra and F-Coalgebra

In category theory, algebras and coalgebras provide the mathematical foundation for recursive data types and stateful processes:

• F-Algebra: For an endofunctor F, an F-algebra is a pair (A, α) consisting of an object A (the carrier) and an evaluation morphism α : F(A) → A. It models how to construct and evaluate data structures. The initial F-algebra defines recursive data structures (like lists and trees).
• F-Coalgebra: The categorical dual of an F-algebra, consisting of an object S (the state space) and a transition morphism β : S → F(S). It models how to observe and unfold dynamic systems over time (like infinite streams, generators, and state machines). The final F-coalgebra defines corecursive data structures.

# An F-Algebra evaluation step for integer expressions (collapsing AST node to Int):
evalAlgebra = expr:
  if expr.type == "const" then expr.value
  else if expr.type == "add" then expr.left + expr.right
  else throw "Unknown node";

Catamorphism and Anamorphism (Recursion Schemes)

In category theory, generalized recursion over algebraic data structures is formalized through algebras and coalgebras:

• Catamorphism (Fold / Reduce): A universal morphism from an initial algebra to any other algebra, denoted ( |f| ). It tears down/collapses a recursive data structure into a summary value (e.g. summing a list or evaluating an abstract syntax tree).
• Anamorphism (Unfold / Generate): The dual of a catamorphism, mapping a seed value into a corecursive data structure, denoted [(g)]. It builds up a data structure step-by-step from a state (e.g. generating an infinite Fibonacci stream or generating a range of numbers).

graph TD
    subgraph Anamorphism ["Anamorphism: Unfold / Corecursion"]
        seed["Seed State: 0"] -->|"ana"| stream["Generated List: [ 0 1 2 3 4 ]"]
    end
    subgraph Catamorphism ["Catamorphism: Fold / Recursion"]
        stream -->|"cata"| summary["Summary Value: 10"]
    end

let
  # Catamorphism (Fold / Reduce): tears down a list to a single value
  cata = f: acc: list: builtins.foldl' f acc list;

  # Anamorphism (Unfold): generates a list from a seed state
  ana = predicate: step: seed:
    if predicate seed
    then [ ]
    else [ (step seed).value ] ++ ana predicate step (step seed).next;

  # Generating [ 0 1 2 3 4 ]:
  unfolded = ana (n: n >= 5) (n: { value = n; next = n + 1; }) 0;
  # Folding to sum (evaluates to 10):
  sum = cata (acc: x: acc + x) 0 unfolded;
in
sum

Hylomorphism (Divide-and-Conquer Fusion)

A hylomorphism, denoted [ [(c, a)] ], is the composition of an anamorphism (unfolding a seed state into an intermediate recursive structure) followed immediately by a catamorphism (folding and collapsing that structure into a summary result): hylo = cata ∘ ana

In functional compilers and advanced architectures, hylomorphisms model divide-and-conquer algorithms (such as Merge Sort or recursive factorials). Through deforestation (fusion), the intermediate virtual structure (e.g. the binary tree or list) is completely eliminated at runtime, executing the generation and reduction in a single memory-efficient pass.

graph LR
    Seed["Seed State: 5"] -->|"ana (Unfold)"| Virtual["Virtual Tree / Call Stack"]
    Virtual -->|"cata (Fold)"| Result["Final Reduced Value: 120"]
    Seed -.->|"hylo (Fused without allocation)"| Result

let
  # Direct hylomorphism fusing unfold and fold steps without storing intermediate list in memory:
  hylo = cataStep: baseVal: anaPred: anaStep: seed:
    if anaPred seed
    then baseVal
    else cataStep (anaStep seed).value (hylo cataStep baseVal anaPred anaStep (anaStep seed).next);

  # Factorial implemented as a hylomorphism:
  # Unfolds n down to 1, and folds by multiplying:
  factorialHylo = n: hylo (x: acc: x * acc) 1 (n: n <= 1) (n: { value = n; next = n - 1; }) n;
in
factorialHylo 5 # 120

5. Architectural & Design Patterns

Higher-level software engineering patterns built directly on mathematical properties of pure functions, algebraic data types, and monads.

Railway Oriented Programming (ROP)

A functional architectural pattern used to manage error handling and data flow in a sequence of operations. Inspired by a two-track railway, Railway Oriented Programming represents functions as tracks that accept an input and can either proceed along the “happy path” (the green track) or switch to the “error track” (the red track). If any function in the pipeline encounters an error and switches to the red track, all subsequent happy-path operations are bypassed, and the error propagates cleanly to the end. Mathematically, this is built on composition over the Either / Result monad.

graph LR
    Input["Input"] --> Step1["Step 1: parseNumber"]
    Step1 -->|"Ok (Happy path)"| Step2["Step 2: validatePositive"]
    Step2 -->|"Ok (Happy path)"| Success["Output: Ok 84"]
    Step1 -->|"Err (Error track)"| ErrorTrack["Error Track: Err"]
    Step2 -->|"Err (Error track)"| ErrorTrack
    ErrorTrack --> ErrorOutput["Output: Err"]

    style Step1 fill:#ffffff,stroke:#000000
    style Step2 fill:#ffffff,stroke:#000000
    style Success fill:#ffffff,stroke:#000000,stroke-width:2px
    style ErrorTrack fill:#ffffff,stroke:#000000,stroke-dasharray: 5 5
    style ErrorOutput fill:#ffffff,stroke:#000000,stroke-dasharray: 5 5

let
  # Result constructors
  ok = x: { type = "ok"; value = x; };
  err = e: { type = "err"; error = e; };

  # bind / and_then for Result
  andThen = f: res:
    if res.type == "ok"
    then f res.value
    else res;

  # map for Result
  mapResult = f: res:
    if res.type == "ok"
    then ok (f res.value)
    else res;

  # Mock validation and parsing functions
  parseNumber = s:
    if s == "42" then ok 42 else err "Not a number";

  validatePositive = n:
    if n > 0 then ok n else err "Must be positive";

  # Chain operations on the happy path; short-circuit on error track:
  result = mapResult (n: n * 2) (andThen validatePositive (parseNumber "42"));
in
result # evaluates to { type = "ok"; value = 84; }

Builder Pattern (Functional)

An architectural design pattern used to construct complex objects or configurations step-by-step. In object-oriented programming, this is traditionally implemented using mutable state. In functional programming, the Builder Pattern is implemented immutably as a sequence of pure, composable transition functions (or a pipeline of endofunctions: Builder -> Builder). Each step returns a brand-new, copy-on-write version of the builder structure, preserving referential transparency and ensuring configurations can be safely branched and reused without side effects.

graph LR
    C0["Initial: defaultServerConfig"] -->|"withPort 8080"| C1["New Config: { port: 8080, ... }"]
    C1 -->|"withMaxConnections 100"| C2["Final Config: { port: 8080, maxConnections: 100 }"]

let
  defaultServerConfig = {
    port = 80;
    maxConnections = 10;
  };

  withPort = port: config: config // { inherit port; };
  withMaxConnections = maxConnections: config: config // { inherit maxConnections; };

  # Immutable pipeline constructing configuration:
  config = withMaxConnections 100 (withPort 8080 defaultServerConfig);
in
config # evaluates to { port = 8080; maxConnections = 100; }

Free Monad & Interpreter Pattern

In category theory, a free construction generates the minimal algebraic structure (here, a Monad) satisfying algebraic laws over an arbitrary base structure (a Functor), without imposing any extra constraints or loss of information.

In functional programming, the Free Monad pattern separates the description of a computation (building an abstract syntax tree of domain operations) from its execution (an interpreter that evaluates the AST):

• Syntax / Program: A purely declarative, side-effect-free data structure describing what needs to happen.
• Interpreters: Separate functions that translate the AST into concrete actions (e.g. an interactive I/O interpreter vs. an in-memory mock interpreter for automated unit tests).

graph TD
    AST["Declarative Program (Free Monad AST)"]
    AST -->|"Interpret (Testing)"| Test["Mock Interpreter: In-Memory / Test Doubles"]
    AST -->|"Interpret (Production)"| Prod["Production Interpreter: Real Disk I/O / Cloud"]

# Declarative DSL instructions (AST nodes)
pure = val: { type = "pure"; value = val; };
readFile = path: next: { type = "read"; inherit path next; };
logMsg = msg: next: { type = "log"; inherit msg next; };

# Program: purely declarative AST
program = logMsg "Reading config..." (readFile "/etc/config" (content: pure content));

# Mock Interpreter for testing without actual disk I/O:
mockInterpret = ast:
  if ast.type == "pure" then ast.value
  else if ast.type == "log" then mockInterpret ast.next
  else if ast.type == "read" then mockInterpret (ast.next "mock-config-content")
  else throw "Unknown node";

State Machine as Coalgebra (Automata Theory)

In category theory, a coalgebra is the categorical dual of an algebra. While algebras describe how to construct data (like constructors in an algebraic data type), coalgebras describe how to observe and transition state over time.

A deterministic state machine (Mealy/Moore automaton) is formalized as a transition morphism: step : S × Input → S × Output or equivalently as a coalgebra S → (Output × S^Input).

In functional architecture, this is the exact formal underpinning of:

• The Elm Architecture (TEA) & Redux: update : Model × Msg → Model × Cmd
• Protocol Parsers & Event-Driven Systems: Processing continuous streams of events through pure transition functions without hidden mutable variables.

stateDiagram-v2
    [*] --> Red
    Red --> Green : next
    Green --> Yellow : next
    Yellow --> Red : next

# Pure state machine transition function: (State * Action) -> State
trafficLight = state: action:
  if state == "red" && action == "next" then "green"
  else if state == "green" && action == "next" then "yellow"
  else if state == "yellow" && action == "next" then "red"
  else state;

# Evolving state through a sequence of actions:
actions = [ "next" "next" "next" ];
finalState = builtins.foldl' trafficLight "red" actions; # "red"