IA014: Advanced Functional
Programming
Course information
1. History of λ-calculus
Jan Obdržálek obdrzalek@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
IA014 1. History 1
Course information
IA014 1. History 2
Course organization
Lectures
• Thursday, 12 noon, D2
• language: English
• slides will be available (IS)
Exam
• midterm exam (worth 15 % of the points)
• final exam (85 %)
• both written
• in English, but you may answer in Czech
• k and z completion possible
IA014 1. History 3
Prerequisites
• no formal requirements
• some experience with functional programming
• evaluation, recursion, abstract data types, pattern matching,
lists (including comprehensions), higher-order functions, . . .
• e.g. to the extent covered by
IB015 – Non-imperative programming
• you should be able to write simple functional programs
• you will have first few weeks to catch-up on FP, if you are
willing to work
• we will use mostly Haskell
• but if you know ML (OCaml, F#, . . . ) you should be fine
(see the recommended literature)
IA014 1. History 4
Topics covered
• history of λ-calculus (and functional programming)
• λ-calculus
• untyped λ-calculus
• simply typed λ-calculus
• polymorphic λ-calculus (system F)
• type inference (Hindley-Milner alg.)
• type system extensions
• type classes
• functors, monads
• monad transformers
• purely functional data structures
• concurrency
• applications
• DSL - Domain specific languages
• Quickcheck - type based property testing
• dependent types: Agda and Coq
IA014 1. History 5
Reading
• There is no book covering the whole course.
• Some topics cannot be found in any book at all.
• I will use various research papers (available in IS)
https://is.muni.cz/auth/el/1433/podzim2014/IA014/index.qwarp
some (more or less) general books
• B. O’Sullivan, J. Goerzen and D. Stewart: Real World Haskell
• M. Lipovaˇca: Learn You a Haskell for Great Good!
• G. Michaelson: An Introduction to Functional Programming
Through Lambda Calculus
• C. Okasaki: Purely Functional Data Sructures
• B. Pierce: Types and Programming Languages
IA014 1. History 6
Real World Haskell
http://book.realworldhaskell.org/
IA014 1. History 7
Learn You a Haskell
http://learnyouahaskell.com/
IA014 1. History 8
(Short) History of λ-calculus
(and functional programming)
Based on a talk “Church’s Coincidences” by Phil Wadler.
IA014 1. History 9
David Hilbert (1862-1943)
IA014 1. History 10
Entscheidungsproblem
Hilbert, 1928
Does there exists an algorithm with the following properties:
INPUT: formula φ of First Order logic
(+ finite number of extra axioms, e.g. Peano arithmetic)
OUTPUT: YES iff φ is true (universally valid)
• Many problems could then be automatically solved:
• Goldbach Conjecture
• Riemann Hypothesis
• Diophantine Equations (Hilbert’s 10th problem)
• . . .
• “Little detail”: what is meant by algorithm?
• We need a notion of effective computability
IA014 1. History 11
David Hilbert (1862-1943)
IA014 1. History 12
David Hilbert (1862-1943)
IA014 1. History 12
David Hilbert (1862-1943)
For the mathematician there is no Ignorabimus, and, in my
opinion, not at all for natural science either. . . . The true reason
why [no one] has succeeded in finding an unsolvable problem is,
in my opinion, that there is no unsolvable problem. In contrast to
the foolish Ignorabimus, our credo avers: We must know, We
shall know.
D. Hilbert
Königsberg, 8 September 1930
Society of German Scientists and Physicians
IA014 1. History 12
Kurt Gödel (1906-1978)
IA014 1. History 13
Kurt Gödel (1906-1978)
IA014 1. History 13
Gödel’s Incompleteness
Theorem
On Formally Undecidable Propositions of Principia Mathematica
and Related Systems I (1931)
For any consistent, effectively generated formal theory that
proves certain basic arithmetic truths, there is an arithmetical
statement that is true, but not provable in the theory.
Königsberg, 7 September 1930
Conference on Epistemology
held jointly with the meetings of Society of German Scientists and PhysiciansIA014 1. History 14
Alonzo Church (1903-1995)
IA014 1. History 15
A. Church – λ-calculus (1932)
. . .
. . .
IA014 1. History 16
λ-calculus (1932)
• formal system of mathematical logic
• based on function abstraction and application using
variable binding and substitution
• intended to be a foundation of mathematics
f(x) = x2
+ x + 42
⇓
f ≡ λx.x2
+ x + 42
Notation
Then Now
x x variable
λx[N] (λx.N) abstraction
{L}(M) (L M) application
IA014 1. History 17
λ-definability
By 1932, the following could be modelled by λ-calculus:
• natural numbers
• +1 (successor)
• addition, multiplication
• exponentiation
• . . . pretty much everything!
Problem!
• How to define the predecessor (-1) operation?
• If that would not be definable, then λ-calculus does not
capture the notion of effective computability!
• Solution: S. Kleene, 1932
IA014 1. History 18
Stephen Kleene (1909-1994)
IA014 1. History 19
S. Kleene – predecessor (1932)
IA014 1. History 20
λ-calculus – Undecidability
(1936)
1935 – Kleene and Rosser showed λ-calculus to be inconsistent
1936 – Church publishes the computational part (numerals etc.)
. . .
First undecidable problem: equivalence of two λ-terms
IA014 1. History 21
λ-calculus – Consistency (1936)
. . .
. . .
Proof that β-reduction is confluent.
IA014 1. History 22
Effective Computability Models
• Alonzo Church: Lambda calculus
An unsolvable problem of elementary number theory (Abstract)
Bulletin the American Mathematical Society, May 1935
Two other notions defined independently:
• Stephen C. Kleene: Recursive functions
General recursive functions of natural numbers (Abstract)
Bulletin the American Mathematical Society, July 1935
• Alan M. Turing: Turing machines
On computable numbers, with an application to the
Entscheidungsproblem
Proceedings of the London Mathematical Society, received 25 May
1936
IA014 1. History 23
Alan Turing (1912-1954)
IA014 1. History 24
A.Turing – Equivalence (1937)
· · ·
IA014 1. History 25
Typed λ-calculi (λ →)
Two flavors
• Implicitly typed
• Haskell B. Curry, 1934
• I = (λx.x) : A → A
• I = (λx.x) : (A → B) → (A → B)
• Explicitly typed
• Alonzo Church, 1940
• IA = (λx:A.x) : A → A
• IA→B = (λx:(A→ B).x) : (A → B) → (A → B)
Later developments
• Higher-order λ-calculi
• Girard, 1972
• system F, system Fω
IA014 1. History 26
Models for λ-calculus
Is there is set theoretic model for λ-calculus?
Naturally, we would need a set D isomorphic to the function
space D → D.
Problem: D and D → D have different cardinality!
Solution: D. Scott 1969
• model D∞
• consider only continuous functions with appropriate
topology
model in cartesian closed category of complete lattices and Scott continuous functions
• then such domain D can be found
Led to the development of denotational semantics.
IA014 1. History 27
Functional programming timeline
• Lisp (McCarthy, 1960)
• Iswim (Landin, 1966)
• Scheme (Steele and Sussman, 1975)
• ML (Milner, Gordon, Wadsworth, 1979)
• Miranda (Turner, 1985)
• Haskell (Hudak, Peyton Jones, Wadler, 1987)
• OCaml (Leroy, 1996)
• Erlang (Armstrong, Virding, Williams, 1996)
• Scala (Odersky, 2004)
• F# (Syme, 2006)
IA014 1. History 28
LISP (1958)
First functional programming language
LISt Processing
Lots of Irritating Superfluous Parentheses
• John McCarthy (MIT)
• eager evaluation
• impure features
• assignment
• dynamic binding (confusion between local and global
variables)
• Quote operator
• fixed-point operator LABEL (implemented as cycle)
IA014 1. History 29
ML (1973)
First important typed FL
• Robin Milner (University of Edinburgh)
• eager evaluation
• implicit typing (Curry style)
• types are automatically derived (Hindley-Milner alg.)
• type-safe exception handling
• impure (assignments)
main additions to λ →
• new primitives
• fixed point combinator Y
• arithmetic operators
• ’let’ construction
let x be N in M end.
IA014 1. History 30
Robin Milner (1934-2010)
IA014 1. History 31
Haskell (1990)
Being Lazy with Class
• designed by committee (P. Hudak, J. Hughes, S. Peyton
Jones, P. Wadler, . . . )
• lazy evaluation (non-strict)
• parametric type polymorphism (System F)
• purely functional
• type classes
• side-effects through monads
IA014 1. History 32
Where can you find FP
languages?
• telecommunications: Erlang – Ericsson
• banking: Credit Suisse (F#), ABN (Haskell), Bank of
America (Haskell)
• insurance: Grange Insurance (F#)
• web applications: Facebook (OCaml))
• verification: SLAM – Microsoft, ASTRÉE – Inria (both
OCaml)
• user applications: Unison (OCaml)
• mathematical libraries: FFTW (OCaml)
• automated theorem proving: Coq (OCaml)
• development tools: Darcs (Haskell)
IA014 1. History 33
Functional features in imperative
languages
• anonymous functions
(JavaScript, Python, Ruby, C#)
• (some) higher-order functions
(e.g. Python: filter, map)
map(lambda x: x ** 3, [2, 4, 6, 8])
• partial function application (Python)
add5 = partial (add, 5)
add5(15)
• lists (Python, C#, . . . ),
list comprehensions (Python)
• ( type derivation (C# 3.0, C++11, Visual Basic 9.0) )
IA014 1. History 34
Reading list
J. Hughes: Why Functional Programming Matters
H. Barendregt: The impact of the lambda calculus
in logic and computer science
Cardone, Hindley: History of Lambda-calculus and Combinatory
Logic
IA014 1. History 35