dfe*_*uer 9 haskell category-theory free-monoid
据我了解，表达某事物是自由幺半群的一种方法是使用这样的类：
class (Foldable s, forall a. Monoid (s a)) => Sequence s where
singleton :: a -> s a
以及以下“通用建筑”法律：
对于任何Monoid m和任何函数f :: a -> m，
foldMap f . singleton = ffoldMap f 是幺半群态射。foldMap f 是唯一同时满足 1 和 2 的函数。这种理解是否正确？
如果是这样，能够使用这些定律来证明基本的序列属性会很好。我们可以定义
data ViewL s a
= EmptyL
| a :< s a
instance Sequence s => Semigroup (ViewL s a) where
EmptyL <> y = y
x <> EmptyL = x
(x :< xs) <> (y :< ys) = x :< (xs <> singleton y <> ys)
instance Sequence s => Monoid (ViewL s a) where
mempty = EmptyL
viewl :: Sequence s => s a -> ViewL s a
viewl = foldMap (:< mempty)
我将如何显示以下内容？
viewl s = EmptyL ==> s == memptyviewl s == a :< s' <==> s == singleton a <> s'1 的逆直接来自foldMap f于 all 的幺半群态射f，但我真的不知道如何处理上述问题。
foldMap我们将从关于和的几个一般引理开始singleton。第一个引理显然是从 any 的参数性得出的Foldable，但我们可以使用序列的定律直接证明它。
引理（foldMap组合）：假设Sequence s、Monoid m、 和Monoid n。让f :: a -> m是一个函数，让g :: m -> n是一个幺半群态射。然后
g . foldMap @s f = foldMap @s (g . f)
证明：
g . foldMap @s f . singleton @s
= -- foldMap/singleton
g . f
凭借 的独特性foldMap，
g . foldMap @s f = foldMap @s (g . f)
引理（重建）：对于任何Sequence s, foldMap @s (singleton @s) = id @s.
证明：id @s . singleton @s = singleton @s。由于 的独特性foldMap，id @s = foldMap @s (singleton @s).
接下来，我们将以Semigroup (ViewL s a)一种更易于使用的形式重写实例。只需一点等式推理（使用一般case变换和幺半群恒等律）就足以表明以下实例是等效的（忽略惰性，正如我将贯穿始终的那样）。
instance Sequence s => Semigroup (ViewL s a) where
EmptyL <> y = y
(x :< xs) <> v = x :< (xs <> unviewl v)
unviewl :: Sequence s => ViewL s a -> s a
unviewl EmptyL = mempty
unviewl (x :< xs) = singleton x <> xs
引理：unviewl是幺半群态射。
证明：我们必须证明unviewl mempty = mempty对于任何v1和v2, unviewl v1 <> unviewl v2 = unviewl (v1 <> v2)。第一个是微不足道的。
unviewl @s mempty
= -- def of mempty for ViewL s
unviewl @s EmptyL
= -- def of unviewl
mempty
对于第二个，我们按案例进行：
第一种情况：
unviewl (EmptyL <> v2)
= -- definition of <> (or the monoid law)
unviewl v2
= -- monoid law
mempty <> unviewl v2
= -- definition of unviewl
unviewl EmptyL <> unviewl v2
第二种情况：
unviewl ((x :< xs) <> v)
= -- definition of <>
unviewl (x :< (xs <> unviewl v))
= -- definition of unviewl
singleton x <> xs <> unviewl v
= -- definition of unviewl
unviewl (x :< xs) <> unviewl v
接下来，我们证明 和viewl是unviewl（完全）逆的。
引理：unviewl . viewl = id
证明：
unviewl . viewl
= -- definition of viewl
unviewl . foldMap (:< mempty)
= -- foldMap composition lemma and the fact that unviewl
-- is a monoid morphism.
foldMap (unviewl . (:< mempty))
=
foldMap (\x -> unviewl (x :< mempty))
= -- definition of unviewl
foldMap (\x -> singleton x <> mempty)
= -- monoid law and eta reduction
foldMap singleton
= -- rebuilding lemma
id
引理 ( viewlof singleton): 对于任何a, viewl (singleton a) = a :< mempty.
证明：
viewl (singleton a)
= -- definition of viewl
foldMap (:< mempty) (singleton a)
= -- foldMap/singleton law
a :< mempty
引理：viewl . unviewl = id
证明：设v :: ViewL s a. 我们按案例进行v。
第一种情况：
viewl (unviewl EmptyL)
= -- definition of unviewl
viewl mempty
= -- viewl is a monoid morphism (because it is a fold)
mempty
= -- definition of mempty
EmptyL
第二种情况：
viewl (unviewl (x :< xs))
= -- definition of unviewl
viewl (singleton x <> xs)
= -- viewl is a monoid morphism
viewl (singleton x) <> viewl xs
= -- viewl of singleton lemma
(x :< mempty) <> viewl xs
= -- definition of <>
x :< (mempty <> unviewl (viewl xs))
= -- monoid law
x :< unviewl (viewl xs)
= -- by lemma above, unviewl . viewl = id
x :< xs
好的！现在我们已经拥有了所需的所有部件。
推论：如果Sequence s、xs :: s a、 和viewl xs = EmptyL，则xs = mempty。
证明：根据假设，viewl xs = EmptyL. 因此unviewl (viewl xs) = unviewl EmptyL。由于unviewl . viewl = id且根据 的定义unviewl，xs = mempty.
推论：如果Sequence s、x :: a、 和xs :: s a，则viewl (singleton x <> xs) = x :< xs。
证明：
viewl (singleton x <> xs)
= -- viewl is a monoid morphism
viewl (singleton x) <> viewl xs
= -- lemma above
(x :< mempty) <> viewl xs
= -- definition of <>
x :< (mempty <> unviewl (viewl xs))
= -- monoid law and unviewl . viewl = id
x :< xs
推论：如果viewl xs = y :< ys，则xs = singleton y <> ys。
证明：适用unviewl于前提两边，unviewl (viewl xs) = unviewl (y :< ys). 由于unview l . viewl = id且根据 的定义unviewl，该定理成立。
我已经证明了我所设定的一切。在发现这些证明的过程中，我证明了关于 的这个公式的其他一些事情Sequence。我把它们收集在这个要点中。