How Initial encoding is converted to right associated structures?

Question

I am trying to understand Free Structures in Haskell using https://jyp.github.io/posts/free-structures.html, but struggling to understand a paragraph.

 data FreeMonoid t where
  Mappend :: FreeMonoid t -> FreeMonoid t -> FreeMonoid t
  Mempty :: FreeMonoid t
  Embed0 :: t -> FreeMonoid t

However the above ignores the associativity law of monoids. For one, it is possible to distinguish objects on the basis of the association structure of Mappend. One way to take into account associativity is to force one particular association. For example, we can force associating on the right. To take care of the unit law, we also won’t allow Mempty on the left of Mappend. Thus, the only thing that we can do on the left of Mempty is embed. We obtain:

data FreeMonoid t where
  Mappend :: t -> FreeMonoid t -> FreeMonoid t
  Mempty :: FreeMonoid t

What observation makes us to tell a structure is ignoring laws? How the second structure has embedded right associativity & I thought in Haskell we will prove laws by writing tests or embedding the laws in the implementation itself as I wrote mappend below. Can we prove the laws in types also? I mean the Mappend in the second structure I can safely ignore t & give the result as second parameter.

-- Left identity
mappend mempty x = x
-- Right identity
mappend x mempty = x
-- Associativity of mappend
mappend x ( mappend y z) = mappend ( mappend x y ) z

Edit:

https://www.schoolofhaskell.com/user/bss/magma-tree This link explained why to choose List like Free Monoid over Tree like Free Monoid by ensuring the Laws on the structure which is formed from Initial encoding.

Answer 1

In the first type, Mappend x (Mappend y z) and Mappend (Mappend x y) z are different values which can be distinguished from each other (using pattern matching, for example, can distinguish between the two).

To give a concrete example, consider this (note that mappend = Mappend in this case)

data NotQuiteFreeMonoid t where
  Mappend :: NotQuiteFreeMonoid t -> NotQuiteFreeMonoid t -> NotQuiteFreeMonoid t
  Mempty :: NotQuiteFreeMonoid t
  Embed0 :: t -> NotQuiteFreeMonoid t

x, y :: NotQuiteFreeMonoid Char
x = Mappend (Mappend (Embed0 'a') (Embed0 'b')) (Embed0 'c')
y = Mappend (Embed0 'a') (Mappend (Embed0 'b') (Embed0 'c'))

f :: NotQuiteFreeMonoid Char -> Int
f (Mappend (Mappend _ _) _) = 1
f _                         = 0

Note that the expression f x gives 1 while f y gives 0.

If we write mappend instead using the second type, we arrive at a definition which can be shown to be associative. It looks like that implementation is not given in that article and the second type should really not have the name Mappend for one of its data constructors, but you can write a (associative) mappend implementation for the second type.