# Haskell Vedanta

A program is precise specification of a process, detailed-enough to be executed by an abstract machine.

An algorithm is a formalized (well-defined and precise) general procedure (a sequence of actions to perform), to be implemented in all sufficient and necessary details.

## Haskell

Haskell is pure Logic. Strongly-typed with type-classes and highly syntactically sugared, which is compiled to a intermediate language (MIR) which is also a language based on a *Simply-Typed Lambda Calculus*, which, in turn, is *evaluated by runtime as a type-checked state machine* - this is what the function `main`

produces (which is what a Haskell executable really is).

Not just that, all Haskell code, including MIR, could be evaluated by pure substitution -- by applying rewrite rules, (beta-reduction, inlining, etc.) exactly like Logic and Math, which, look at this:

*makes Haskell a pure high-order predicate logic, statically typed with type-classes, reducible to pure Lambda Calculus (as its implementation)*.

C++ is a joke compared to this and NodeJS is just bullshit.

## Purity

All Haskell expressions are pure, even when they describe impure actions to be performed eventually by mundane impure runtime.

The expression produced by the main function is a pure definition of a state-machine (an actual structure!) verified to be type-safe (have no contradictions) by the compiler.

Each function is pure because the *context* (or state) is always passed to it as a parameter, even *The Whole World* is passed in the case of IO (implementation, however, throws it away!).

From the mathematical point of view if you have the whole world as a parameter to a function which returns a value *together with a new version of the world, after causing some effect on it*, then, the function is indeed pure. *Same input - same output. Always*.

This is not a joke. Not just a beautiful metaphor. As long as all functions are pure *the substitution model of evaluation (as in Lambda Calculus, Logic and Mathematics) still holds*, so Haskell is still a pure higher-order logic - *Simply Typed Lambda Calculus extended with some additional evaluation rules, type-classes and decorated with some syntactic sugar*. Its MIT is exactly this.

One more time: Haskell code is *a Pure Logic*, not just theoretically but technically and operationally.

It all can, in principle, be evaluated with pen and pencil using substitution. Just like Maths.

## Monads

Haskell literally separates a pure functional code from impure by creating *an abstraction barrier* between pure and impure code by encapsulation such code into various Monads.

Separation (an abstraction barrier) is enforced at a type level. Functions below cannot access values (and functions) above.

The *contexts* could play very different roles, from holding algebraic data types, such as `Either`

or `Maybe`

, to encapsulations `State`

and `IO`

.

Being composed (which is what it is all about) Monads provide an implicit sequencing for a pure, lazy code, via nesting of functions -- `(.)`

and `(>>=)`

are merely nested lambdas.

Thus, Monads are fit to encapsulate `IO`

actions which imply serialization (sequencing).

End of the long and messy story.

## End of knowledge.

Technically, Haskell is a pure-functional language with lazy semantics which is statically (and, obviously, strongly) typed with type-classes. It is simplified into an intermediate language (representation), which is just *Simple-Typed Lambda Calculus extended with a few additional types, syntactic forms and evaluation rules*. Even more technically, it uses *System F Omega formalism* to implement High-order Logic.

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