Functional Programming and Programming-Language Semantics

Lambda calculus supplied a compact theory of functions. Turning related ideas into programming languages required decisions about data, evaluation, recursion, types, and interaction with a machine.

The history is therefore more than a sequence of languages inspired by Church. It includes a sustained attempt to explain what programs mean and which transformations preserve their behavior.

Lisp and symbolic computation

John McCarthy's 1960 paper, “Recursive Functions of Symbolic Expressions and Their Computation by Machine”, presented a foundation for Lisp.

Lists and symbolic expressions made programs suitable for manipulating formulas and other structured data. Function definitions, conditionals, and recursion supported an expressive style of symbolic computation.

The relationship between programs and data was especially significant. An evaluator could itself be described within the symbolic framework, connecting an implemented language with the earlier mathematical idea of a universal computation.

Lisp should not be identified without qualification with pure lambda calculus. Its implementations and dialects included choices about variable binding, mutation, evaluation, and other operations. Those choices affect equational reasoning about programs.

The relevant historical contribution is the construction of a practical language for symbolic procedures, with a clear mathematical vocabulary for recursive definitions.

Landin and the analysis of language

Peter Landin investigated how programming-language constructs could be understood through lambda calculus and abstract machines. His 1964 work on the mechanical evaluation of expressions introduced the SECD machine; his 1966 “The Next 700 Programming Languages” articulated a language-design program centered on a small semantic core.

An abstract machine specifies states and transitions at a level between mathematical expressions and physical hardware. It can make evaluation order, environments, and control explicit.

This matters because substitution on paper and execution in an implementation need not look the same. A machine may use environments to associate variables with values instead of copying expressions textually.

An adequate semantics explains why such implementation choices realize the intended computation.

Operational and denotational accounts

An operational semantics describes evaluation through rules or machine transitions. A denotational semantics assigns mathematical meanings to expressions compositionally.

For the recursive function

an operational calculation gives

The rule explains how execution unfolds on this input. A denotational account asks which mathematical object represents the entire recursive definition, including behavior on inputs where other definitions might fail to terminate.

Dana Scott and Christopher Strachey's work around the end of the 1960s and the early 1970s developed influential foundations for such meanings.

Recursion as a least fixed point

Let a partial function represent a computation that may be undefined on some inputs. Write $\bot$ for absence of a result.

The factorial equation determines an operation $F$ on candidate partial functions:

A solution is a fixed point $g=F(g)$.

Begin with the everywhere-undefined function $g_0$. Applying $F$ once gives a function defined at $0$. Applying it again also supplies the result at $1$, and further iterations extend the available information.

For this example, the limit of the chain supplies every factorial value. In suitable ordered domains, continuous operations have least fixed points obtained from such increasing approximations.

“Least” refers to the information order. The interpretation includes exactly the information justified by finite unfoldings of the definition, rather than arbitrarily choosing among possible mathematical solutions.

This approach also handles definitions that remain partial. Denotational semantics does not prove that every recursive program terminates; it provides a way to give divergence a systematic mathematical treatment.

ML and inference of types

ML originated as a metalanguage for the LCF theorem-proving project. Its users needed a practical language for composing proof procedures while preserving the discipline of the underlying theorem system.

Roger Hindley's 1969 work on principal type schemes, Robin Milner's 1978 account of type polymorphism, and Luis Damas and Milner's 1982 paper established central results behind the familiar Hindley–Milner tradition.

A principal type scheme is sufficiently general that other permitted types of the expression arise as instances. An inference algorithm seeks that general scheme rather than requiring the programmer to annotate every occurrence.

Consider

Assign $x$ a type $\alpha$. Because $g$ is applied to $x$, let $g:\alpha\to\beta$. Because $f$ is applied to the result, let $f:\beta\to\gamma$. The whole expression then has type

Generalizing the unconstrained type variables yields a polymorphic scheme. The same composition function can be instantiated for many concrete types.

The Damas–Milner paper proves the relevant principal-type result for its specified language. Extensions involving effects, higher-rank polymorphism, or other mechanisms require separate rules and qualifications.

Polymorphism and its limits

System F, developed independently by Girard and Reynolds, expresses polymorphism through explicit quantification over types. Its expressive power exceeds ordinary Hindley–Milner let-polymorphism.

One should therefore distinguish the existence of a polymorphic language from the decidability and practicality of inferring its types. A result for a restricted inference discipline does not automatically extend to a richer calculus.

Reynolds's 1983 work on relational parametricity studied uniform behavior across type instantiations. A polymorphic term cannot arbitrarily inspect a type parameter when the language supplies no operation for doing so.

For example, in a pure total setting, a term of type

has no source for an arbitrary output of type $\alpha$ except its input. Under the relevant parametricity assumptions, it behaves as the identity.

General recursion, exceptions, runtime type analysis, and other language features complicate that conclusion. A divergent term can inhabit a programming-language type without returning its argument. The theorem must match the actual language.

Evaluation strategy is part of meaning

Consider a function that ignores its argument and returns zero, applied to a divergent computation.

A call-by-value language evaluates the argument first and may diverge. A call-by-name or suitable lazy evaluation strategy can return zero without evaluating that argument.

Thus the mathematical-looking equation “the function always returns zero” needs an account of how application evaluates. Equational laws valid in a total calculus may need refinement in a language with partiality and effects.

Haskell's design, begun by a committee in 1987, combined non-strict evaluation with a shared functional-language framework. Type classes and later approaches to organizing effects became important parts of its identity.

The history written by Hudak, Hughes, Peyton Jones, and Wadler presents a collaborative design process, rather than attributing the language to one inventor or treating it as a direct transcription of a logical calculus.

A continuing exchange with logic

Functional programming influenced the construction of proof assistants, and proof-assistant requirements influenced functional languages. Semantics supplied tools for compiler transformations, reasoning about equivalence, and understanding abstraction boundaries.

The exchange was productive precisely because its distinctions remained visible. A type can prevent some erroneous operations without proving termination. A denotation can describe partial behavior without declaring it desirable. A program can manipulate proof objects without itself being a proof of every property it computes about.

The next development asks how programs can search for mathematical proofs automatically.

Sources and further reading

• John McCarthy, “Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I” (1960).
• Peter J. Landin, “The Mechanical Evaluation of Expressions” (1964); “The Next 700 Programming Languages” (1966).
• Dana Scott and Christopher Strachey, Toward a Mathematical Semantics for Computer Languages (1971).
• J. Roger Hindley, “The Principal Type-Scheme of an Object in Combinatory Logic” (1969); Robin Milner, “A Theory of Type Polymorphism in Programming” (1978).
• Luis Damas and Robin Milner, “Principal Type-Schemes for Functional Programs” (1982).
• John C. Reynolds, “Types, Abstraction and Parametric Polymorphism” (1983).
• Paul Hudak, John Hughes, Simon Peyton Jones, and Philip Wadler, “A History of Haskell: Being Lazy with Class” (2007).