wiki:FunctionalProgramming/Monad

Monad

Maybe is merely an Algebraic Data Type (Either of type AKA Sum type).

To be of the Maybe type is to be Either Nothing or Just something - data Maybe a = Nothing | Just a

Maybe Monad is a data type together with implementation of two function.

To be a Monad is to implement return :: a -> m a and (>>=) :: m a -> (a -> m b) -> m b

List is just a recursive Algebraic Data Type

A List is Either Empty or a List of something - data [] a = [] | a : [a]

List Monad is a List type and implementation of return and >>=

To be a Monad is to implement return :: a -> m a and (>>=) :: m a -> (a -> m b) -> m b

...

Just this, a Type and an Interface together. Type itself is not a Monad!. Interface itself is not a Monad. The type-class (type-trait) which includes an interface and type-constructors is.

The interface implements explicit strongly-typed transition for a lazy language, which is implicit in a eager languages and corresponds to ;. In a context of a strict (non-lazy) language this interface is an unnecessary wrapping, similar to if x then True else False.

Fucking this and only this.

An abstract view - a high-order type, a super-type

merely a generalized (and well-defined) super-category - a nested type (a super-type) which must satisfy certain composition laws - usually termed (wrongly) as a higher-level abstraction.

Nothing to see here.

Precisely

A Monad is a second-order (higher-order) type. A type of types. A type-tagged type. Literally.

It forms a type-class with a type-constructor, applying (instantiation) of which to a type produces a new type.

Thus, a value bound to the symbol x of type a is just the type-tag a attached to the symbol x in so-called static environment.

A value of the type m a is a type-tag a, type-tagged with additional tag m. So, m a are nothing, but two nested types - m of a.

Just this.

M >>= λx.N

  • M is an expression of type m a
  • N is an expression of type m b, which could be the same type as m a or different
  • x is a value of type a (the extra type-tag m has been stripped off).
  • λx.N is a lambda which has type a -> m b (x to be substituted with an actual value in the body of N)
  • the type of whole thing is m b

λx.N is semantically equivalent to

(\x -> N) M

which in turn is equivalent to

let a = M in N

Both lambda and let introduce a local binding, and semantically, let is an implicit lambda plus invocation.

(let ((x 2)) (+ 1 x))

is

((lambda (x) (+ 1 x)) 2)

So far, there is nothing but wrapping and unwrapping of values. Remove a type-tag, evaluate an expression, attach a type-tag to the value being returned.

No more, no less.

Nested lambdas

Nested lets are nested lambdas

(let ((a 1)
      (b 2))
     (+ a b))

is semantically equivalent to

(((lambda (a) (lambda (b) (+ a b))) 1) 2)

which is just a curried procedure

(fn a => fn b => a+b) 1 2

or

let val a = 1
in
   let val b = 2
       in
         a + b
   end
end

Nothing more than nested lambdas.

Composition

for composition to work we need associativity or laws

What it takes to be a Monad

To be a Monad is to implement at least two functions - return and >>= with certain signatures with follow the protocol (monadic laws) to ensure composability.

return :: a -> m a

and

(>>=) :: m a -> (a -> m b) -> m b
infixl 1 >>=

respectively.

Why?

Monadic code is generic, so it could be evaluated no matter which particular instance of monad is given. The "details" are encapsulated inside (>=) - "compose", and >> - "chain".

No more, no less. Too explicit wrapping and composition.

Algebraic Data Types type-tagged as a Monad

This is what it is for. Sum Types (disjoint unions) and Product Types (structured data) could be wrapped in a Monad.

State modeled as a Tuple

A state being passed explicitly through function composition (as a parameter) is "safe".

Nesting as the way to Establish Order Of Evaluation

Sequential function composition (f . g . h) x could be viewed as an instance of Monad, however it is already completely or totally defined using nesting f(g(h(x))), which implies the notion of an Order Of Evaluation - (h(x) to be evaluated first) in a lazy language.

There is no surprise that monadic composition (using >>= or >> and so called do-notation) is desugared into a bunch of nested lambdas. This is precisely what a monadic composition is - wrapped (tagged with an extra type-tag) nesting of lambdas.

Unnecessary Wrapping

For a strict (call-by-value) languages all the Monadic code is merely unnecessary function wrapping the way \x -> x is just x or if E then true else false is just E

Encapsulation of Effects

For a lazy (call-by-need) language Monadic composition allows to explicitly define the order of evaluation of a compound expression (implemented as nested lambdas), which is required for serialization of IO, and (orthogonally) to encapsulate an effect inside a specialized implementation of >>= or >> and to encapsulate a state as an explicit parameter being passed through the compound expression (monadic composition).

Too Explicit Sequential Composition

any Sequence (a recursive sum-type) could be wrapped into a Monad (implemented as an instance of a Monad) but this would be an unnecessary wrapping in the context of a strict (call-by-value) language.

a List (a sequential composition of values) could be viewed as an instance of Monad (while it is just a cons of a value a and another List)

Building on top of this

A notion of mapping of a function f on values (of type a -> b) over a value wrapped in a Monad (of type m a), which is similar to mapping a function over a singleton List. Notice how the map function evaluates m (unwraps m) using >>= and lifts (wraps) a value back into a Monad using return (delegation)

map :: (a -> b) -> m a -> m b
map f m =  m >>= \x -> return (f x)

Partially applied map yield a function on Monads m a -> m b (lifting)

This is the notion of flattening.

Notice how join evaluates z (unwraps one m) using >>= (delegation)

join :: Monad m => m (m a) -> m a
join z = z >= \x -> x   -- just id
Last modified 15 months ago Last modified on Dec 29, 2018, 4:45:01 PM
Note: See TracWiki for help on using the wiki.