Options

Question 3.5 - Monoids as List algebras

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

  • 1.
    edited February 1

    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

    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
  • 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."
  • 3.
    edited February 4

    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...
  • 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.)
  • 5.
    edited February 3

    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?
  • 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...
  • 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.
  • 8.

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

    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`.
  • 9.
    edited February 4

    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.
  • 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))`.
Sign In or Register to comment.