Is there some unifying concept to be found here that would bring the now
, delay
, and weft
operations into some sort of inheritance hierarchy, with delay = weft . pure
and now = weft . fmap pure
as laws akin to the laws that relate pure
, (<*>)
and (>>=)
?
The relation between now
, delay
, weft
is closely connected to the Applicative-Monad hierarchy. There is a different presentation of these operations as follows.
An “applicative with f
” is an applicative functor m
with an embed :: forall a. f a -> m a
:
class ApplicativeWith f m where
pure :: a -> m a
liftA2 :: (a -> b -> c) -> m a -> m b -> m c
embed :: f a -> m a
A “monad with f
” is a monad with embed
.
class MonadWith f m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
embed :: f a -> m a
Here the operations pure
/liftA2
/(>>=)
should be thought concretely as those of the Free
applicative and Free
monad, which are different from those of Phases
and Weave
even though they are the same types (actually, there is a small difference between Phases
and the Free
applicative which is unimportant).
An applicative with f
can implement now
and delay
: now = embed
,
and delay
appends pure () :: f ()
to a computation: delay = (pure () *>)
.
A monad with f
can implement weft = join . embed
. A “monad with f
” is of course also an “applicative with f
”, so it also implements now
and delay
.
With that, the equations relating weft
to now
and delay
can be derived from the definitions of pure
and liftA2
/(<*>)
using return
and (>>=)
.
I’m deeply intrigued by the similarity between the shapes of Phases
and WeaveL
(with a flipping of the parameters to make things line up):
-- T = Phases
data T f a where
_ :: f a -> T f a
_ :: f (a -> b) -> T f a -> T f b
-- T = WeaveL
data T f a where
_ :: a -> T f a
_ :: (a -> b) -> f (T f a) -> T f b
The lining up of (a -> b)
/a
in the second constructor is because both involve a “Day convolution”, which is a product-like operation on functors.
data Day :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
Day :: f (a -> b) -> g a -> Day f g b
(There is a slightly different definition of Day
in the library kan-extensions which generalizes further to non-functors.)
In a way, the fact that the pattern _ (a -> b) -> _ a -> _ b
appears in both Phases
and WeaveL
just says that they both involve a certain notion of “multiplication”, which is Day convolution. That common point is very visible because the definition of multiplication is inlined in both, but it is not a super deep common point because multiplication is a quite common operation.
The difference between WeaveS
and WeaveL
is the difference between y and 1 \times y, where 1 is the functor Identity
, \times is Day
convolution, and y is the functor f . T f
. On a semantic level, the fact that WeaveS
and WeaveL
have the same “meaning” is as obvious as x = 1 \times x. Thus the occurrence of Day
convolution in WeaveL
is not as meaningful as it is in Phases
.
-- These constructors of WeaveL and WeaveS are semantically equivalent
Weft :: (a -> b) -> f (T f a) -> T f b -- 1 Ă— y = Day Identity (f :.: T f)
Weft :: f (T f a) -> T f a -- y = f :.: T f
Another way to line up weaves and phases which I mention briefly at the end of my post is
-- Phases with a simplified base case
data T f a where
_ :: a -> T f a
_ :: (f `Day` T f) a -> T f a
-- WeaveS
data T f a where
_ :: a -> T f a
_ :: (f :.: T f) a -> T f a
Those types correspond to two interpretations of the equation T = 1 + f \times T as an equation between functors:
- if \times is
Day
, then T is Phases f
;
- if \times is
(:.:)
(aka. Compose
), then T is Weave f
.
You may have seen that equation elsewhere, as an equation between types:
- if \times is
(,)
(the product of types), then T is [f]
, the type of lists of f
.
Phases
and Weave
are just lists in a different category!
Re @meooow: that’s an awesome find! This will be a fine addition to the weave library.