Skip to content

Latest commit

 

History

History
444 lines (326 loc) · 13 KB

story-of-effects.org

File metadata and controls

444 lines (326 loc) · 13 KB
Raw

Taming of effects (in Haskell)

Taming effects

A tour of why things are as they are in the ongoing attempt(s) to encode effects in Haskell (a pure functional, lazy language).

We will perhaps, also see that:

“…code is the wrong abstraction for doing programming.” –Sandy Maguire. Algebra-Driven Design

Overview

./sof-map.png

Model effects

Because really we want to have impure “functions”: a ~> b

  • Partial functions a -> Maybe b
  • Environment (a,e) -> b
  • State (a,s) -> (b,s)
  • Non-determinism a -> [b]

How to proceed?

Kleisli arrows

Impure functions can be encoded in a common pattern:

a -> t b          -- for some (Type->Type) t
                  -- e.g.
a -> Maybe b      -- partial a ~> b
a -> (e -> b)     -- Reader e a
a -> (s -> (b,s)) -- State s a
a -> List b       -- Non-det
a -> IO b         -- world state

These are known as Kleisli arrows, (or morphisms in the Kleisli category). (Aka T-programs: A -> T(B); T(B) is a T-computation)

To write functional programs we want to compose these arrows…

The Kleisli Category

Composition of Kleisli arrows

The “fish” operator

(>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)

Identity for composition

return :: a -> m a

return >=> f ≡ f – left identity

f >=> return ≡ f – right identity

What we have

✓ Composition of Kleisli arrows (>=>)

With a “proof” of:

✓ associativity

✓ left and right identity

So our morphisms commute/compose and we have identities for them: it looks like a category, walks like a category…

A Monad?

a -> T b

T is a monad just when it has the structure needed to turn T-programs into a category:

i.e. The Kleisli category of the monad T

But we have also defined

“A monoid in the category of endofunctors” (in the category Hask)

(via composition of Kleisli arrows)

So what’s the problem? 🤯

What monad is not

Anything else (not a Burrito for sure!) and now we are officially forbidden from writing monad tutorials…

bind and join?

Give me Kleisli composition; I’ll give you bind:

infixr 1 >=>
-- | Monad done right :)
class Monad m where
  (>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
  return :: a -> m a
  -- | Bind in terms of composition of Kleisli arrows
  (>>=) :: m a -> (a -> m b) -> m b
  m >>= f = id >=> f $ m

So why bind is default?

  • It’s often easier to define bind for an instance.
  • Kleisli composition is the real deal though as it reflects the essense of the category.

Deriving fish (>=>) from bind (>>=) is left as an exercise.

Bind and Join

-- | bind in terms of join
(>>=) :: Monad m => m -> (a -> m b) -> m b 
m >>= f = join $ fmap f m

-- | join in terms of bind
join :: Monad m => m (m a) -> m a
join mm = mm >>= id

A historical note on Monad

I didn’t need to add a constraint for Functor as fmap can be derived from bind:

fmap :: Monad f => (a -> b) -> f a -> f b
fmap f m = m >>= return . f

-- Or more fishy 
fmap f = id >=> (\x -> return (f x))

And for a long time AFAIK this was Monad (in Haskell)

Monad composition is not closed

If we tried to compose two monads and implement join for the composite; we would end up needing the distributive law:

distribute :: (Monad f, Monad g) => g (f a) -> f (g a)

Can you see how that might (not) work?

distribute :: IO (Maybe a) -> Maybe (IO a)

Stackoverflow question n-category cafe

What is this Free thing then?

What is means to be free

A free structure on A has all the laws for A but no other constraints i.e. it’s free to be A (free as in freedom).

So far we have a free monoid (via. Kleisli composition)

Free by fiat

data Free f a
  = Pure a
  | Free (f (Free f a))

Which looks like a tree with branches of the Free structure of an arbitrary type f and leaves of type a.

Reminiscent of anything?

The constructors look like return and join!

data Free f a where
  Pure :: a -> Free f a            -- return :: a -> f a
  Free :: f (Free f a) -> Free f a -- join :: m (m a) -> m a

Voilà: The Free Monad

Since we can define Monad in terms of return, join and fmap; we can encode the monad in the free structure iff we require f to be a functor:

instance Functor f => Functor (Free f) where
  fmap f (Pure x) = Pure (f x)
  fmap f (Free g) = Free (fmap f <$> g)

instance Functor f => Monad (Free f) where
  return = Pure
  Pure x >>= f = f x
  Free g >>= f = Free ((>>= f) <$> g)

So what? What’s it for?

Introduction to Free Monads - Nikolay Yakimov

Using free monads, we can define a computation as a data structure.

The data structure in question doesn’t define how the computation is performed.

We can write a separate interpreter (or indeed many interpreters) that performs the actual computation in question.

Trees of computations?

Embedded domain specific languages (eDSL)

  • Abstract syntax tree (AST)
  • Interpreter(s)

effects expressed as ASTs that can be interpreted by handlers!

Moving past the typeclasses

The Principle of Least Power!

Monad > Arrow > Applicative

SO: When does one consider using (say) arrows?

Ans: Probably never :) some good comments from that discussion suggest not putting the cart before the horse.

That is; model domain entities and their natural algebras first, only then see if there’s some nice higher order structures that would be useful.

✓ Algebra Driven Design - Sandy Maguire ✓ Denotational Design - Conal Elliot

Then design a eDSL 🙂

Free summary

  • Any functor can be lifted into Free.
  • Free allows the evaluation of an AST of effects to be deferred.
  • This makes writing eDSLs very easy as Free monads are:
    • Composable
    • Extensible
    • allow for multiple interpretations
    • and we get do notation for free (as in beer, not freedom)

And in the end its all the same

But you might have your cake AND eat it too:

Next?

  • Data types à la Carte
  • Tagless finally
  • Denotational design
  • Other composable structures
    • Arrows etc.
  • A look at frameworks and libraries
    • polysemy, free, freer, eff, fused-effects, effectful

Roadmap