|
|
Пишет Journal de Chaource (![[info]](http://lj.rossia.org/img/syndicated.gif){kind=small} lj_chaource)@ 2016-08-11 21:44:00 |
 |
|
 |
|
|
|
|
|
|
 |
|
 |
Free functors, free applicatives, free monads IV
Part I
Part II
Part III
After extensive preparation and practice with free functors and free applicatives, we will now find it easy to tackle the free monad.
There are two equivalent definitions of a monadic functor: one with "pure" and "join", another with "pure" and "bind".
All of these properties have the form of a representable functor, that is,
"...something..." -> M t
For this reason, defining the free F-monad is straightforward. We have a choice: either use "pure" and "join", or use "pure" and "bind" as primitive constructors.
The corresponding definitions of a "free F-monad" look like this in the short notation:
M1 t = t + F t + M1 ( M1 t )
M2 t = t + F t + ∃a. M2 a * (a -> M2 t)
Both definitions are recursive and use the recursive instance of "M" at two places.
In Haskell's "long form", the definitions are
These definitions will certainly yield us all the monadic properties "for free".
At this point, we would naturally come up with the following questions about these definitions:
- Are these two definitions equivalent?
- What are the possible "optimizations" for these definitions? How do they affect the performance of the corresponding "universal runners"?
- Is there a definition of M(F) that does not assume that F is a functor?
Comparing the two definitions of the free F-monad, we notice that we can get M2 out of M1 if we substitute M1t by ∃a. M2 a * (a -> t) in the recursive case.
Now, this looks suspiciously like the free functor construction. Note that if F is already a functor then the free F-functor,
∃a. F a * (a -> t),
is actually equivalent to F t. (This is one form of Yoneda's lemma, but that's the only time we used it so far, so I don't feel that it helps to emphasize the name "Yoneda".)
So, it appears that M2 could be a candidate for a free monad that doesn't assume F to be a functor. In its present form, however, M2 does require F to be a functor because F t is one of the variants of M2t, and so F t needs to be a functor by itself.
To remedy this, we can try implementing fmap for M2 in a different way, so that F t after an "fmap" with a function of type "t->s" is converted into ∃a. M2 a * (a -> M2 s) with a = t. To produce a value of (t -> M2 s), we use the given function t -> s and regard s as a "pure" variant of M2 s, so that the given function is viewed as a morphism t -> M2 s. However, this implementation does not satisfy one of the monadic laws: fmap of identity is not equal to identity (because it transforms F t into another variant of M2 t).
Let us therefore consider possible optimizations of the definitions of the free monad.
Our approach to "optimization" consists of trying to replace "M t by "F a" at certain places in the definitions of the free monad, and trying to remove the "wrap" constructor. Let us see how well this works.
It turns out that we can replace "M" by "F" only in the first recursive use of "M". The second recursive use of "M" cannot be replaced by "F", because attempted definitions such as
M t = t + F t + M1 ( F1 t )
M t = t + F t + ∃a. M2 a * (a -> F2 t)
do not work (we can't define the monadic functions "bind" and "join" any more).
Replacing the first recursive use of "M" works and brings the expected results. It is straightforward to check that
M3 t = t + F ( M3 t )
M4 t = t + ∃a. F a * (a -> M4 t)
are valid definitions of the free monad that allow us to define all the required morphisms and satisfy the required laws.
The "wrap" and "bind" operations have to be implemented since they are no longer simply equal to type constructors. Let us show briefly how the "wrap" and "bind" operations are defined for M4. (The corresponding definitions for M3 can be seen in an earlier post.)
To define "wrap", we need to inject a value of F t into M4 t. We can set a = t and use F t * (t -> M t) as the value, where t -> M t is the identity morphism t->t composed with "pure" :: t -> M t to obtain a morphism t -> M t.
To define "bind", we need to transform M t * (t -> M s) into M s. We proceed by case analysis on the first M t. If we have a pure value t, we can evaluate the function t -> M s and obtain a value of M s. If we have a value of ∃a. F a * (a -> M4 t), we can build a function a -> M s by evaluating "bind" recursively on M4 t * (t -> M s). Note that the result is F a * (a -> M s), where the function of type a -> M s contains a call to "bind" but is not yet evaluated. Thus, applying "bind" does not actually run the recursive call to "bind", and so takes O(1) operations. The recursive layers are accumulated in the recursive instance of "M s", while "F a" stays unchanged.
The difference between M3 and M4 can be seen clearly now: M4 uses the free F-functor instead of F. Thus, M4 does not require F to be a functor, while M3 does. When F is a functor, the definitions 3 and 4 are equivalent, due to the fact that the free F-functor is equivalent to F when F is itself a functor (Yoneda's lemma).
The performance differences between M1 and M3 is similar to the difference we saw when studying the free F-functor. The original definition M1 performs no computations at all until the "universal runner" is applied; the "optimized" definitions will perform some computations (composing some functions) while applying "fmap" or "bind" to the free F-monad, so that the "universal runner" will have fewer computations to do.
Note that the runner will have to descend into several layers of "bind", while applying "bind" to the monad itself takes O(1) operations.
We can restore the "F t" constructor in these definitions. However, some of the identity laws will not hold any more, as we already noted. If the violation of these laws is not important, but the performance gain is significant, we can use the versions of the free F-monad with the "F t" constructor. But, strictly speaking, only M3 is the free F-monad in the categorical sense (where F is assumed to be a functor). Replacing F with a free F-functor, we obtain M4 out of M3.
We can also see why it is impossible to replace the second recursive instance of M by F in the definitions of the free F-monad. The free F-monad must, in one way or another, accumulate several layers of "bind" without actually performing those computations. Therefore, it is required that we have some recursive instance of M in the definition. However, if we wanted to have the recursive instance on the first use of "M", we would have to transfer the "bind" or "join" from the second instance of M to the first, passing through a layer of the functor F. This, however, is impossible, since the types F ( M t) and M ( F t) are not equivalent, while we need to define the free F-monad such that it works for every functor F. For this reason, the definitions M3 and M4 are the simplest ones possible.
/lj-cut>
Part I
Part II
Part III
After extensive preparation and practice with free functors and free applicatives, we will now find it easy to tackle the free monad.
There are two equivalent definitions of a monadic functor: one with "pure" and "join", another with "pure" and "bind".
pure :: t -> M t join :: M (M t) -> M t bind :: M a -> (a -> M t) -> M t
All of these properties have the form of a representable functor, that is,
"...something..." -> M t
For this reason, defining the free F-monad is straightforward. We have a choice: either use "pure" and "join", or use "pure" and "bind" as primitive constructors.
The corresponding definitions of a "free F-monad" look like this in the short notation:
M1 t = t + F t + M1 ( M1 t )
M2 t = t + F t + ∃a. M2 a * (a -> M2 t)
Both definitions are recursive and use the recursive instance of "M" at two places.
In Haskell's "long form", the definitions are
data M1 t where Pure :: t -> M1 t Wrap :: F t -> M1 t Join :: M1 (M1 t) -> M1 t data M2 t where Pure :: t -> M2 t Wrap :: F t -> M2 t Bind :: forall a. M2 a -> (a -> M2 t) -> M2 t
These definitions will certainly yield us all the monadic properties "for free".
At this point, we would naturally come up with the following questions about these definitions:
- Are these two definitions equivalent?
- What are the possible "optimizations" for these definitions? How do they affect the performance of the corresponding "universal runners"?
- Is there a definition of M(F) that does not assume that F is a functor?
Comparing the two definitions of the free F-monad, we notice that we can get M2 out of M1 if we substitute M1t by ∃a. M2 a * (a -> t) in the recursive case.
Now, this looks suspiciously like the free functor construction. Note that if F is already a functor then the free F-functor,
∃a. F a * (a -> t),
is actually equivalent to F t. (This is one form of Yoneda's lemma, but that's the only time we used it so far, so I don't feel that it helps to emphasize the name "Yoneda".)
So, it appears that M2 could be a candidate for a free monad that doesn't assume F to be a functor. In its present form, however, M2 does require F to be a functor because F t is one of the variants of M2t, and so F t needs to be a functor by itself.
To remedy this, we can try implementing fmap for M2 in a different way, so that F t after an "fmap" with a function of type "t->s" is converted into ∃a. M2 a * (a -> M2 s) with a = t. To produce a value of (t -> M2 s), we use the given function t -> s and regard s as a "pure" variant of M2 s, so that the given function is viewed as a morphism t -> M2 s. However, this implementation does not satisfy one of the monadic laws: fmap of identity is not equal to identity (because it transforms F t into another variant of M2 t).
Let us therefore consider possible optimizations of the definitions of the free monad.
Our approach to "optimization" consists of trying to replace "M t by "F a" at certain places in the definitions of the free monad, and trying to remove the "wrap" constructor. Let us see how well this works.
It turns out that we can replace "M" by "F" only in the first recursive use of "M". The second recursive use of "M" cannot be replaced by "F", because attempted definitions such as
M t = t + F t + M1 ( F1 t )
M t = t + F t + ∃a. M2 a * (a -> F2 t)
do not work (we can't define the monadic functions "bind" and "join" any more).
Replacing the first recursive use of "M" works and brings the expected results. It is straightforward to check that
M3 t = t + F ( M3 t )
M4 t = t + ∃a. F a * (a -> M4 t)
are valid definitions of the free monad that allow us to define all the required morphisms and satisfy the required laws.
The "wrap" and "bind" operations have to be implemented since they are no longer simply equal to type constructors. Let us show briefly how the "wrap" and "bind" operations are defined for M4. (The corresponding definitions for M3 can be seen in an earlier post.)
To define "wrap", we need to inject a value of F t into M4 t. We can set a = t and use F t * (t -> M t) as the value, where t -> M t is the identity morphism t->t composed with "pure" :: t -> M t to obtain a morphism t -> M t.
To define "bind", we need to transform M t * (t -> M s) into M s. We proceed by case analysis on the first M t. If we have a pure value t, we can evaluate the function t -> M s and obtain a value of M s. If we have a value of ∃a. F a * (a -> M4 t), we can build a function a -> M s by evaluating "bind" recursively on M4 t * (t -> M s). Note that the result is F a * (a -> M s), where the function of type a -> M s contains a call to "bind" but is not yet evaluated. Thus, applying "bind" does not actually run the recursive call to "bind", and so takes O(1) operations. The recursive layers are accumulated in the recursive instance of "M s", while "F a" stays unchanged.
The difference between M3 and M4 can be seen clearly now: M4 uses the free F-functor instead of F. Thus, M4 does not require F to be a functor, while M3 does. When F is a functor, the definitions 3 and 4 are equivalent, due to the fact that the free F-functor is equivalent to F when F is itself a functor (Yoneda's lemma).
The performance differences between M1 and M3 is similar to the difference we saw when studying the free F-functor. The original definition M1 performs no computations at all until the "universal runner" is applied; the "optimized" definitions will perform some computations (composing some functions) while applying "fmap" or "bind" to the free F-monad, so that the "universal runner" will have fewer computations to do.
Note that the runner will have to descend into several layers of "bind", while applying "bind" to the monad itself takes O(1) operations.
We can restore the "F t" constructor in these definitions. However, some of the identity laws will not hold any more, as we already noted. If the violation of these laws is not important, but the performance gain is significant, we can use the versions of the free F-monad with the "F t" constructor. But, strictly speaking, only M3 is the free F-monad in the categorical sense (where F is assumed to be a functor). Replacing F with a free F-functor, we obtain M4 out of M3.
We can also see why it is impossible to replace the second recursive instance of M by F in the definitions of the free F-monad. The free F-monad must, in one way or another, accumulate several layers of "bind" without actually performing those computations. Therefore, it is required that we have some recursive instance of M in the definition. However, if we wanted to have the recursive instance on the first use of "M", we would have to transfer the "bind" or "join" from the second instance of M to the first, passing through a layer of the functor F. This, however, is impossible, since the types F ( M t) and M ( F t) are not equivalent, while we need to define the free F-monad such that it works for every functor F. For this reason, the definitions M3 and M4 are the simplest ones possible.
/lj-cut>
