It looks like you're new here. If you want to get involved, click one of these buttons!
Recall that the monad List: \(Set \rightarrow Set\) that sends a set X to the set of lists of elements of X, whose multiplication flattens a list of lists, and whose unit takes an element \(x \in X\) to the singleton list [x] \(\in\) List(X).
(a) Given a List-algebra \(a: List(X) \rightarrow X\), construct a monoid on the set X.
(b) Given a monoid (X,*,e), construct a list algebra
(c) Show that your two constructions are inverses (we hope they are!)
Comments
I don't know if I quite get what this question is asking. Is it to map the components of the List Algebra to a Monoid and vice-versa?
For example:
a) List(X) = 1 + A.X
\( 1 \mapsto e \)
\( . \mapsto * \)
or in Haskell
I don't know if I quite get what this question is asking. Is it to map the components of the List Algebra to a Monoid and vice-versa? For example: a) List(X) = 1 + A.X \\( 1 \mapsto e \\) \\( . \mapsto * \\) or in Haskell > alg2monoid :: Algebra a -> Monoid a > alg2monoid Nil = mempty > alg2monoid (Cons a x) = a <> xThis is what David Spivak told me: "In Set, an algebra for the list monad is a set X together with a function mult : List X -> X satisfying unitality and associativity. There is an equivalence between the category of monoids and the category of List-algebras. Note that we are using non-infinite lists here."
This is what David Spivak told me: "In Set, an algebra for the list monad is a set X together with a function mult : List X -> X satisfying unitality and associativity. There is an equivalence between the category of monoids and the category of List-algebras. Note that we are using non-infinite lists here."Apparently a List-algebra is a kind of monad algebra. According to nlab, we have the following axioms for a monad algebra \(a : T A \to A\):
\[ a \circ \eta = id \\ a \circ T a = a \circ \mu \]
In Haskell, these laws would be:
(a) Here's how I would do this in Haskell
Here's a prove that
(<>)associates:And
mempty <> x = x <> mempty = x:(b) Here's the other way around:
You could write
Data.Foldable.foldasfoldr (<>) mempty(which is what its default definition reduces to).Let's check the unital law:
The associative law is more complicated:
(c) Maybe later...
Apparently a List-algebra is a kind of monad algebra. According to [nlab](https://ncatlab.org/nlab/show/algebra+over+a+monad), we have the following axioms for a monad algebra \\(a : T A \to A\\): \\[ a \circ \eta = id \\\\ a \circ T a = a \circ \mu \\] In Haskell, these laws would be: a . return = id (unitality) a . fmap a = a . join (associativity) (a) Here's how I would do this in Haskell {-# LANGUAGE FlexibleInstances, UndecidableInstances #-} import qualified Data.Foldable class ListAlg a where alg :: [a] -> a instance ListAlg a => Semigroup a where x <> y = alg ([x] ++ [y]) instance ListAlg a => Monoid a where mempty = alg [] Here's a prove that `(<>)` associates: (x <> y) <> z = alg ([alg ([x] ++ [y])] ++ [z]) = alg [alg [x,y], z] = alg [alg [x,y], alg [z]] (by unitality) = alg . fmap alg $ [[x,y],[z]] = alg . join $ [[x,y],[z]] (by associativity) = alg [x,y,z] = alg . join $ [[x],[y,z]] = alg . fmap alg $ [[x],[y,z]] (by associativity) = alg [alg [x], alg [y,z]] = alg [x, alg [y,z]] (by unitality) = alg ([x] ++ alg ([y] ++ [z])) = x <> (y <> z) And `mempty <> x = x <> mempty = x`: mempty <> x = alg [alg [], x] = alg [alg [], alg [x]] = alg . fmap alg $ [[],[x]] = alg . join $ [[],[x]] = alg [x] = x = alg . join $ [[x],[]] = alg . fmap alg $ [[x],[]] = alg $ [alg [x], alg []] = alg $ [x, alg []] = x <> mempty (b) Here's the other way around: instance Monoid a => ListAlg a where alg = Data.Foldable.fold You could write `Data.Foldable.fold` as `foldr (<>) mempty` (which is what its default definition reduces to). Let's check the unital law: alg [a] = foldr (<>) mempty [a] = a <> mempty = a The associative law is more complicated: alg . fmap alg $ [[x1, x2, ...], [y1, y2, y3, ...], ...] = foldr (<>) mempty $ [alg [x1, x2, ...], alg [y1, y2, ...], ...] = alg [x1, x2, ...] <> alg [y1, y2, ...] <> ... <> mempty = x1 <> x2 <> ... <> mempty <> y1 <> y2 <> ... <> mempty <> ... <> mempty = x1 <> x2 <> ... <> y1 <> y2 <> ... <> ... <> mempty = alg [x1, x2, ..., y1, y2, ..., ...] = alg . join $ [[x1, x2, ...], [y1, y2, ...], ...] (c) Maybe later...I'm a little confused about how to do this in a way such that the two constructions are strictly inverses of each other (as per 5c). In particular, when I go from the carrier type of the list, X, to the set for the monoid, I had to modify it to be 1 + X instead of X. Because how else am I going to guarantee that my monoid set has a unit in it?
(I assume that the function associated with the list algebra uses identity on the carrier type when the second parameter is the empty list.)
I'm a little confused about how to do this in a way such that the two constructions are strictly inverses of each other (as per 5c). In particular, when I go from the carrier type of the list, X, to the set for the monoid, I had to modify it to be 1 + X instead of X. Because how else am I going to guarantee that my monoid set has a unit in it? (I assume that the function associated with the list algebra uses identity on the carrier type when the second parameter is the empty list.)I'm also a bit confused by the exact terminology used around list algebras. In the course notes we have:
So, if I'm reading that right, a
ListAlgwith type paramsaandbis a function from the functorListF a, applied tob, tob, or in other words(ListF a b) -> b.Notably, it's not a function from
List a(akaFix (ListF a)) tob. My understanding is that if we want a function fromList atob, we have to take the catamorphism of the list algebra.However, this problem statement seems to define the list algebra as a function from List(X) to X, which looks like it should translate to
List x -> x. But this is what you'd get if you took the catamorphism of aListAlg x xlist algebra. It's not the list algebra itself.Is the problem statement just being a bit loose with the terminology, such that when it says the list algebra is List(X) -> X, it really means that that's the catamorphism of the list algebra? Or am I missing something?
I'm also a bit confused by the exact terminology used around list algebras. In the course notes we have: data ListF a x = NilF | ConsF a x deriving Functor type List a = Fix (ListF a) type Algebra f a = f a -> a type ListAlg a b = Algebra (ListF a) b So, if I'm reading that right, a `ListAlg` with type params `a` and `b` is a function from the functor `ListF a`, applied to `b`, to `b`, or in other words `(ListF a b) -> b`. Notably, it's *not* a function from `List a` (aka `Fix (ListF a)`) to `b`. My understanding is that if we want a function from `List a` to `b`, we have to take the catamorphism of the list algebra. However, this problem statement seems to define the list algebra as a function from List(X) to X, which looks like it should translate to `List x -> x`. But this is what you'd get if you took the catamorphism of a `ListAlg x x` list algebra. It's not the list algebra itself. Is the problem statement just being a bit loose with the terminology, such that when it says the list algebra is List(X) -> X, it really means that that's the catamorphism of the list algebra? Or am I missing something?@EricRogstad - As far as I know the puzzle doesn't have anything to do with initial F-algebras. I think the type for a list algebra should just be
[a] -> a. There's no need to take any fixedpoints.Let me keep going with (c). In order to show the two operations are inverses, we need to show:
alg = foldr (\x y -> alg [x,y]) (alg [])(ie, turning an list algebra into a monoid and converting it back gets us the original list algebra)Two parts:
a.
(<>) = \ x y -> foldr (<>) mempty [x,y]b.
mempty = foldr (<>) mempty []So (1) is annoying but (2) is super easy.
2a. Showing
(<>) = \x y -> foldr (<>) mempty [x,y]is the same as showingx <> y = foldr (<>) mempty [x,y]. But we have:2b. In one step of evaluation we have
foldr (<>) mempty [] = mempty, so we're done.Showing (1) requires more work, and we may need to lean on associativity/unitality...
@EricRogstad - As far as I know the puzzle doesn't have anything to do with initial F-algebras. I think the type for a list algebra should just be `[a] -> a`. There's no need to take any fixedpoints. Let me keep going with (c). In order to show the two operations are inverses, we need to show: 1. `alg = foldr (\x y -> alg [x,y]) (alg [])` (ie, turning an list algebra into a monoid and converting it back gets us the original list algebra) 2. Two parts: a. `(<>) = \ x y -> foldr (<>) mempty [x,y]` b. `mempty = foldr (<>) mempty []` So (1) is annoying but (2) is super easy. 2a. Showing `(<>) = \x y -> foldr (<>) mempty [x,y]` is the same as showing `x <> y = foldr (<>) mempty [x,y]`. But we have: foldr (<>) mempty [x,y] = x <> y <> mempty = x <> y 2b. In one step of evaluation we have `foldr (<>) mempty [] = mempty`, so we're done. Showing (1) requires more work, and we may need to lean on associativity/unitality...@MatthewDoty This contradicts the definition given in the course notes. That's what I'm confused about.
> As far as I know the puzzle doesn't have anything to do with initial F-algebras. I think the type for a list algebra should just be [a] -> a. @MatthewDoty This contradicts the definition given in the course notes. That's what I'm confused about.@EricRogstad
In the video lectures they defined:
data ListInt x = Nil | Cons Int x deriving FunctorThe definition of
data ListF a x = NilF | ConsF a x deriving Functorjust generalize the
ListIntdefinition to any type, not justInt.So instead of an Algebra
ListInt x -> xwe would haveListF a x -> x. With this definition we can create aListIntwithListF Int xor aListStringwithListF String x, etc.In other words, the notation ( List(X) \rightarrow X ) corresponds to
ListF a x -> x.@EricRogstad In the video lectures they defined: ` data ListInt x = Nil | Cons Int x deriving Functor ` The definition of ` data ListF a x = NilF | ConsF a x deriving Functor ` just generalize the `ListInt` definition to any type, not just `Int`. So instead of an Algebra `ListInt x -> x` we would have `ListF a x -> x`. With this definition we can create a `ListInt` with `ListF Int x` or a `ListString` with `ListF String x`, etc. In other words, the notation \( List(X) \rightarrow X \) corresponds to `ListF a x -> x`.Well, they did say at the top:
So the question clearly is concerned with
a : [x] -> x, right?You can find more notes on monoid-algebras in Chapter 10 of Awodey's Category Theory and nlab
Remember: an F-algebra is just a function
a : f a -> awherefis a functor. This problem demands a little more structure, as Bartosz was saying. So we need those extra rules I was mentioning.> > As far as I know the puzzle doesn't have anything to do with initial F-algebras. I think the type for a list algebra should just be `[a] -> a`. > > @MatthewDoty This contradicts the definition given in the course notes. That's what I'm confused about. Well, they did say at the top: > (a) Given a List-algebra \\(a : List(X)\to X\\), construct a monoid on the set \\(X\\). So the question clearly is concerned with `a : [x] -> x`, right? You can find more notes on monoid-algebras in [Chapter 10 of Awodey's _Category Theory_](https://www.andrew.cmu.edu/course/80-413-713/notes/chap10.pdf) and [nlab](https://ncatlab.org/nlab/show/algebra+over+a+monad) Remember: an F-algebra is just a function `a : f a -> a` where `f` is a functor. This problem demands a little more structure, as Bartosz was saying. So we need those extra rules I was mentioning.Indeed, this is a bit confusing. In the lecture, we talked about the list functor as
ListF a x = NilF | ConsF a x. It is actually a bifunctor, so its fixed point is a functor ina. The starting point of the exercise can be written asList a = Nil | Cons a (List a), so you may think of it as the fixed point ofListF.Listis a functor, so you can define an algebra for it:alg :: List a -> a. It is also a monad, so you can define a monad algebra for it, which is just an algebra with additional laws. These laws make the setainto a monoid, with unitalg Niland multiplicationalg (Cons x (Cons y Nil)).Indeed, this is a bit confusing. In the lecture, we talked about the list functor as `ListF a x = NilF | ConsF a x`. It is actually a bifunctor, so its fixed point is a functor in `a`. The starting point of the exercise can be written as `List a = Nil | Cons a (List a)`, so you may think of it as the fixed point of `ListF`. `List` is a functor, so you can define an algebra for it: `alg :: List a -> a`. It is also a monad, so you can define a monad algebra for it, which is just an algebra with additional laws. These laws make the set `a` into a monoid, with unit `alg Nil` and multiplication `alg (Cons x (Cons y Nil))`.