Wir müssen wissen. Wir werden wissen
David Hilbert, Society of German Scientists and Physicians on 8 Sep. 1930

The term “functional programming” is frequently used to denote a programming paradigm characterized by immutability, higher-order functions, declarative style and the avoidance of side effects. Under this interpretation, functional programming appears as one paradigm among others, comparable to Object-oriented or imperative programming and defined primarily by a set of recommended practices.
This characterization, however, introduces a structural ambiguity. Paradigms are typically identified through patterns of use rather than through formally specified semantic constraints. As a consequence, their boundaries are inherently elastic: the presence or absence of mutation, side effects or object-like abstractions does not admit a principled threshold beyond which a language ceases to qualify as belonging to the paradigm. The resulting classification depends on degrees of adherence rather than on formally stated properties.
An alternative interpretation situates functional programming at the level of computational models rather than at that of programming paradigms. In this view, functional programming is grounded in the formal framework of the λ-calculus. Within such a framework, programs are identified with expressions, computation with reduction and functions with first-class abstractions. Properties such as referential transparency and the absence of mutable state are not stylistic prescriptions but structural constraints imposed by the underlying model.
The distinction between these two interpretations is not merely terminological. If functional programming is understood as a paradigm, its defining characteristics are normative and subject to reinterpretation. On the contrary, if it is understood as an instantiation of a formal model of computation, many of the properties commonly associated with it follow from semantic constraints rather than from design conventions.
The present work adopts the latter perspective. Its aim is not to advocate for a particular programming style, but to clarify the conceptual foundations underlying the term “functional programming” and to distinguish properties that are mathematically entailed from those that are contingently adopted in practice.

Functions as mathematical objects

Since this topic concerns functional programming in a mathematically grounded sense, it is necessary to clarify what is meant by a “function”.

Let 𝐴 and 𝐵 be sets. A binary relation 𝑅 ⊆ 𝐴 × 𝐵 is said to be:

• total if ∀𝑎 ∈ 𝐴, ∃ 𝑏 ∈ 𝐵 such that (𝑎,𝑏) ∈ 𝑅
• univalent if ∀𝑎 ∈ 𝐴, ∀𝑏1,𝑏2 ∈ 𝐵, (𝑎,𝑏1) ∈ 𝑅 ∧ (𝑎,𝑏2) ∈ 𝑅 ⇒ 𝑏1 = 𝑏2

A function from 𝐴 to 𝐵 is a relation that is both total and univalent.

This definition emphasizes that a function is not an instruction sequence, nor a computational mechanism, but a mathematical object characterized by determinacy and completeness of mapping.
Simple examples illustrate the distinction:

• The relation “is biological mother of” over the set of human beings is neither total (not every human is a biological mother in the domain considered) nor univalent
• Subtraction over the natural numbers, interpreted as a relation 𝑁 × 𝑁 → 𝑁, is univalent but not total, since 𝑎 − 𝑏 is undefined when 𝑏 > 𝑎
• The identity relation on a set is both total and univalent and therefore constitutes a function

This relational definition will serve as the mathematical backdrop against which lambda abstraction and typed functions are to be understood.

Non-total functions in practice

Many functions in conventional programming languages are not total: they fail to produce a value for some inputs of the declared type. This partiality may arise either because the function enters an infinite computation (non-termination) or because it aborts via an exception, which can be seen as a controlled form of non-termination: in both cases, no valid value of the declared type is returned.

NOTE
From a mathematical perspective, the “infinite computation” phenomenon deserves clarification. A recursive specification can be interpreted in two distinct ways. Under a declarative (extensional) reading, a definition characterizes the set of functions satisfying the stated equations. For instance, consider:

𝑔(𝑛) = 0 if 𝑛 = 0, 𝑔(𝑛 + 1) otherwise

Extensionally, any function that maps 0 to 0 and assigns arbitrary values elsewhere satisfies these clauses. The specification does not uniquely determine a function. In computability theory and programming language semantics, however, recursive definitions are interpreted operationally: they describe a computational process. Under this reading, evaluating 𝑔(𝑛) for 𝑛 > 0 produces an infinite unfolding and therefore does not terminate. The definition is understood as denoting the least fixed point compatible with the operational semantics, which in this case is a partial function undefined for all 𝑛 > 0. Non-termination is therefore not merely an implementation detail, but a structural feature of the computational interpretation of recursive definitions. Partiality arises from the interaction between recursion and effective computability.

const divide = (numerator: number, denominator: number): number => {
  if (denominator === 0) {
    throw new Error("division by zero");
  }
  return numerator / denominator;
};

Although this function type-checks, it is not total: it does not produce a valid output for all inputs of type number × number. At runtime, it may throw an exception (a mechanism to “transfer control”). In other words, the declared type does not faithfully represent the function’s behavior and correctness is deferred to runtime.
Totality can be enforced by making all possible outcomes explicit in the type. One approach is to encode the result as a sum type, distinguishing successful from failing cases:

type Result = number | Error;

const divide = (numerator: number, denominator: number): Result =>
  denominator === 0 ? new Error("division by zero") : numerator / denominator;

In this version, the type enforces handling of all possible cases, so the compiler participates in correctness: callers are required to address the error case and the function is total relative to its declared type. This shift moves failure from runtime to compile-time, a fundamental improvement when reasoning about correctness.
Languages such as Java attempt similar guarantees through checked exceptions. Whether this achieves true totality is debated, but at minimum it acknowledges the limitations of partial functions.

NOTE
ECMAScript does not enforce totality by construction. In these settings, it is necessary to represent partial functions as effectful computations, making potential failures explicit in the type system or in the program structure.

Functional programming: a reasonable formal definition

A preliminary formal characterization of functional programming can be attempted by relating it directly to the λ-calculus.
We say that a programming language admits functional programming in the strong sense if it embeds a λ-calculus fragment whose β-reduction semantics is preserved. More precisely, the language must support:

• first-class function abstraction
• application as a primitive form of computation
• the possibility of expressing arbitrary λ-terms modulo the language’s evaluation strategy (in the appropriate typed or untyped fragment under consideration; this distinction will be addressed in the following section on the “Simply typed λ-calculus”)

Under this characterization, a language qualifies as “functional” insofar as it embeds the λ-calculus as a reduction-preserving core. However, this embedding is semantically robust only if additional constructs do not introduce observable effects that interfere with substitutivity. In languages with mutable state, the λ-fragment remains syntactically valid, but its equational theory is no longer globally enforceable (the precise relationship between substitutivity, observable effects and purity will be analyzed in detail in a later section).
This definition is not trivial. Historically, many mainstream languages did not provide first-class function abstraction or higher-order functions. Earlier versions of languages such as Java or C#, for instance, lacked direct support for lambda abstraction and treated functions as second-class citizens.
A further clarification concerns “recursion”. In most contemporary programming languages, recursion is introduced as a primitive operational mechanism. In the λ-calculus, however, recursion is not primitive: it is obtained through fixed-point combinators, such as the Y-combinator. This distinction is conceptually significant. The untyped λ-calculus was developed as a foundational model of effective computation and its expressive power coincides extensionally with that of Turing-computable functions. Recursive definitions are therefore not presupposed but derived from higher-order abstraction.
Consequently, defining functional programming as a conservative extension of the λ-calculus emphasizes structural commitments rather than computational power. The distinguishing feature is not Turing completeness - a property shared by most modern languages - but the presence of a function-centered semantic core from which recursion, abstraction and composition arise intrinsically.

Simply typed λ-calculus

The untyped λ-calculus provides a minimal and expressive foundation for modeling computation. Its formal simplicity and expressive completeness allow it to represent all effectively computable functions. However, this generality comes at a structural cost: in the absence of restrictions on term formation, any expression may be applied to any other, including itself and the system admits non-terminating terms (e.g. Ω = (λ𝑥. 𝑥 𝑥)(λ𝑥. 𝑥 𝑥)).
While such unrestricted expressiveness is computationally adequate, it is unsuitable for logical interpretation. If programs are to be regarded as mathematical objects subject to formal reasoning, additional structure must be imposed.
Typed variants of the λ-calculus introduce this structure by constraining the formation and application of terms. One canonical example is the simply typed λ-calculus (STLC), in which every term is assigned a type and application is restricted to compatible abstractions. Unlike the untyped system, the STLC forbids unrestricted self-application and satisfies the property of strong normalization: every well-typed term reduces to a normal form.
This refinement has a significant consequence. The STLC is strictly less expressive than the untyped λ-calculus; in particular, it is not Turing-complete, since general recursion cannot be defined within the system without further extensions. This loss of expressive power is not incidental but structural: it is precisely what enables the calculus to support a consistent logical interpretation.

Lambda abstraction

To illustrate the operational continuity between the λ-calculus and modern programming languages, consider the classical 𝐾-combinator:

λ𝑥. λ𝑦. 𝑥

This term denotes a function that takes an argument 𝑥, returns a function of one argument 𝑦 and yields 𝑥, ignoring its second parameter.
In a contemporary typed language such as typescript, the same structure can be expressed directly:

const K =
  <X, Y>(x: X) =>
  (_: Y): X =>
    x;

The structural correspondence is immediate. The nested λ-abstractions map to nested function definitions; application corresponds to invocation; unused parameters are syntactically permissible. The term’s computational behavior is preserved.
This example should not be overinterpreted. The mere presence of lambda expressions in a language does not entail that the language is semantically reducible to the λ-calculus. However, the faithful embedding of such combinators demonstrates that the language admits, at minimum, a function-centered core expressive enough to encode λ-terms.
The introduction of explicit type parameters in the typescript version already anticipates a further refinement: once types are assigned, the combinator acquires a structural interpretation beyond computation. It is precisely this transition - from untyped abstraction to typed structure - that enables the correspondence between programs and logical propositions.

Towards “types as propositions”

One of the central topics in this work is the Curry-Howard isomorphism, which provides a rigorous foundation for understanding the benefits of typed functional programming in terms of “correctness” of programs. It has already been established that types are not a prerequisite for functional programming in general, but their adoption enables programs to be interpreted as formal objects subject to logical reasoning.
According to the Curry-Howard correspondence, types correspond to propositions and programs correspond to proofs. More precisely, a function type 𝐴 → 𝐵 corresponds to the proposition “𝐵 holds under hypothesis 𝐴”. The program implementing the function serves as a constructive proof. In this sense, programs can be treated as a proof system: proofs can be represented as programs, particularly as lambda terms, or equivalently, proofs can be executed as programs.
Let’s have a look at two tautologies:

proposition	description	type	program
𝐴 → 𝐴	if 𝐴 is true, then 𝐴 is true	(a: A) => A	const identity = <A>(a: A): A => a
𝐴 ∧ 𝐵 → 𝐴	if 𝐴 and 𝐵 are both true, then 𝐴 is true	([A, B]) => A	const fst = <A, B>([a]: [A, B]): A => a;

The existence of a program inhabiting the type provides a constructive demonstration of the corresponding logical proposition. The identity function proves 𝐴 → 𝐴, while fst proves (𝐴 ∧ 𝐵) → 𝐴. The type expresses the proposition and the program provides the proof.

proposition	description	type	program
𝐴 → ¬𝐴	if 𝐴 holds, then 𝐴 does not hold	(a: A): never	const nothing = <A>(a: A): never => ?

The one above is a logically inconsistent proposition. No total program can inhabit this type, reflecting the impossibility of proving a contradiction. The type system enforces correctness by disallowing constructions that would violate logical consistency.

Constructive proofs as programs

Formally, we can summarize the correspondence as follows:

• A proposition corresponds to a type
• A proof corresponds to a program

Proving a proposition corresponds to implementing a function with the corresponding type.
Take the logical tautology:

𝐴 → 𝐴

In typescript:

type Id<A> = (a: A) => A;

A function of this type can be implemented as:

const id = <A>(a: A): A => a;

The existence of this function constitutes the proof of the proposition.
When writing programs in a strongly typed functional style, correctness becomes a property enforced by the type system, not by convention. Typed functional programming thus enables the type system to serve as a formal mechanism for correctness, aligning program construction with proof construction.

Referential transparency and purity

In typed functional programming, correctness is not only about having well-typed programs, but also about reasoning reliably about program behavior. Two central properties facilitating such reasoning are referential transparency and purity. These properties ensure that programs behave predictably and can be manipulated algebraically, which is crucial when treating programs as proofs.

Referential transparency

A program is referentially transparent if any expression can be replaced by its value without affecting the behavior of the program.

Given a program 𝑃 and an evaluation function 𝑓:

∀𝑒 ∈ 𝑃, let 𝑒' = eval(𝑒), 𝑓(𝑃[𝑒:=𝑒']) = 𝑓(𝑃)

where 𝑃[𝑒:=𝑒'] denotes the program 𝑃 with 𝑒 replaced by 𝑒' and eval(𝑒) denotes the value 𝑒 evaluates to

Example:

const increment = (n: number): number => {
  console.log("incrementing");
  return n + 1;
};

Compare the following:

increment(increment(1));

increment(2);

Numerically, both expressions return 3, but they differ behaviorally: the first logs twice, the second logs once. Because substituting increment(1) with 2 changes the program’s observable behavior, increment is not referentially transparent.

Purity

Let 𝛴 denote the space of all possible program states. A function 𝑓: 𝐴 × 𝛴 → 𝐵 × 𝛴 is pure if it neither reads from nor modifies the ambient state. Formally:

∀𝑥 ∈ 𝐴, ∀𝜎 ∈ 𝛴, 𝑓(𝑥, 𝜎) = (𝑔(𝑥), 𝜎)

for some function 𝑔: 𝐴 → 𝐵 that depends only on 𝑥.

That is, the state component is passed through unchanged, and the output is fully determined by the argument alone. The type 𝐴 × 𝛴 → 𝐵 × 𝛴 describes the ambient computational model; purity is the constraint that 𝑓 inhabits only the well-behaved fragment of it.

NOTE
The λ-calculus is intrinsically referentially transparent.
Languages embedding λ-abstractions do not automatically inherit this property if they introduce observable effects such as mutable state.
However, some purely functional languages, such as Haskell, provide effectful features (e.g. IO) without compromising referential transparency. They achieve this by reifying effects as values within the type system, preserving substitutivity at the semantic level. In this sense, such languages can be understood as semantically conservative extensions of a pure λ-based core. The point is that effects are not performed during pure evaluation; they are represented as values whose interpretation is controlled by the runtime system.

Currying and partial application

Currying is a fundamental transformation in functional programming, converting a function of multiple arguments into a sequence of single-argument functions. It makes composability uniform.

Let 𝐴, 𝐵 and 𝐶 be sets. Define the two function sets:

𝐹 = { 𝑓 | 𝑓: 𝐴 × 𝐵 → 𝐶 }
𝐺 = { 𝑔 | 𝑔: 𝐴 → (𝐵 → 𝐶) }

There exists a bijection φ: 𝐹 → 𝐺 defined by φ(𝑓) = λ𝑎. λ𝑏. 𝑓(𝑎, 𝑏); hence 𝐹 ≅ 𝐺, i.e. (𝐴 × 𝐵 → 𝐶) ≅ (𝐴 → (𝐵 → 𝐶))

In purely functional languages like Haskell, all functions are curried by default, meaning 𝑓: 𝐴 → 𝐵 → 𝐶 is the norm rather than 𝑓: 𝐴 × 𝐵 → 𝐶. This makes partial application trivial: supplying only 𝑎 to a curried function yields a legitimate 𝐵 → 𝐶 value, enabling point-free composition.
Typescript example:

const compose =
  <A, B, C>(f: (b: B) => C, g: (a: A) => B) =>
  (a: A): C =>
    f(g(a));

const sum = (a: number) => (b: number): number => a + b;
const mul = (a: number) => (b: number): number => a * b;
const sumFive: (b: number) => number = sum(5);
const mulThree: (b: number) => number = mul(3);

const addFiveThenMulThree =
  compose(mulThree, sumFive);

We can now recall the Curry-Howard isomorphism and try to define a type and a program (proof) for the proposition (𝐴 × 𝐵 → 𝐶) ≅ (𝐴 → (𝐵 → 𝐶)):

// =>
type Curry = <A, B, C>(f: (a: A, b: B) => C)
  => (a: A)
  => (b: B)
  => C;
const curry: Curry = f => a => b => f(a, b);

// <=
type Uncurry = <A, B, C>(
  f: (a: A) => (b: B) => C
) => (a: A, b: B) => C;
const uncurry: Uncurry = f => (a, b) => f(a)(b);

Algebraic Data Types and Logical Structure

We have previously examined the correspondence between a function type 𝐴 → 𝐵 and the logical implication “if 𝐴 holds, then 𝐵 holds”. For instance, in typescript:

type BoolToNumber = (b: boolean) => number;
const f: BoolToNumber = (b) => b ? 1 : 0;

• f is the term
• BoolToNumber is the type corresponding to the proposition (𝐴 → 𝐵)
• Logical interpretation: “given a boolean value, I can produce a number”
• The function itself serves as a constructive proof of the proposition

The Curry-Howard correspondence, however, extends beyond the identification of function types with logical implication.
In typed functional languages, more structured types are built by combining simpler ones. These are known as Algebraic Data Types (ADTs): types formed by products (pairing values together) and sums (values that may be of one type or another). ADTs provide a natural framework for representing structured data in a way that mirrors logical reasoning.
We can summarize the correspondence between types and logical connectives as follows:

logic	description	typescript example
𝐴 ∧ 𝐵	product type (𝐴 × 𝐵)	[a, b]: [A, B]
𝐴 ∨ 𝐵	sum type (𝐴 + 𝐵)	type Boolean = 'True' | 'False'
⊤	unit type 1	type Unit = {} (unit-like)
⊥	empty type 0	never
𝐴 → 𝐵	function type (𝐴 → 𝐵)	(a: A) => B

Constructing a value of a product type corresponds to proving both 𝐴 and 𝐵; constructing a value of a sum type corresponds to proving either 𝐴 or 𝐵, together with evidence of which alternative holds. Types that correspond to inconsistent propositions are uninhabitable, reflecting the impossibility of proving a contradiction.
A simple and illustrative ADT is the list type:

type ConsList<T> = null | [T, ConsList<T>];

• null represents the empty list (the unit type 1)
• [T, ConsList<T>] (head and tail) represents a value paired with a recursive list (T × ConsList<T>)

A function that operates on such a list performs case analysis, which is the constructive analogue of logical elimination:

const len = <T,>(list: ConsList<T>): number => {
  if (list == null) {
    return 0;
  }
  const [_, xs] = list;
  return 1 + len(xs);
}

Here, len is the term inhabiting the type (ConsList<T> → number) and the conditional ensures that all cases of the ADT are addressed, just as a logical elimination rule guarantees that no possibilities are omitted. Constructing len is therefore a constructive proof that a length can be computed for any list.
Beyond this operational view, ADTs are not merely convenient data structures but inductively defined types.
Their constructors specify how values are generated and from this generative structure their elimination principles follow necessarily.
For a type such as finite lists, defined by the constructors “null” and “cons”, any total function over lists must proceed by structural recursion. This is not a programming convention but a logical consequence of the type’s inductive definition.
This structural principle can be stated more formally.
The list type can be defined inductively as the minimal solution of the type equation ConsList(𝑇) ≅ 1 + 𝑇 × ConsList(𝑇), where:

• 1 represents the empty list (null)
• 𝑇 × ConsList(𝑇) represents a head element paired with a recursive list (cons)

Given this inductive definition, defining a total function on lists 𝑓: ConsList(𝑇) → 𝑅 is necessary and sufficient to specify:

• a value of type 𝑅 for the empty list case
• a function (𝑇 × 𝑅) → 𝑅 describing how to combine a head element with the result of recursively processing the tail

This universal elimination principle is commonly expressed by the fold function. Formally, fold has the signature:

fold: 𝑅 × (𝑇 × 𝑅 → 𝑅) → (ConsList(𝑇) → 𝑅)

const fold = <T, R>(
  onNil: R,
  onCons: (x: T, xs: R) => R
) => (list: ConsList<T>): R => {
  if (list == null) {
    return onNil;
  }
  const [x, xs] = list;
  return onCons(x, fold(onNil, onCons)(xs));
};

Under this formulation, defining a total function on lists amounts precisely to specifying how to interpret the two constructors of the type. The fold is therefore not merely a programming convenience, but the canonical elimination principle induced by the inductive structure of the type.
For example, the len function can be defined canonically using the fold principle as:

len = fold(0, (𝑥,𝑛) ↦ 1 + 𝑛)

const len = <T,>(list: ConsList<T>): number =>
  fold(0, (_, n) => 1 + n)(list);

The existence and uniqueness of such a construction follow directly from the inductive definition of the list type. Operationally, this corresponds to structural recursion; logically, it corresponds to induction.

Conclusions

If functional programming is interpreted merely as a programming paradigm, its virtues remain methodological.
If, however, it is understood as a conservative extension of the typed λ-calculus enriched with algebraic data types, its properties acquire a formal status.
In such a system, program construction coincides with proof construction. The shape of data mirrors the shape of logical propositions; the structure of evaluation mirrors normalization in proof theory. Correctness is not appended to programs through external verification but arises from the constraints of the system itself.
Functional programming, under this interpretation, is therefore not defined by stylistic commitments but by structural ones. Its distinctive contribution lies in aligning computation with formal reasoning, such that writing a program amounts, in a precise sense, to constructing a proof.
The elimination principles examined in this work - in particular the fold function over inductively defined types - point towards a deeper mathematical structure. The existence and uniqueness of such constructions are not incidental properties of lists, but instances of a more general phenomenon: in the language of category theory, they arise as catamorphisms over initial F-algebras. Under this generalization, the structural recursion principles derived here are subsumed by a uniform theory of inductive types and their canonical eliminators. This connection, and its implications for the foundations of typed functional programming, will be the subject of a subsequent work.

Bibliography

• Benjamin C. Pierce (2002), Types and Programming Languages (MIT Press)
• Philip Wadler (2014), Propositions as Types (University of Edinburgh)
• Robin Milner, Robert Harper, David MacQueen, Mads Tofte (1997), The Definition of Standard ML (MIT Press)

Written by