haskell - 初始编码如何转换为正确的关联结构？

Question

我正在尝试使用 https://jyp.github.io/posts/free-structures.html 来理解 Haskell 中的自由结构，但很难理解一个段落。

 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

什么观察让我们判断一个结构忽略了定律？第二个结构如何嵌入右关联性&我认为在 Haskell 中我们将通过编写测试或将定律嵌入到实现本身中来证明定律，正如我在下面编写的 mappend 一样。我们也能证明类型定律吗？我的意思是第二个结构中的 Mappend 我可以安全地忽略 t 并将结果作为第二个参数。

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

编辑:

https://www.schoolofhaskell.com/user/bss/magma-tree此链接解释了为什么选择像 Free Monoid 这样的 List 而不是像 Free Monoid 这样的 Tree，因为确保了初始编码形成的结构的规律。

Answer 1

在第一种类型中，Mappend x (Mappend y z) 和 Mappend (Mappend x y) z 是可以彼此区分的不同值(使用模式匹配，例如，可以区分两者)。

为了给出一个具体的例子，请考虑这个(请注意，在本例中，mappend = Mappend)

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

请注意，表达式 f x 给出 1，而 f y 给出 0。

如果我们编写 mappend 而不是使用第二种类型，我们就会得到一个可以证明是关联的定义。看起来该文章中没有给出该实现，并且第二种类型的数据构造函数之一实际上不应该具有名称 Mappend ，但您可以编写一个(关联的)mappend code> 第二种类型的实现。