wiki:Haskell/Vedanta

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.

Last modified 2 months ago Last modified on Sep 25, 2020, 5:45:10 AM
Note: See TracWiki for help on using the wiki.