I define free Monad
and free Applicative
using single type, parametrised over a tensor. It's possible, because both Monad
and Applicative
are monoids in the category of endofunctors. There is little, if any, practical applications I can foresee for these definitions, but it's fun to see how things are connected. I won't prove laws hold, or constructions are free (= are left adjoint of a forgetful functor).
The post was inspired by Bartosz Milewski blog post about Free Monoidal Functors, and only while writing this I discovered Notions of Computations as Monoids, read that for rigid explanations.
Warning: plenty of infix operators ahead. Also formulas typeset with LaTeX.
Free applicative functors are free monoids where Day convolution is a tensor:
On the other hand, free monads are also free monoids, but with function composition as monoidal product.
Note, lists are also free monoids where product is a Cartesian product (different category)!
So we can extract the common free monoid notion:
or
as in free monoid - ncatlab article.
Using we can abstract over applicatives and monads (and lists):
Let's try to encode all of that in Haskell.
This blog post is a literate Haskell file. For this work we don't need a lot of extensions, they'd almost fit on one line.
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module SingleFree where
-- all these imports are from the base library
import Control.Applicative ((<**>))
import Data.Functor.Identity (Identity (..))
import Data.Proxy (Proxy (..))
import GHC.Exts (Constraint)
-- for examples
import Control.Monad.Trans.Writer (Writer, tell, runWriter)
import Data.Functor.Const (Const (..))
import Text.Read (readMaybe)
-- we'll define own isomorphic variants.
import qualified Data.Functor.Compose as B -- from base
import qualified Data.Functor.Day as K -- from kan-extensions
Let's start by defining a free monoid. The definition resembles in shape the definition of lists, but is higher-order and parametrised over a tensor h
and its unit i
:
We could also used a FixH
(as Bartosz does in his post) and separate FreeF
algebra, but for our purposes splitting out recursion is not necessary, and would only clutter the presentation.
Next we need tensors. These definitions are unorthodox. Enlightened reader would guess why we use such variants. We will explain that in the respective sections.
data Day f g a where
(:<**>:) :: f x -> g (x -> a) -> Day f g a
data Comp f g a where
(:>>=:) :: f x -> (x -> g a) -> Comp f g a
infix 1 :>>=:
Using Free
we can right away define free Applicative
and free Monad
: Both tensors have Identity
as a unit functor.
Let's see how to define the operations on Free
. We can immediately define pure
(or return
), independently of choice of h
or f
:
As both free applicative and free monad are free monoids in category of endofunctors, it shouldn't be surprising that pure
and return
look like empty list. (Even there's a
, there aren't any f
).
Both Applicative
and Monad
instances can be defined in a very similar way using auxiliary classes HAppend
and FromDay
:
instance (FromDay h, i ~ Identity) => Applicative (Free h i f) where
pure = point
f <*> x = happend $ fromDay $ f :<**>: fmap (flip id) x
instance (h ~ Comp, i ~ Identity) => Monad (Free h i f) where
return = point
m >>= k = happend $ m :>>=: k
FromDay
witnesses a tensor homomorphism from Day
to h
.
The long squiggly arrow is a transformation between Tensor
s:
Day
can be converted to Day
trivially:
HAppend
is a generalization of ++
for our Free
lists, happend
appends two Free h
"lists". We need such class as plumbing is different for different choices of h
. (Here I really miss that we cannot use infix operator as a type variable!)
The short squiggly arrows are natural transformations:
One interesting operation is lifting f a
into a free structure. For that we need more structure from h
, in particular left unitor intro1
. Then we map into Done
, and wrap that into More
. In other words that's a singleton
for a list.
For this operation we show types of intermediate results:
Or in Haskell:
The last operation is retracting of a free structure, one can spot the resemblance with foldMap
.
retractFree :: forall h f g a. (HApply h, C h g)
=> (f ~> g) -> Free h (I h) f a -> g a
retractFree _nt (Done x) = hpure (Proxy :: Proxy h) x
retractFree nt (More x) = happly (hbimap nt (retractFree nt) x)
HApply
"applies" or retracts the tensor. That doesn't work for all f
, so we need a constraint. It carries natural transformations
Or in Haskell terms:
class Tensor h => HApply h where
type C h :: (* -> *) -> Constraint
hpure :: C h f => Proxy h -> I h a -> f a
happly :: C h f => h f f a -> f a
The basic example for free monads is the restricted IO. First we define the operation type (note, not a Functor
):
Test console writes output into Writer
log, and always returns "yes"
as an input.
testConsole :: Console ~> Writer [String]
testConsole (Output s) = tell [s]
testConsole Input = return "yes"
The runnable example of reading an input once, writing it and "done"
, and returning the read value as result of the computation:
-- ("yes",["yes", "done"])
exampleM :: (String, [String])
exampleM = runWriter $ retractFree testConsole $ do
x <- liftFree Input
liftFree $ Output x
liftFree $ Output "done"
return x
Free applicatives are used a lot in various parsers. For example a naive command line argument parser: First a type encapsulating an option (example as in Free Applicative Functors by Paolo Capriotti and Ambrus Kaposi)
Then we need a type for a value we need to parse, let's use simple User
:
The example parser could look like:
userParser :: Free Day Identity Option User
userParser = User
<$> option "name"
<*> option "id"
where
option :: Read a => String -> Free Day Identity Option a
option n = liftFree $ Option n readMaybe
And because the structure is static, we can not only run the parser, but also generate "help" message:
-- ["name","id"]
exampleA :: [String]
exampleA = getConst $ retractFree nt userParser where
nt :: Option ~> Const [String]
nt = Const . return . optName
In this section we define HBifunctor
, Tensor
and other related type classes.
As we deal with tensors which are (higher-order) bifunctors, we will need a variant of Bifunctor
for higher order functors. In this post will have a special version, one where bfmap
(a variant of fmap
) requires only second argument to be Functor
. The kind annotation for h
isn't strictly required, but it's there to show that h
is binary operations on types of kind * -> *
. hbimap
is a higher-order variant of bimap
.
class HBifunctor (h :: (* -> *) -> (* -> *) -> (* -> *)) where
bfmap :: Functor g => (a -> b) -> h f g a -> h f g b
hbimap :: (f ~> f') -> (g ~> g') -> (h f g ~> h f' g')
Using HBifunctor
we can defined Functor
instance for Free
.
instance (HBifunctor h, Functor i) => Functor (Free h i f) where
fmap f (Done x) = Done (fmap f x)
fmap f (More x) = More (bfmap f x)
Some HBifunctor
s are Tensor
s. Tensor laws resembles monoidal ones: I h
is a unit functor and h
is associative up to isomorphism.
See Wikipedia or ncatlab for more discussion.
class (HBifunctor h, Functor (I h)) => Tensor h where
type I h :: * -> *
intro1 :: f ~> h f (I h)
intro2 :: Functor g => g ~> h (I h) g
elim1 :: Functor f => h f (I h) ~> f
elim2 :: Functor g => h (I h) g ~> g
assoc :: (Functor f, Functor g, Functor k)
=> h f (h g k) ~> h (h f g) k
disassoc :: (Functor k)
=> h (h f g) k ~> h f (h g k)
Next we'll define two Tensor
s: function composition Comp
and Day convolution Day
.
Day convolution (named after Brian Day) is a product in the category of endofunctors. We won't use kan-extensions
definition but have slightly different one:
It and kan-extensions
definition are isomorphic, we can convert back and forth:
toKanExts :: Day f g a -> K.Day f g a
toKanExts (fx :<**>: gxa) = K.Day fx gxa (flip id)
fromKanExts :: Functor g => K.Day f g a -> Day f g a
fromKanExts (K.Day fx gy xya) = fx :<**>: fmap (flip xya) gy
Similarly to Comp
(defined later), Functor (Day f g)
requires Functor g
, but not Functor f
.
-- used in this post
instance Functor g => Functor (Day f g) where
fmap h (fx :<**>: gxa) = fx :<**>: fmap (h .) gxa
Day
is HBifunctor
:
Next we define rest of the instances for Day
: it's a Tensor
, HApply
and Happend
.
Day
is a tensor, with Identity
as a unit:
instance Tensor Day where
type I Day = Identity
intro1 fx = fx :<**>: Identity id
intro2 gx = Identity () :<**>: fmap const gx
elim1 (fx :<**>: Identity xa) = fmap xa fx
elim2 (Identity x :<**>: gxa) = fmap ($ x) gxa
assoc (fx :<**>: (gy :<**>: kyxa)) =
(fx :<**>: fmap (,) gy) :<**>: fmap uncurry kyxa
disassoc ((fx :<**>: gxy) :<**>: kya) =
fx :<**>: (gxy :<**>: fmap (.) kya)
HApply
and Happend
instances are interesting, they show why we chose :<**>:
name for the constructor. HApply
needs Applicative
constraint, and we use <**>
in happly
implementation:
instance HApply Day where
type C Day = Applicative
hpure _ = pure . runIdentity
happly (fx :<**>: gxa) = fx <**> gxa
HAppend
instance is straight forward. Note how More
case resembles the disassoc
defined above.
instance HAppend Day where
happend (fx :<**>: gxa) = fx -<**>- gxa
(-<**>-) :: FreeA f x -> FreeA f (x -> a) -> FreeA f a
Done (Identity x) -<**>- xa = fmap ($ x) xa
More (fz :<**>: gzx) -<**>- xa = More $
fz :<**>: (gzx -<**>- fmap (.) xa)
One more point: kan-extensions
Day
has liftA2
as the "native" operation (you should think how Free Day
"lists" would look like, if used this definition):
instance HAppend K.Day where
happend (K.Day fx gy xya) = liftA2' xya fx gy
liftA2' :: (a -> b -> c)
-> Free K.Day Identity f a
-> Free K.Day Identity f b
-> Free K.Day Identity f c
liftA2' abc (Done (Identity a)) fb = fmap (abc a) fb
liftA2' abc (More (K.Day gx fy xya)) fb = More $ K.Day
gx
(liftA2' (,) fy fb)
(\x (y, b) -> abc (xya x y) b)
In previous section we defined own version of functor composition.
That's a surprising choice, as Functor composition is usually defined as
We can convert between these definition quite freely:
toBase :: Functor f => Comp f g a -> B.Compose f g a
toBase (fx :>>=: xga) = B.Compose (fmap xga fx)
fromBase :: B.Compose f g a -> Comp f g a
fromBase (B.Compose fga) = fga :>>=: id
The reason is that to make comparison with Day convolution more fair, we'll drop the requirement for Functor f
. We can do this by wrapping f
in (sliced in) Coyoneda
.
So instead of
-- base
instance (Functor f, Functor g) => Functor (Compose f g) where
fmap f (Compose x) = Compose (fmap (fmap f) x)
we have more relaxed context for Functor (Comp f g)
instance:
-- used in this post
instance Functor g => Functor (Comp f g) where
fmap ab (fx :>>=: xga) = fx :>>=: fmap ab . xga
And because of relaxed context, we can defined HBifunctor
instance:
Instead of usual Free
monad (which requires Functor f
), with our Comp
we will get a freer monad (which doesn't require Functor f
). Free
monad adds return
and join
operations (you still need fmap
), where naive encoding of freer monad adds return
and bind
, thus doesn't requiring anything from the f
.
-- Haskell98, written using GADTSyntax
data Free f a where
Pure :: a -> Free f a
Join :: f (Free f a) -> Free f a
-- Needs GADTs
data Freer f a where
Pure :: a -> Freer f a
Bind :: a -> (a -> Freer f b) -> Freer f b
The rest of this section is instance definitions.
Comp
is a tensor with Identity
as a unit:
instance Tensor Comp where
type I Comp = Identity
intro1 fx = fx :>>=: Identity
intro2 gx = Identity () :>>=: const gx
elim1 (fx :>>=: xga) = fmap (runIdentity . xga) fx
elim2 (fx :>>=: xga) = xga (runIdentity fx)
disassoc ((fx :>>=: xgy) :>>=: yka) =
fx :>>=: \x -> xgy x :>>=: yka
assoc = error "hard"
The HApply
requires a Monad
as a constraint:
instance HApply Comp where
type C Comp = Monad
hpure _ = return . runIdentity
happly (fx :>>=: xga) = fx >>= xga
As in Day
case, Happend
instance for Comp
shows why the constructor is named :>>=:
(Also if we would use Compose
from base
, the operation would look like join
).
instance HAppend Comp where
happend (x :>>=: f) = x ->>=- f
(->>=-) :: FreeM f a -> (a -> FreeM f b) -> FreeM f b
Done (Identity x) ->>=- f = f x
More (x :>>=: g) ->>=- f =
More $ x :>>=: \a -> g a ->>=- f
The last thing to do is FromDay
instance for Comp
. Because Hask has rich structure, we can convert Day
into Comp
.
Compare that to
it's virtually the same.
As we represent free applicatives and free monads using same Free
, it's quiet simple to map free Applicative
to free Monad
:
where hhoistFree
changes the tensor:
hhoistFree :: forall h g i f. (HBifunctor h, HBifunctor g, Functor i)
=> (h ~~> g)
-> Free h i f ~> Free g i f
hhoistFree nt = go where
go :: forall x. Free h i f x -> Free g i f x
go (Done x) = Done x
go (More x) = More $ nt $ hbimap id go x
Let's look on tensors we have, They have similar structure:
data Comp f g a where (:>>=:) :: f x -> (x -> g a) -> Comp f g a
data Day f g a where (:<**>:) :: f x -> g (x -> a) -> Day f g a
The object can be split into and for some .
This can be encoded in Haskell as another type-class:
class Tensor h => Uncons h where
type Arrow h :: (* -> *) -> * -> * -> *
split :: h f g a -> Combined (Arrow h) f g a
combine :: f x -> Arrow h g x a -> h f g a
(>>>) :: Arrow h (Free h (I h) f) a b
-> Arrow h (Free h (I h) f) b c
-> Arrow h (Free h (I h) f) a c
infixr 1 >>>
where Combined
is a specialized dependent sum:
data Combined (h' ::(* -> *) -> * -> * -> *) f g a where
(:=>) :: f x -> h' g x a -> Combined h' f g a
We already spoiled a little: the reminder of "unconsing" f x
, is an arrow! And they can be composed with >>>
. Using this machinery we can define happend'
differently, pushing the combination plumbing into implementation of >>>
:
happend' :: Uncons h
=> Free h (I h) f `h` Free h (I h) f ~> Free h (I h) f
happend' t = case split t of
Done i :=> f -> elim2' (combine i f)
More lhs :=> f -> case split lhs of
x :=> g -> More $ combine x (g >>> f)
where elim2'
is a specialised version of elim2
to help out the type-checker:
Now we only need to show that Comp
and Day
are instances of Uncons
: The arrow for Comp
is not so surprising, it's Kleisli
:
newtype Kleisli g x a = Kleisli (x -> g a)
instance Uncons Comp where
type Arrow Comp = Kleisli
split (fx :>>=: xga) = fx :=> Kleisli xga
combine fx (Kleisli xga) = fx :>>=: xga
Kleisli ab' >>> Kleisli bc' = Kleisli $ go ab' bc' where
go :: (a -> FreeM f b) -> (b -> FreeM f c) -> (a -> FreeM f c)
go ab bc a = case ab a of
Done (Identity b) -> bc b
More (fx :>>=: xb) -> More $ fx :>>=: go xb bc
The arrow for Day
is less known, so called StaticArrow
(it's an Arrow
if g
is an Applicative
, Kleisli
is an arrow if g
is a Monad
):
newtype StaticArrow g x a = StaticArrow (g (x -> a))
instance Uncons Day where
type Arrow Day = StaticArrow
split (fx :<**>: gxa) = fx :=> StaticArrow gxa
combine fx (StaticArrow gxa) = fx :<**>: gxa
StaticArrow ab' >>> StaticArrow bc' = StaticArrow $ go ab' bc' where
go :: FreeA f (a -> b) -> FreeA f (b -> c) -> FreeA f (a -> c)
go (Done (Identity ab)) bc = fmap (. ab) bc
go (More (fx :<**>: fxb)) bc =
More $ fx :<**>: go fxb (fmap (.) bc)
I think we can define Free
also using a Path
of Arrow
s and a first element. I leave that as an extended exercise for a reader. :)
We defined Tensor
so we can have other unit than Identity
. We can use this now. The Product
(pair) as a tensor with Proxy
as a unit. The free monoid is a "list of f a
".
Again, we don't use base
Product
, but a variant with embedded Coyoneda
for first element. The mapping function is put into a new data type. This makes plumbing less tedious as Arrow Prod = ProdK
:
data Prod f g a where
(:*:) :: f x -> ProdK g x a -> Prod f g a
data ProdK g a b = (a -> b) :> g b
infix 6 :*:
infix 7 :>
Fixity definitions are important, as we don't need to write as many parentheses. We skip ahead to define HApply
. What's the right constraint? Alternative
feels like a good fit, but it has restrictive context (Applicative
), so let's define a new class:
class Functor f => Monoid1 f where
unit1 :: f a
(<!>) :: f a -> f a -> f a
infixl 3 <!>
instance HApply Prod where
type C Prod = Monoid1
hpure _ _ = unit1
happly (fx :*: xa :> ga) = xa <$> fx <!> ga
instance (h ~ Prod, i ~ Proxy) => Monoid1 (Free h i f) where
unit1 = Done Proxy
f <!> x = happend (f :*: id :> x)
Note: Monoid1
class is deliberately agnostic to "left catch" vs. "left distribution". It's just a monoid. (See MonadPlus
on wiki.haskell.org or documentation for Alt
class).
instance HAppend Prod where
happend (fx :*: xa :> gxa) = appendProd fx xa gxa
type FreeP = Free Prod Proxy
appendProd :: FreeP f x -> (x -> a) -> FreeP f a -> FreeP f a
appendProd (Done Proxy) _ fa = fa
appendProd (More (fy :*: yx :> fx)) xa fa = More $
fy :*: xa . yx :> appendProd fx xa fa
The following example will use retractFree
to extract the list of f a
.
newtype List1 f a = List1 { getList1 :: [f a] }
instance Functor f => Functor (List1 f) where
fmap f (List1 xs) = List1 (fmap (fmap f) xs)
instance Functor f => Monoid1 (List1 f) where
unit1 = List1 []
List1 xs <!> List1 ys = List1 (xs ++ ys)
freePToList :: Functor f => FreeP f a -> [f a]
freePToList = getList1 . retractFree (\x -> List1 [x])
In theory, we could split Free
into FixH
and FreeF
, and then make a fixed point of a composition of FreeF Day
and FreeF Prod
to build a free Alternative
out of abstract non-senses. In practice you'd use something simpler or even completely custom thing (especially if you cannot have default many
or some
).
The rest of the section are instances, for completeness. Note that I Prod = Proxy
. It's unusual use for Proxy
!
instance Functor g => Functor (ProdK g a) where
fmap f (ab :> gb) = f . ab :> fmap f gb
instance Functor g => Functor (Prod f g) where
fmap ab (fx :*: xaga) = fx :*: fmap ab xaga
instance HBifunctor Prod where
bfmap = fmap
hbimap f g (fx :*: xaga) = f fx :*: hoistProdK g xaga
hoistProdK :: (f ~> g) -> ProdK f a b -> ProdK g a b
hoistProdK nt (ab :> gb) = ab :> nt gb
instance Tensor Prod where
type I Prod = Proxy
intro1 fa = fa :*: id :> Proxy
intro2 ga = Proxy :*: id :> ga
elim1 (fx :*: xa :> _) = fmap xa fx
elim2 (_ :*: _ :> ga) = ga
disassoc ((fx :*: xy :> gy) :*: ya :> ka) =
fx :*: ya . xy :> (gy :*: ya :> ka)
assoc (fx :*: xa :> (gy :*: ya :> ka)) =
(fx :*: xa :> fmap ya gy) :*: id :> ka
instance Uncons Prod where
type Arrow Prod = ProdK
split (fx :*: xaga) = fx :=> xaga
combine = (:*:)
ab :> fb >>> bc' :> fc = bc' . ab :> go fb bc' fc where
go :: FreeP f x -> (x -> y) -> FreeP f y -> FreeP f y
go (Done Proxy) _ gc = gc
go (More (gx :*: xb :> gb)) bc gc =
More $ gx :*: bc . xb :> go gb bc gc
There is a lot of abstract nonsense in this post, hopefully you enjoyed and gained some new insights! Drop me a line on Twitter or Reddit.