Monadic Vedanta

The confusion and frustration come from a lack of clear separation between interfaces and implementation.

A pure function could

• take an extra argument (usually a context)
• return an extra argument (usually a modified state)

Abstractly or conceptually, these extras could be separated and completely hidden by an abstraction barrier.

These abstractions should be composable, just like ordinary functions \[g \circ f = g(f(x))\]

g . f = \x -> g (f x)

Just like ordinary functions, these abstractions can be Functoral

instance Functor ((->) r) where
  fmap = (.)

So a Functor is required and the type-class Monad is a subclass of a Applicative, which is a special kind of Functor.

class Applicative m => Monad m where
  (>>=)       :: forall a b. m a -> (a -> m b) -> m b
  return      :: forall a. a -> m a
  return      = pure

These, however, are Haskellisms - fancies of library writers. Applicative is NOT required at all.

Moreover, implementations of Functor instances break an abstraction (makes it leaky) by “looking at and manipulating the guts”, which is a violation of the abstraction principle.

In the context of a List

xs >>= f = concat (map f xs)
return x = [x]

were f must use return and have the type f : a -> m b

And, of course, List is a “classic” Functor

instance Functor [a] where
  fmap = map

For other, arbitrary instances there is join

join :: Monad m => m (m a) -> m a

which is structurally just like concat for Lists

concat :: Foldable t => t [a] -> [a]

Life Itself has been evolved upon certain molecular structures, which are made out of Atoms. Life does not know anything about their nature, it is just using them as given.

If it could make any assumptions, that would be, as we assume, that they are indivisible and indestructible, and some particular molecular structures such as aminoacids or RNAs are immutable.

The fact that atoms can actually be broken in certain conditions (created by humans on this planet) is irrelevant, because in the actual environment in which Life has been evolved such conditions do not arise.

What we have here is a very real, not imaginary, abstraction barrier, so real an actual, that literally everything within you and around you is made upon it.

And this is the Reality First Principle for functional programming - atomicity and immutability of base structures, which is only apparent.

At a highest, most abstract level a Monad in Haskell is a generalization of an abstraction barrier similar to that one which holds Life Itself.

Functions on Monadic Values (of a particular type) are as pure as mathematical functions (could be calculated by pure substitution with pen an paper), referential transparency is preserved.

What is going on inside these values is beyond the abstraction barrier and literally cannot be seen by pure Haskell code (the code only declare what to do with these values, including pattern matching on value’s structure).

These are the same notions (of an impenetrable abstraction barrier), and it is not “abstract” or imaginary. Everything is real.

The (>>=) function (called bind) which does re-binding and sequencing should be considered impure, because it (and only it) has access to the internal state and actual representations.

However, the code that uses (>>=) is as pure as math or logic.

The type system guarantees that no code could “see” or access any value behind the monad interface (abstraction barrier). (>>=) and only (>>=) can access and pattern-match (but not “see”, because Haskell is declarative.).

This is exactly how Haskell code is pure (as math or logic) in the presence of IO, State transformation and side-effects. All these are beyond the abstraction barrier with the Monad type-class establishes, and the type system enforses.

Each instance of a Monad (an actual type) hides all its “stuff” behind a standardized interface, which separates the pure code from impure.

And that is really it. No more, no less.

This metaphor is both philosophically funny and useful. In an abstract theory, a function is indeed pure if it takes a snapshot of the whole universe and returns a value together with the whole universe modified by itself.

In reality this is a form of an explicit serialization (via nesting of calls and explicit passing of a value - nested lets, which are semantically equivalent to nested lambdas) which is required for sequencing of IO actions, since Haskell is a call-by-need language.

Nested function calls and implicit passing of a values inside a Monadic context (behind the abstraction barrier) is the most common idiom.

Nesting of expressions is the natural way to establish an evaluation order in a language with lazy semantics.

Passing of “RealWorld” values ensures “threading”- than no two IO contexts ever overlap.

IO is a type synonym defined in the following way:

type IO a  =  RealWorld -> (a, RealWorld)

Technically, it is an ADT as defined by Barbara Liskov. There is an interface, which is what the pure code “sees” and uses. There is an actual implementation, based on some particular representation (actual data structure) hidden behind the interface, exactly as intended.

All the most fundamental concepts of programming are there in play.

At the lowest level there is an impure code which manipulates data in memory, like everything else.

The purity ends when the main function of a Haskell program returns a pure expression (to be eventually evaluated by the runtime), which is a type-checked specialized state machine, defined in pure logic.

It is just a lambda which returns a pair of values. Lambda, so that they can be composed sequentially (yes, just nested lambdas) by >>=.

The two values of a pair are at the different sides of an abstraction barrier. The State cannot be seen or accessed outside of the Monad.

The lambda (which is called a State Transformer) captures the value, and it is lifted into this particular Monadic context “forever”.

The actual State type and how exactly the values of that type are actually handled is encapsulated inside a particular instance of a Monad type-class and it does not pollute the pure code.

Moreover, the code is still declarative and will be evaluated eventually, so it is literally a pure logical expression which declares what is to be done with Monadic values. Referential transparency still holds.