Functional Programming is a different perspective, the unique way of thinking about programs and visualizing structure of a program.
It is based on the black-box abstraction, which means a habit of concealing all the irrelevant little details and keep focused on an appropriate level of abstraction. This allows us to zoom vertically to the lower layers and up when necessary.
On each level there are connected black-boxes, each of which takes a well-defined input and produce well-specified output. This is a horizontal dimension - you can visualize an execution of a program as a propagation of a signal.
Those black-boxes behave as a mathematical function - it gives the same output for the same input. Always.
The whole program could be viewed as a function composition (like a music), where output of one function becomes an input to another, without any intermediate internal state variables.
Thus we have the layers of abstractions with well-defined boundaries, black-boxes (functions) with well-defined behavior and connections, which are applications of functions to its arguments.
Together function composition (output of f() is an input for g(), and so on) forms a function pipeline, with separate stages, which could be comprehended and modified independently, as long as conventions and interfaces remain unchanged. It is almost like an electric scheme. Several concepts were put together to make the whole filed of Electrical Engineering. This is where Scheme languages comes from.
This is a perspective we take on a software development. This is what Functional Programming is really. (and it has nothing to do with Haskell)).
SICP - the great book - gives an in-depth discussion of this approach. It is the only one book you need to become a software engineer (nothing to do with "learn xxx the hard way"). There are several courses based on this book.
Types are propositions, functions are proofs
The proof of an implication
B → A is a function, which takes a proof of the antecedent
B (a value from a nested function) into a proof of the consequent
The function that proves
B → A is applied to the proof of
B to yield a proof of
Introduction + elimination (reduction) is a transition - a step further, preserving the
This is formal logic.
The reduction rule for functions applies when a
lambda term introduces a function, which is immediately eliminated by an application (
Similarly, the reduction rules for
Pairs apply when a constructor (
CONS introduces a
Pair, which is immediately eliminated by a selector (
There is nothing extra in it.
Start from the types, and the terms and reductions follow. The terms follow as introducers (
define and eliminators (
apply) for the type, and the reductions follow when an introducer meets an eliminator (
eval which calls
apply), and type safety follows by showing that each of the reduction rules preserves type derivations.
* are generalized to an abstract notion called
transformation of values (mapping) is generalized into a
Applicative Functor is a transformation (a mapping) that could be applied to a value
Monad is an abstraction which generalizes a transition (a step) - a transition from one state to the next.
Maybe Monad or
Either Monad are forks - a transition to one of the two possible states (outcomes).