这种类型的身份是什么？

Question

我有以下数据类型:

data Bull = Fools
  | Twoo
  deriving (Eq, Show)

并使用Monoid实现它:

instance Monoid Bull where
  mempty = Fools
  mappend _ _ = Fools

如您所见,mempty身份法不具备的身份功能:

*Main> x = Twoo
*Main> mappend mempty x == x

什么是Bull类型的身份？什么是Bool类型的身份？

Answer 1

简答:这取决于mappend功能.

什么是Bull类型的身份？什么是Bool类型的身份？

一个类型没有"固有的"标识,一个标识元素只存在于二元函数(这里mappend),就像维基百科的文章所说:

在数学中,标识元素或中性元素是关于该集合上的二元操作的集合的特殊类型元素,当与它们组合时,其他元素保持不变.

所以它取决于什么mappend是操作.

在的情况下,Bool如果我们定义mappend = (&&),那么身份元素mempty = True.但是,如果我们选择mappend = (||),那么mempty = False.

你instance Moniod Bull的不对.由于它不能满足财产:

mappend mempty x = x

如果我们选择Fools的mempty = Fools,那么mappend Fools Twoo应该是Twoo.如果我们选择mempty = Twoo,那么mappend Twoo Twoo仍然没有Twoo.

要点Monoid是你必须仔细设计二元运算符.就像Haskell文档中Monoid说的那样,它应该满足以下要求:

mappend mempty x = x

mappend x mempty = x

mappend x (mappend y z) = mappend (mappend x y) z

mconcat = foldr mappend mempty

这些规则并非为Haskell"发明":幺半群是众所周知的代数结构.通常在数学中,幺半群表示为3元组.例如(N,+,0),其中N设置在这里(例如自然数),+二进制函数,0是标识元素.

Answer 2

这是一个很好的问题,也是我以前玩过几次的问题.事实上,它是我曾经想到的宇宙的第一次使用之一,我仍然认为它是一个整洁的.所以,让我告诉你!

这里的想法:我们要使用乾坤包枚举所有的可能的实现mempty和mappend,然后检查哪些满足法律.首先,一些样板:

import Data.Universe
import Data.Universe.Instances.Reverse

data Bull = Fools | Twoo deriving (Bounded, Enum, Eq, Ord, Read, Show)
instance Universe Bull
instance Finite Bull

这只是导入包的适当位并定义您的类型.现在,让我们编写幺半群法则.我们希望我们mappend成为联想; 写(+)的mappend,我们可以要求:

associative        (+) = all (\(x,y,z) -> (x+y)+z == x+(y+z)) universe

身份的法律是非常相似的对方,我们连接mappend到我们的mempty(我们称之为(+)和zero这里):

leftIdentity  zero (+) = all (\x -> zero+x == x) universe
rightIdentity zero (+) = all (\x -> x+zero == x) universe

幺半群应该满足所有三个法则:

monoid (zero, (+)) = associative (+) && leftIdentity zero (+) && rightIdentity zero (+)

现在我们可以通过过滤掉符合法律的那些来构建所有幺半群的列表:

monoidsOnBull :: [(Bull, Bull -> Bull -> Bull)]
monoidsOnBull = filter monoid universe

我们来看看ghci:

> mapM_ print monoidsOnBull
(Twoo,[(Fools,[(Fools,Fools),(Twoo,Fools)]),(Twoo,[(Fools,Fools),(Twoo,Twoo)])])
(Fools,[(Fools,[(Fools,Fools),(Twoo,Twoo)]),(Twoo,[(Fools,Twoo),(Twoo,Fools)])])
(Twoo,[(Fools,[(Fools,Twoo),(Twoo,Fools)]),(Twoo,[(Fools,Fools),(Twoo,Twoo)])])
(Fools,[(Fools,[(Fools,Fools),(Twoo,Twoo)]),(Twoo,[(Fools,Twoo),(Twoo,Twoo)])])

(旁白:我们应该如何读取这个输出？嗯,Universe包a -> b通过显示类型图来显示类型的函数[(a, b)],即输入和输出对的列表.上面输出的每一行都是一个适合的元组mempty.第一部分和mappend第二部分适用.)

那么这些幺半群会做什么呢？我们一次带一个:

(Twoo,[(Fools,[(Fools,Fools),(Twoo,Fools)]),(Twoo,[(Fools,Fools),(Twoo,Twoo)])])

这里mappend输出Fools除非两个输入都是Twoo.也就是说,这Bull相当于(&&).(&&)是True- 或者Twoo,在Bull案件中的身份.

(Fools,[(Fools,[(Fools,Fools),(Twoo,Twoo)]),(Twoo,[(Fools,Twoo),(Twoo,Fools)])])

此mappend输出Fools如果其两个输入是相等的,和Twoo以其他方式.您可以将此视为xor on Bool,或者是1位数字的两个补码.它的身份是Fools(或零).

(Twoo,[(Fools,[(Fools,Twoo),(Twoo,Fools)]),(Twoo,[(Fools,Fools),(Twoo,Twoo)])])

这个就像最后一个,但到处都是否定的.

(Fools,[(Fools,[(Fools,Fools),(Twoo,Twoo)]),(Twoo,[(Fools,Twoo),(Twoo,Twoo)])])

这个就像第一个,但到处都是否定的.这也恰好就像(||)上Bool,它具有身份False.

这结束了讲座,但还有另外两个值得添加的有趣笔记.

首先,base提供All和Any幺当你希望你mappend是(&&)和(||)分别.据我所知,没有一个合适的新类型可以得到xor或它的否定作为Monoid; 但是你可以通过声明一个Num实例Bool(使用Word1直觉False为0并且True为1)来伪造它Sum Bool.

第二,这里的另一个答案是:有什么幺半群data Color = Red | Green | Blue？我们现在有了解决这个问题的所有机制,并确认实际上存在相当多的幺半位:

> length monoidsOnColor
33

我鼓励您尝试构建将所有列表全部列出的代码并通过它们来查看您可以获得的见解!