Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Options

Question 3.5 - Monoids as list algebras

edited June 2020

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!)

• Options
1.
edited February 2020

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 *$$

alg2monoid :: Algebra a -> Monoid a

alg2monoid Nil = mempty

alg2monoid (Cons a x) = a <> x

Comment Source: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 <> x
• Options
2.

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."

Comment Source: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."
• Options
3.
edited February 2020

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 . 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... Comment Source: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...
• Options
4.

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.)

Comment Source: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.)
• Options
5.
edited February 2020

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?

Comment Source: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?
• Options
6.

@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...

Comment Source:@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...
• Options
7.

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.

Comment Source:> 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.
• Options
8.

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.

Comment Source:@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.
• Options
9.
edited February 2020

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 and nlab

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.

Comment Source:> > 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.
• Options
10.

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)).

Comment Source: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)).