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