【问题标题】:What is the identity of the type?类型的身份是什么?
【发布时间】:2017-06-26 14:25:38
【问题描述】:

我有以下数据类型:

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类型的标识是什么?

【问题讨论】:

  • 这取决于您希望如何实现mappend

标签: haskell math monoids


【解决方案1】:

简答:它取决于mappend 函数

Bull 类型的标识是什么? Bool类型的标识是什么?

一个类型没有“固有”身份身份元素仅存在于关于二元函数(此处为mappend) ,比如Wikipedia article says

在数学中,单位元素或中性元素是集合中相对于该集合上的二元运算的一种特殊类型的元素,当与其他元素组合时,它不会改变其他元素。 p>

所以这取决于mappend是什么操作。

如果是Bool,如果我们定义mappend = (&&),那么identity 元素就是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 documentation on Monoid 所说,它应该满足以下规则:

mappend mempty x = x

mappend x mempty = x

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

mconcat = foldr mappend mempty

这些规则并不是为 Haskell “发明”的:monoid 是众所周知的algebraic structure。通常在数学中,幺半群表示为 3 元组。例如 (N, +, 0) 其中 N 是这里的集合(例如自然数),+ 是二元函数,而 0 标识元素。

【讨论】:

    【解决方案2】:

    这是一个很好的问题,我之前已经玩过好几次了。事实上,这是我想出的universe 的第一个用法,我仍然认为它是一个简洁的用法。所以让我告诉你!

    这里的想法是:我们将使用 Universe 包来枚举 所有 memptymappend 的可能实现,然后检查哪些满足法律。首先,一些样板:

    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。你可以认为这有点像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 提供了 AllAny 半群,当您希望 mappend 分别为 (&&)(||) 时。据我所知,没有合适的新类型来获取 xor 或其否定作为Monoid;但是您可以通过为Bool 声明一个Num 实例来伪造它(使用Word1 直觉,False 为0,True 为1)通过Sum Bool 获取它。

    其次,这里的另一个答案是:data Color = Red | Green | Blue 有什么幺半群?我们现在有所有的机器来回答这个问题,并确认实际上存在相当多的幺半群:

    > length monoidsOnColor
    33
    

    我鼓励您尝试构建将它们全部列出的代码,并仔细研究它们,看看您可以获得什么见解!

    【讨论】:

      【解决方案3】:

      对于给定的集合(或类型,在 Haskell 中)没有一个单一的幺半群。事实上,幺半群中的身份不是由定义它的集合决定的,而是由操作决定的(在 Haskell 中称为mappend)。例如,整数上的幺半群可以定义为加法(标识为0)或乘积(标识为1)。

      这就是SumProduct 类型存在的原因:因为Monoid 类型类在Num a => a 的集合上有多种可能的实现,我们更愿意将它包装成newtype 并定义包装类型上的 Monoid 实现。

      Bool 类型也有类似的构造,All 是布尔值上的幺半群((&&)),身份为 TrueAny 是布尔值上的幺半群((||))身份为False。事实上,布尔值可以在许多其他操作(例如 XOR 和 XNOR 门)上形成幺半群。

      由于Bull 类型与Bool 类型同构(两者都有两个空构造函数),您可以从Bool 上的Monoid 实现中获得启发,但我们无法确定哪种实现最适合在你的情况下有更多的背景。

      另外,正如 Anton Xue 所提到的,即使您可以Bull 定义一个幺半群,这真的有意义吗?你的类型应该代表什么?

      【讨论】:

      • 这只是haskellbook中的一个展示案例。感谢您的回答。
      猜你喜欢
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 2011-09-20
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 2010-10-23
      相关资源
      最近更新 更多