2

fmap对于Monads通常默认为liftM：

liftM   :: (Monad m) => (a1 -> r) -> m a1 -> m r
liftM f m1 = do { x1 <- m1; return (f x1) }

然而，正如人们所看到的，它使用绑定（如右手去糖成m1 >>= \ x1 -> return (f x1)）。我想知道这样的 a 是否fmap可以用于为mfix具有严格>>=运算符的单子写下来。更准确地说，我想知道Control.Arrow.loop（再次）的以下实现。

我使用的 monad 是Identity，但它会在绑定发生时强制其中的任何内容seq。

newtype Id' a = Id' { runId' :: a } deriving ...

instance Functor Id' where
    fmap = liftM -- instead of `f <$> (Id' x) = Id' (f x)`. 

instance Applicative Id' where
    pure  = return
    (<*>) = ap

instance Monad Id' where
    return         = Id'
    (Id' x)  >>= k = x `seq` k x

instance MonadFix Id' where
    mfix f = let a = f (runId' a) in a

myMfix :: MonadFix m => (a -> m a) -> m a
myMfix k = let f ~(_, d) = ((,) d) <$> k d
           in (flip runKleisli () . loop . Kleisli) f

我的直觉是可以的，可以用。我认为我们只会在两种情况下遇到问题：

  1. k我们申请mfix/myMfix是严格的。
  2. 我们申请mfix/ myMfix。return

这两种情况都相当简单，我们一开始并不期望任何收敛的结果。我相信其他案例可以在不强制反馈的情况下强制进行WHNF。

我的直觉正确吗？如果没有，可以举一个失败的例子吗？

4

1 回答 1

1

您的定义Id'不是有效的单子，因为它不符合左单位定律：

  return undefined >= const (return 3)
= Id' undefined >>= const (return 3)
= undefined `seq` const (return 3) undefined
= undefined

不等于_

  const (return 3) undefined
= return 3
= Id' 3

所以关于你对MonadFixfor的定义是否Id'有效的讨论是没有实际意义的，更不用说通过 Kleisli 构造的定义是否忠实的有效性了。

话虽如此，如果你想看一个定义是否忠实地实现mfix，你需要写下并证明严格、纯洁和左缩三定律。如果您从一个实际的单子开始（而不是您Id'的未通过该测试的单子），那么您需要建立这三个定律才能被视为有效的单子反馈运算符。如果不做这项工作，就不可能说出定义如何概括。

我的预感是，您通过 Kleisli 结构对定义的直觉很可能适用于表现良好的箭头，即那些其loop操作符确实满足右收紧定律的箭头。然而，众所周知，具有左严格绑定运算符的单子的 Kleisli 类别上的箭头不具有loop满足右紧缩的运算符。（见推论 3.1.7和第 6.4.1 节的讨论。）

因此，任何具有左严格绑定运算符（例如[]、Maybe、IO、严格状态等）的 monad 都将无法通过测试。但是从诸如环境、惰性状态等单子以及由幺半群（又名作家单子）构建的单子产生的箭头可能会奏效。

于 2020-08-26T12:43:36.537 回答