首页 文章

自由组monad

提问于
浏览 次
14

在类别理论中，monad是两个伴随函子的组合 . 例如，Maybe monad是由遗忘函子组成的自由尖集函子 . 同样，List monad是由健忘的仿函数组成的免费monoid仿函数 .

Monoid是最简单的代数结构之一，所以我想知道编程是否可以从更复杂的代数中受益 . 我没有在标准的Haskell包中找到自由组monad，所以我将在这里定义它

data FreeGroup a = Nil | PosCons a (FreeGroup a) | NegCons a (FreeGroup a)

== 运算符定义为 NegCons x (PosCons x y) == y . 因此，在 length :: FreeGroup a -> Int 中，每个 PosCons 被计数1并且每个 NegCons -1（它是Int的唯一组态射，其在每个PosCons上的值为1） .

在列表（自由幺半群）中， concat 只是乘法而 map 是函数的函数提升 . 所以 FreeGroup 的monad实例与 List 完全相同 .

自由组monad是否有任何编程用途？此外，通常会将monad解释为上下文中的值：对于 List ，上下文将是选择或不确定性 . 对于自由组monad有这样的解释吗？

免费铃声和向量空间（总是免费的）怎么样？

对于任何代数结构 S ，categorical free functor FS :: Set -> S 的存在意味着存在一个函数Haskell调用fold：

foldS :: S s => (a -> s) -> FS a -> s

它在 a 的基础上将一个函数提升为自由对象 FS a 上的 S -morphism . 通常的 foldr 函数是 foldMonoid 的一个特殊化（在Haskell中称为 foldMap ，由于某些原因我不太了解），monoid是函数集合 b -> b ，其组合为乘法 .

为了完整起见，这里是 FreeGroup 的monad实例：

mult :: FreeGroup a -> FreeGroup a -> FreeGroup a
mult Nil x = x
mult x Nil = x
mult (PosCons x y) z = PosCons x (mult y z)
mult (NegCons x y) z = NegCons x (mult y z)

inverse :: FreeGroup a -> FreeGroup a
inverse Nil = Nil
inverse (PosCons x y) = mult (inverse y) (NegCons x Nil)
inverse (NegCons x y) = mult (inverse y) (PosCons x Nil)

groupConcat :: FreeGroup (FreeGroup a) -> FreeGroup a
groupConcat Nil = Nil
groupConcat (PosCons x l) = mult x (groupConcat l)
groupConcat (NegCons x l) = mult (inverse x) (groupConcat l)

instance Functor FreeGroup where
  fmap f Nil = Nil
  fmap f (PosCons x y) = PosCons (f x) (fmap f y)
  fmap f (NegCons x y) = NegCons (f x) (fmap f y)

instance Applicative FreeGroup where
  pure x = PosCons x Nil
  fs <*> xs = do { f <- fs; x <- xs; return $ f x; }

instance Monad FreeGroup where
  l >>= f = groupConcat $ fmap f l
haskell monads category-theory

1 回答

  • 1

    “自由组monad是否有任何编程用途？”

    由于过去四个月缺乏答案，我认为答案是“不，不是真的” . 但这是一个有趣的问题，因为它基于基本的数学概念，在我看来（也）它应该 .

    首先我注意到，建议的自由组功能也可以很容易地实现一个a a a a，

    type FreeGroupT a = [Either a a]

fgTofgT :: FreeGroup a -> FreeGroupT a
fgTofgT Nil = []
fgTofgT (a :+: as) = Right a : fgToList as
fgTofgT (a :-: as) = Left a : fgToList as

fgTTofg :: FreeGroupT a -> FreeGroup a
fgTTofg [] = Nil
fgTTofg (Right a : as) = a :+: fgTTofg as
fgTTofg (Left a : as) = a :-: fgTTofg as

--using (:-:) instead of NegCons
--and   (:+:) instead of PosCons

    这是一个很好的定义，因为我们确保我们的自由组只是一个具有一点额外结构的幺半群 . 它呼吁自由群体只是一个自由幺半群的组合与另一个仿函数（名称是什么？不是一个b bifunctor而是一个仿函数F a = L a | R a） . 我们还确保自由组monad实例与自由monoid的monad实例一致 . 也就是说，自由组上的monad操作的条件恰好都是正数，应该像自由monoid上的monad一样，对吗？

    但最终，如果我们想要减少逆，我们需要 Eq a 实例 . 我们需要在学期一级工作，纯类型信息是不够的 . 这使得自由幺半群和自由群体之间的类型级别区别无益 - 据我所见 . 至少没有依赖打字 .

    为了讨论实际的编程用法，我将尝试（但失败）提供一个似是而非的用例 .

    想象一下一个文本编辑器，它使用"Ctrl"键来指示命令序列 . 按住"Ctrl"时按下的任何键序列都被建模为FreeGroup中的负数（负缺点（： - :)） . 因此，可以使用自由组术语 'a':+:'b':+:'b':-:'a':-:[] 来模拟写入"ab"的emacs行为，将光标移回字符，然后移动到行的开头 . 这样的设计很好 . 我们可以轻松地在流中嵌入命令和宏，而不需要一些特殊的保留转义字符 .

    但是，此示例作为正确的用例失败，因为我们希望 'a':+:'b':+:'b':-:'a':-:[] 与 [] 是相同的程序，但事实并非如此 . 而且，它很容易，只需将每个列表术语包装在Either中，如上所述 .

    回复于

相关问题