so, free monads
Nov. 1st, 2016 07:13 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
juan_gandhiAs I understand for a functor F to be able to produce a free monad, it has to preserve colimits, right? That includes unions.
So the functor X2, not preserving sums, cannot produce a free monad... right? I think so, at least.
On the other hand, a fixpoint of 1+X2 is a binary tree. So? :)
Something's wrong here.
So the functor X2, not preserving sums, cannot produce a free monad... right? I think so, at least.
On the other hand, a fixpoint of 1+X2 is a binary tree. So? :)
Something's wrong here.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2016-11-02 07:42 am (UTC)> cannot produce a free monad... right?
Functor X^2 is a not functor on a category of functors.
no subject
Date: 2016-11-02 06:17 pm (UTC)no subject
Date: 2016-11-02 09:31 am (UTC)Isn't this once again about the fact that "categorical" nomenclature in type theory doesn't map to actual categorical nomenclature it mimics?
Free Pairsure exists, it's a binary values-in-leaves tree.> fixpoint of 1+X2 is a binary tree
Well, if we define
data Either' f a b = Left' (f a) | Right' b, then it's easy to show thatFree f ais isomorphic toFix2 (Either' f) a. This can be extended to a more general notion of covariant functors (endofunctors in the category of indexed types, at least), but it gets seriously ugly, and I haven't the foggiest how all of that maps to proper CT.no subject
Date: 2016-11-02 12:25 pm (UTC)(probably true for pretty much any application in computer science),
then all what you need is preservation of filtered colimits
(i.e., no need to preserve coproducts).
This is a rather weak condition and monads with such a property are sometimes
referred to as finitary monads
(and finitary endofunctors are endofunctors that preserve filtered colimits).
In fact, in this situation not only does the free monad always exist,
but the adjunction between finitary monads and finitary endofunctors
is itself monadic, i.e., there is a certain monad on the category
of finitary endofunctors whose algebras are (finitary) monads.
This is a theorem of Kelly, see
http://dx.doi.org/10.1016/S0022-4049(99)00019-5
no subject
Date: 2016-11-02 06:18 pm (UTC)no subject
Date: 2016-11-03 05:17 pm (UTC)Мне кажется, что в статье из предыдущего пункта устанавливаются условия для более сильного результата, чем просто существование св. монады. Интересно поставить вопрос о контрпримере, в смысле свободной монады на нефинитарном функторе.
no subject
Date: 2016-11-03 06:34 pm (UTC)Нефинитарный, для которого свободная монада существует (мой пример не годится?), и нефинитарный, для которого свободной монады не существует.
no subject
Date: 2016-11-03 06:48 pm (UTC)no subject
Date: 2016-11-03 06:46 pm (UTC)no subject
Date: 2020-11-01 07:23 pm (UTC)Filtered colimits only. Sum is not a filtered colimit.