如何基于自由幺半群定律证明Haskell Sequence类的基础序列性质

认知正确性判断 #

你的认知完全正确，该类型类加三条定律恰好是自由幺半群泛性质的Haskell编码：

• 自由幺半群的核心性质就是对任意目标幺半群m，任意从元素到m的映射f，都存在唯一的幺半群同态将f延拓到整个幺半群结构上
• 这里的singleton就是泛性质里的单位映射η : a → s a，foldMap f就是唯一的延拓同态，三条定律和泛性质完全等价。

预备引理 #

证明前先推导两个核心预备结论：

引理1：foldMap singleton = id #

根据Sequence定律：

1. foldMap singleton是幺半群同态（定律2）
2. 对任意x，foldMap singleton (singleton x) = singleton x（定律1）
   而恒等函数id也满足：

• id是幺半群同态（id mempty = mempty，id (x<>y) = id x <> id y）
• id (singleton x) = singleton x
  由唯一性定律3，可得foldMap singleton = id。

引理2：定义g :: ViewL s a -> s a为 #

g EmptyL = mempty
g (x :< xs) = singleton x <> xs

则有：

1. g是幺半群同态
2. g . viewl = id

证明：

1. 证明g是同态

• 单位元保持：g mempty = g EmptyL = mempty，成立
• 运算保持：分三种情况
  • 左为空：g (EmptyL <> v) = g v = mempty <> g v = g EmptyL <> g v
  • 右为空：g (v <> EmptyL) = g v = g v <> mempty = g v <> g EmptyL
  • 两边均为cons：g ((x:<xs) <> (y:<ys)) = g (x :< (xs <> singleton y <> ys)) = singleton x <> xs <> singleton y <> ys = (singleton x <> xs) <> (singleton y <> ys) = g (x:<xs) <> g (y:<ys)
    因此g是幺半群同态。

2. 证明g . viewl = id

首先viewl = foldMap (\x -> x :< mempty)，记f_view x = x :< mempty，则：

• g . foldMap f_view是两个幺半群同态的复合，因此也是同态
• 对任意x：(g . foldMap f_view) (singleton x) = g (f_view x) = g (x :< mempty) = singleton x <> mempty = singleton x
  由唯一性定律3，满足“是同态且h . singleton = singleton”的函数只有foldMap singleton = id，因此g . viewl = id。

命题证明 #

命题1：viewl s = EmptyL ==> s == mempty #

证明：
假设viewl s = EmptyL，两边同时应用g：

g (viewl s) = g EmptyL

由引理2的g . viewl = id，左边等于s；右边g EmptyL = mempty，因此直接得s = mempty。

命题2：viewl s == a :< s' <==> s == singleton a <> s' #

双向分别证明：

从左到右（==>）

假设viewl s = a :< s'，两边同时应用g：

g (viewl s) = g (a :< s')

左边等于s，右边g (a:<s') = singleton a <> s'，因此直接得s = singleton a <> s'。

从右到左（<==）

假设s = singleton a <> s'，首先由引理2可知g是单射：

若g u = g v，则u = viewl (g u) = viewl (g v) = v

计算g作用在viewl s和a:<s'上的结果：

• g (viewl s) = s = singleton a <> s'
• g (a :< s') = singleton a <> s'
  两者g的结果相等，由g的单射性可得viewl s = a :< s'。

内容的提问来源于stack exchange，提问作者dfeuer