【问题标题】:MonadFix instance for PutPut 的 MonadFix 实例
【发布时间】:2012-06-19 13:45:59
【问题描述】:

一个简单的问题,我希望:binary 包定义了两种类型,Get and Put。前者本质上是一个状态单子,后者本质上是一个作家。 state 和 writer 都有合理的 MonadFix 实例,所以我希望 GetPut 也可以。

Get 可以。 Put 没有。那么,是否可以为Put(真的为PutM)定义一个合适的MonadFix 实例?

一个更普遍的问题是:通常如何验证一个类型类实例是否真正满足该类型类的规则?

【问题讨论】:

  • 如何验证一个类型类是否满足定律:写下你要验证的方程,代入函数的定义,然后求值。这会导致两个相等的术语吗?如果是,则符合法律规定;否则,不。

标签: haskell typeclass monadfix


【解决方案1】:

正如您在二进制包 (Data.Binary.Put:71) 的源代码中看到的,用于一元值的数据结构在构建器中是严格的。由于从 monad 中提取值必须强制找到值所在的结构,如果构建器依赖于输入,这将导致无限循环。

data PairS a = PairS a !Builder
newtype PutM a = Put { unPut :: PairS a }

所以你可以写一个MonadFix 实例,但是你不能用它做任何有用的事情。但我不认为你可以在这里用MonadFix 做任何有用的事情,至少你不能用普通的旧fix 做任何事情,因为PutM monad 基本上是Writer Builder(但有一个专门的实施)。

至于你的第二个问题,它与第一个无关,所以你应该把它作为一个单独的问题来问。

【讨论】:

  • 作为一个实验,我刚刚编写了以下似乎可行的实例:instance MonadFix PutM where mfix f = let (a, b) = runPutM $ f a in (putLazyByteString b >> return a)。这应该工作吗?我是不是很傻?
  • 如果你能证明它遵循 MonadFix 法则,那么看起来我错了 MonadFix 是不可能的。但是,实现它没有意义,因为无论如何您都可以使用常规的fix
【解决方案2】:

这是对第二个问题的回答,也是对 Daniel 评论的跟进。您手动验证法律,我将使用Functor 法律的示例为Maybe

-- First law
fmap id = id

-- Proof
fmap id
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just (id a)
= \x -> case x of
    Nothing -> Nothing
    Just a -> Just a
= \x -> case x of
    Nothing -> x
    Just a  -> x
= \x -> case x of
    _ -> x
= \x -> x
= id

-- Second law
fmap f . fmap g = fmap (f . g)

-- Proof
fmap f . fmap g
= \x -> fmap f (fmap g x)
= \x -> fmap f (case x of
    Nothing -> Nothing
    Just a  -> Just (f a) )
= \x -> case x of
    Nothing -> fmap f  Nothing
    Just a  -> fmap f (Just (g a))
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just (f (g a))
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just ((f . g) a)
= \x -> case x of
    Nothing -> fmap (f . g) Nothing
    Just a  -> fmap (f . g) (Just a)
= \x -> fmap (f . g) (case x of
    Nothing -> Nothing
    Just a  -> Just a )
= \x -> fmap (f . g) (case x of
    Nothing -> x
    Just a  -> x )
= \x -> fmap (f . g) (case x of
    _ -> x )
= \x -> fmap (f . g) x
= fmap (f . g)

显然我可以跳过很多这些步骤,但我只是想拼出完整的证明。一开始很难证明这些定律,直到你掌握它们的窍门,所以最好从缓慢和迂腐开始,然后一旦你变得更好,你就可以开始组合步骤,甚至在一段时间后在你的脑海中做一些更简单的事情那些。

【讨论】:

  • 谢谢加布里埃尔。有两件事使这些证明变得复杂……一是严格评估与惰性评估:您可以为Put 编写一个MonadFix 实例,该实例将满足其代数属性,但由于严格的评估仍然会失败。另一件事,可能更重要,是现实生活:您可以正确地为任何类型类编写实例,然后由于代码更改,它会以某种方式中断或倒退。似乎是您可以编写 QuickCheck 测试的那种东西,但是当您尝试测试 monad 转换器时,我很难看到如何做到这一点......
  • @mergeconflict 我一直在用我的pipes 库来解决回归问题。每当我扩展库时,我都必须重新证明类型类的规律。我可以从实际经验中说,您最终要做的是“分解”您的证明,以便您可以将改变的部分与不变的部分分开。关于 monad 转换器,我在FreeT 之上构建了所​​有我的,它免费提供了一个保证正确的 MonadTrans 实例。
猜你喜欢
  • 2016-11-05
  • 2011-07-18
  • 2014-11-06
  • 2021-03-22
  • 2014-11-07
  • 2015-05-23
  • 2018-05-29
  • 2013-01-16
  • 2013-03-11
相关资源
最近更新 更多