Great lecture, thanks very much! I did find the following somewhat confusing on first viewing: at 37:15 you start talking about the category of algebras for a fixed endofunctor. Objects in this category is a pair of an object and a morphism (38:00); when explaining the constraint on the morphisms in this category a second diagram is drawn (starting at 39:42). It took me a while to understand that this second diagram is in a different category (I think: Hask), especially since no further diagrams of the category of algebras are drawn. Hope that's helpful!
The category of algebras for a given endofunctor is built on top of the underlying category (this can be any category). The diagrams I draw are in the underlying category -- they show the "implementation" of the morphisms of the category of algebras in terms of morphisms in the underlying category.
Excellent lecture. Was a bit confused about how the fixed point of a functor fits in the with rest of the lecture though. Is `(Fix f) a -> a` also an algebra? Will probably have to go over this lecture again.
Assuming I understand it correctly, the algebra is the function which can evaluate things that one might find at the ends of branches in an expression tree, but that is not recursive on its own, and nor is the functor on which the algebra is based. In order to construct a tree of arbitrary depth, you need Fix. It's then the catamorphism which can traverse the tree and distill it to a single value in the carrier type.
As a passing remark, interestingly, if I'm not mistaken, at the end, we don't need anything more to have the other direction of the isomorphism, because by definition of m, the left square of the diagram commutes, which give m ○ j = Fj ○ Fm = F(j ○ m) = F(id) = id
I like that when it comes to explaining "algrebra", the terms "endofunctor" and "monoid" are used - again. As if we could say "an algrebra is just a monad, what's the problem"? I'm just kidding, because I honestly don't know what I'm talking about. But I wonder if there could be made another over-my-head statement about algrebras in the likes of "a monad is just a monoid in the category of endofunctors".
Impressive! If functor related to algebra expression like a polynomial, can we imply some rules to create equation, and then illustrate field extension in the language of category theory?
For an endofuctor F, considering two algebras (a, i) and (F a, j), is it always the case that the evaluation of (a, i) is also an homomorphism from (F a, j) to (a, i)? F (F a) -------------> F a | F m | | | | j i | | | | | \/ m \/ F a -------------------> a m and i are the same?
Higher order functions rely on exponential object (or function types, as we call them). I have a video on that. I prefer to introduce recursion through initial algebras, but this is totally equivalent to Y-combinator.
Hi, Bartosz, thanks for the great lectures and book! It took me a while to wrap my head around anamorphisms and I am still not sure whether I understand it correctly. I was confused a bit with the application of Fix as the last step in the definition of ana: ``` ana :: Functor f => (a -> f a) -> a -> Fix f ana coalg = *Fix* . fmap (ana coalg) . coalg ``` IIUC, If I take this definition of Fix ``` newtype Fix f = In (f (Fix f)) ``` It can be gradually expanded into ``` In (f (Fix f)) In (f (In (f (Fix f)))) In (f (In (f (In (f (Fix f)))))) In (f (In (f (In (f (In (f (...)))))))) ``` Fix in the line ``` ana coalg = Fix . fmap (ana coalg) . coalg ``` is the application of data constructor (aka In). As I understand it now, it is needed to match the infinite alternation of `In` and `f` to match definition of `Fix f` (data type, functor fixed point). Is my understanding correct?
45:44 Why the morphism m converts i to Fi? We know, that m converts i to a, but who said a is necessarily equal to Fi? Mr Milewski just wrote Fi without explaining where did it come from
The morphism called m in 45:44 is not the same as the morphism in 42:23. Notice that a few seconds before at 42:41 there is also a morphism a-> b called m. In 42:23 he states the defn. of an initial object so an object i is initial if there is a unique morphism from i to any other object in the category. In 45:44 he says that i is an initial object hence there is exists a unique morphism from i to Fi, that he happened to call m. Fi might not be a, it might be it does not matter, what matters it that we know m exists. (i assume that after 2 years you got it but it might help someone else and it helps me to make things clearer in my head. Farewell.)
@@julianacunha3855 following your reply I listened to this lecture again and this moment was very clear for me now, I would not ask any questions :) Thank you anyway
Suppose for a general Endofunctor F of C there is no Initial Algebra - I think this implies C does not have all limits, otherwise we could find such an algebra - F in such a C can be discontinuous or incomplete in the limit. Isn't that the case for usual "1/(1+x)" algebra on the reals where expressions can result in partial functions #DIV/0 etc.?
A good starting point is this paper: www.iti.cs.tu-bs.de/~adamek/initial.AT.pdf . It goes more into detail about constructing initial algebras and terminal coalgebras.
One issue I run into when describing algebras like this (with fixpoints of functors encoding the signature): With `Fix MonF`, I can't write any simple example expressions, because there is no way to inject a value of the carrier. I can only write boring expressions like `Fix (MAppend (Fix MEmpty) (Fix MEmpty)`, that all evaluate to `MEmpty` The way I usually get around this is by using `Free MonF a` instead, which is precisely the fixpoint of MonF + an injection. This lets me write e.g. `Free (MAppend (Pure 4) (Free (MAppend (Pure 3) (Free MEmpty))))` While this works, it's ... different from what all the literature I've seen talks about. I don't know if I'm missing something?
You're right, Fix MonF generates all binary trees with empty leaves, so there is really nothing to evaluate. You still have some leeway, for instance, you could evaluate all leaves to a fixed number, say 1, but that's not very interesting either. And anyway, since there is no way to impose monoid laws, this is not a real monoid. To really deal with monoids, you'd have to go to Lawvere's theories (which I discuss later). Having said that, what you can do is to parameterize the functor with one additional data type e: data MonF e a = Leaf e | Node a a. Then the fixed point in a will be a binary tree with e-type leaves. You can then define an algebra for (MonF Int a), with the carrier a that's also an Int. It would evaluate Leaf x to x, and Node x y to x+y. A catamorphism for this algebra would sum up all the leaf values. What you did also makes sense: your Pure is just an Int-carrying leaf, and you also have MEmpty leaves that evaluate to zero. The fact that zero is a neutral element is then encoded in the algebra, rather than being the (non-enforceable in Haskell) monoid law.
