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

- All Categories 2.3K
- Chat 494
- ACT Study Group 5
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 1
- Strategy 110
- Azimuth Project 1.1K

Options

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 <> x`

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

`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.fold`

as`foldr (<>) 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

`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

nota 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?

`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 showing`x <> 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 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`

.`@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 Theoryand nlabRemember: 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.`> > 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 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))`

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