The Whys
The Foundations
The right understanding (and the proper knowledge) begins with very strange questions, which most people would never ask.
Following the purely theoretical (but absolutely fundamental) result of Alonzo Church, that his Lambda Calculus is a universal language – absolutely minimal but yet good enough to compute any commutable mathematical function, the question is – Why? Why just these three forms are enough for everything. This is not an easy question to approach.
Lambda Calculus
In its canonical form the whole calculi consist of a set of terms, and a set of reduction rules.
It has just 3 syntactic forms:
- a variable binding (a convenience for the Mind)
- a \[\Lambda\]-abstraction (a capture)
- an application (a single step)
and just 1 reduction rule:
- \[\beta\]-reduction (a uniform substation of a value for a bound variable)
There are a few often overlooked subtleties here:
- there is an implicit environment, which remembers the immutable bindings
- there is the substitution model, which is implicitly used in all mathematics
- there is an interpreter (which uses the substitution model), and this is you
- the process of reduction (simplification) stops when a normal form is reached
Currying is an extension for uniformly implementing a multi-argument functions.
Partial application “naturally follows”.
The Universal Machine
The crucial part of the Classic MIT Culture is recognition (and subsequent studying) of an interpreter as a Universal Machine.
Generalized patterns of What Is.
Now why. The way to at least some answers is not toward abstract concepts, but towards molecular and biological processes from which some fundamental abstractions have been captured and properly generalized.
An Environment
The environment is a membrane-separated distinct partition of a single cell, which, in turn, has an enclosing environment.
A Closure
This gives us both nesting of environments (and nesting in general) and a “closure” (a distinct partition) which “captures” (holds) all its “stuff” inside.
A Universal Pattern
These closures are not just physical, but also “logical” and “mathematical” patterns. It is, thus, a Universal Pattern, indeed, the most general and the most fundamental one – the pattern of capturing something distinct within an environment.
At all levels
We have an environment of a shared (agreed upon) concepts, expressed in a shared (common) human language.
A definition captures the meaning. A concept captures a generalized notion, etc.
Again, distinct “closures” (partitions) within some environment. It becomes an environment for its “internals”.
The definitive property of a “closure” is that everything necessary (being used inside) is captured (held) within. Ideally, it has to be eternal (indestructible).
The Lambda-abstraction
And this is, of course, what the Lambda-abstraction corresponds to – what notion it, as a minimal abstraction, captures.
A single step
What universal notion the application of lambda terms (to one another) captures? It captures the notion of creating a process, which performs at least one single step.
Again, application implicitly creates a process which performs at least one single step. This is corresponds to an enzyme within a cell.
Even more generally, to a simple chemical reaction, when a single required condition has been meet (a process notion).
At the level of the Mind we have a single step of reasoning (deductive or inductive), and the process in implicit withing the brain.
Cool, isn’t it? This is why the Curry-Howard isomorphism is possible - there are the same fundamental notions being captured by “different observers”.
Abstraction by parameterization
There is another connection, this time to the Barbara Liskov’s fundamental notion of abstraction by parameterization.
Closures which capture and do noting are useless, so would be any biological cell which has no “pumps” or “portals” to its environment.
The notion that the Lambda Abstraction is parameterized by a “variable” is crucial and fundamental. There is nothing redundant or unimportant in the Lambda Calculus.
The fact that the Lambda Abstraction is parameterized is a properly captured generalization of the universal pattern.
To be precise - an arity-one mathematical function is such proper generalized abstraction.
Any “multi-argument” functions are just a nesting of lambdas. This, as we will see, is another captured pattern.
An arrow between two dots
The pattern
Currying, when we look at what it actually does is just lambdas return another lambdas (which has to be called properly).
There is a curried '+ with an in-place invocation
(((lambda (x) (lambda (y) (+ x y))) 2) 3)
The fundamental part is that the only way to implement a composition of functions in a Normal Order (lazy) language is also via nesting of lambdas, which produces an implicit order of evaluation - the inner lambda will be first.
(define compose (lambda (g) (lambda (f) (lambda (x) (g (f x))))))
or in the another classic language:
g . f = \x -> g (f x)
The subtlety is, again, that in a Normal Order (as intended by God, or at least by Church, you know) nesting of lambdas is the only way to establish a sequential order – so the evaluator (the interpreter), which follows the same fixed set of rules, will “serialize” without “knowing about it” or any explicit support for serialization.
This is not a coincidence. This subtle pattern is just emerged or discovered by us.
At a type level what we see is chaining, and it is not a coincidence that we see some chained arrows up there. This is the pattern.
The aha-moment
The “thing” to realize is not just that the Lambda Calculus has everything that is required for computing every commutable mathematical function, but that the notions and patterns involved are not arbitrary or incidental.
The notions and the patterns (captured) have the deep connections to the universal patterns which “enable” (make possible) Life Itself, at the level of molecular biology.
Higher-level patterns
There are the same universal patterns at any level. They has been captured and generalized without the right understanding.
Function closures as cells or enzymes
At the “most primitive” level we have individual lambdas – the basic means of abstraction. They ought to behave as mathematical functions.
Biological enzymes not accidentally, behave as pure functions.
Functions have parameters, which act as the simplest interface (a “pump”).
ADTs as cells or enzymes
A the level of abstract interfaces we have the very same enzyme pattern. The requirements that the interface has to be abstract, and the abstractions to be non-leaking (as by B. Liskov) are not arbitrary, but necessary and sufficient.
Notice that generalizing of interfaces (types) is done by parameterization, which, again, is a universal pattern. Specialization is supplying the actual parameters, which is related to the Causality itself.
Modules as cells or enzymes
At the level of proper modules we have the same patterns - closures, parameterization and even application of one to another, as in SML or Ocaml.
The type level
At the level of types we have, not surprisingly, the same “building blocks” of the Lambda Calculus all over again. Most type systems, however, do not allow type-level lambdas and its application because it is too general.
It has been discovered that unrestricted applying anything to anything else is way “too abstract” and lead to paradoxes, so the Simple Typed Lambda Calculus has been created (and then the Hindley-Milter type system).
In other words, restrictions (constraints) are necessary, which, again, molecular biology has shown us.
Abstraction barriers
Abstraction barriers are very real. This is what atoms are to the molecules upon which Life Itself has been evolved.
Monads
A Monad captures a generalized abstract pattern. This abstract pattern can be viewed as a generalization of composable computations (just like function composition) which cross of an /abstraction barrier.
It required to form a Monoid with respect to >>= – the operation of composition (which
crosses an abstraction barrier). This is not arbitrary and related to the how a
proper composition (of functions) is possible.
It is implemented,not surprisingly, in the only possible way, as nested lambdas (which the implicit serialization property). Yes, the same fundamental pattern again.
Technically, a Monad is just an ADT (Liskov), defined as a type-class (Wadler), which means a Set of required to implement interfaces (duck-typng) and a sub-type relation to another type-class, which is, again, just a required set of interfaces.
Algebraic types
The universality here captured by the notion of a “sum” and “product” types, which is actually misleading .
The proper notion is that two distinct “values” could be either “both presented
in the same locality” – one AND another“ (,), or only one OR another (|) can
be preset – they are alternatives to each another (alternative distinct possibilities).
Do you see the | as a barrier or a partition there?
These structured types can be nested (yes, yes) so it could be a sum of products, or a product of sums. There is a regularity emerges.
Pattern-matching
It has been discovered that we could “naturally” we could pattern-match /on data constructors of algebraic data types, and the shape of the code would match the shape of the data type.
Pattern-matching itself is a universal notion. What we would call a structural pattern-recognition is how molecular biology works (no, there is no notion of a number at that level).
The encoding of Natural Numbers and the implementation of arithmetic within the Lambda Calculus uses a rudimentary pattern-matching (on the representation of Nats). I am Jack’s total lack of surprise.
At the Type-level
Can the types be generalized (as captured repeated patterns) and then parameterized? Why not.
Can we parameterize by whole type-classes (use the duck-typing)? Absolutely.
Yes, the same universal building blocks of the Lambda Calculus at the type level.
The message to take home
The “building blocks” The Simply Typed Lambda Calculus are universal abstractions, which, in turn, are properly captured emergent universal patterns in What Is.
The languages which just augment, extend and syntactically sugar the Lambda Calculus (the pure subset of Scheme, Miranda, Haskell, Coq) are doing the right thing.
Haskell managed to retain the purity of the Lambda Calculus and still can be evaluated using the substitution model (or with a pen and paper), so it has all the properties of pure logic or maths (which follow form ensuring unbroken the Referential Transparency property, which is an operational definition of “purity”).
The actual message is that the proper abstractions can be traced back, through the captured recurring (reemerging) patterns, back to What Is.