10:44]
@loganmac Another way to think of the free monad over f is to say we want expressions of the form x >>= \a -> y >>= \b -> z ... where x, y, z :: f _
[10:45]
So we just make a type by expanding f to include those terms, purely symbolically. But then to be a Monad we need the laws to hold, so we equate terms which the laws say have to be equal
[10:46]
So finding the free monad over f is to find the "smallest" lawful monad which includes all such terms
[10:46]
The adjunction between Free and the forgetful functor is another way to see this
[10:47]
For there to be an adjunction, we need a natural isomorphism forall g. Monad g => (f ~> g) -> (Free f ~> g)
[10:49]
Turn it around: Free f ~> Λa. { forall g. Monad g => (f ~> g) -> g a }
[10:49] I'm running out of syntax here
[10:49] Anyway, you can ask how we can form the terms on the right there, and what do the monad laws say about when those various terms are equal?
[10:50]
If I want a forall g. Monad g => (f ~> g) -> g a, I could have x :: a on hand, in which case I could give you back \_ -> pure x. That is like the Pure constructor of Free
[10:51]
Or maybe I have y :: f a, then I can give you \k -> k y
[10:52]
Or if I have z :: f b and w :: b -> f a, I could give you \k -> k z >>= k <<< w
[10:52]
It turns out the possible solutions (up to equalities given by the laws) are exactly the inhabitants of Free f a
[10:53]
So forall g. Monad g => (f ~> g) -> g a gives another way of thinking about how Free constructs the smallest monad which supports the actions we want from f.