# Types are propositions, functions are proofs

In a pure functional languages based on *substitution*, such as Simply Typed Lambda Calculus, various systems of various Logic, or high level languages like Miranda or Haskell, *types could be viewed as propositions, while semantically correct pure functions (without side effects) define (or implement) actual proofs*.

Each sub-expression inside a pure function (which as a whole is one single expression) *has its own type*.

Nested functions corresponds to a program, which is a *single expression* too. (The result of evaluation of `main :: IO ()`

in Haskell is an expression to be evaluated (reduced to a value) by the runtime.

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* `A`

. **This**.

The function that proves `B → A`

is applied to the proof of `B`

to *yield a proof of* `A`

(which is a *value*).

Introduction + elimination (reduction) is a *transition* - a step further, preserving the `Truth`

.

This is the formal logic.

The reduction rule for functions applies when a `lambda`

term *introduces a function*, which is immediately eliminated by an *application* (`apply`

).

Similarly, the reduction rules for `Pair`

s apply when a *constructor* `CONS`

introduces a `Pair`

, which is immediately eliminated by a *selector* `CAR`

or `CDR`

.

There is nothing extra to 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 (inside `eval`

which calls `apply`

), and *type safety* follows by showing that each of the reduction rules *preserves type derivations*, which means the whole thing is *consistent* (without any contradiction).

This is what is called *well-typed, type-sage or fp-complete* - consistency guarantee.

Provided that *semantics* of each function (or proof) are correct, the whole program, then, is correct. The way *some* Math or Logic is correct.

**Note:**See TracWiki for help on using the wiki.