19

给定一个可微类型，我们知道它Zipper是一个Comonad. 对此，丹·伯顿（Dan Burton）问道：“如果推导产生了一个单子，这是否意味着整合产生了一个单子？或者这是胡说八道吗？”。我想给这个问题一个具体的含义。如果一个类型是可微的，它一定是一个单子吗？给定以下定义，该问题的一种表述是问

data Zipper t a = Zipper { diff :: D t a, here :: a }

deriving instance Diff t => Functor (Zipper t)

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)

我们可以编写具有类似签名的函数吗

return :: (Diff t) => a -> t a
(>>=) :: (Diff t) => t a -> (a -> t b) -> t b

遵守单子定律。

在链接问题的答案中，有两种成功的方法可以解决类似的Comonad为Zipper. 第一种方法是扩展Diff类以包括对偶>>=并使用偏微分。第二种方法是要求类型是两次或无限可微的。

4

2 回答 2

5

不。 void 函子data V a是可微的，但return不能为它实现。

于 2014-12-04T15:46:39.427 回答
3

如果我们完全颠倒一切，我们可以毫不奇怪地推导出Monad类似的东西。我们之前的声明和新的声明如下。我不完全确定下面定义的类实际上是集成，所以我不会这样明确地引用它。

如果 D t 是 t 的导数，则 D t 的乘积和恒等式是 Comonad
如果 D' t 是 ??? 的 t 那么 D' t 和恒等式的总和是 Monad

首先，我们将定义 a 的反义词Zipperan Unzipper。它将是一个总和，而不是一个产品。

data Zipper   t a = Zipper { diff :: D  t a  ,  here :: a }
data Unzipper t a =          Unzip  (D' t a) |  There   a

AnUnzipper是 aFunctor只要D' t是 a Functor。

instance (Functor (D' t)) => Functor (Unzipper t) where
    fmap f (There x) = There (f x)
    fmap f (Unzip u) = Unzip (fmap f u)

如果我们回忆一下课堂Diff

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)

与它相反的事物类别Diff', 是相同的，但每个实例都Zipper替换为Unzipper并且箭头的顺序->翻转了。

class (Functor t, Functor (D' t)) => Diff' t where
    type D' t :: * -> *
    up' :: t a -> Unzipper t a
    down' :: t (Unzipper t a) -> t a

如果我们使用我对上一个问题的解决方案

around :: (Diff t, Diff (D t)) => Zipper t a -> Zipper t (Zipper t a)
around z@(Zipper d h) = Zipper ctx z
    where
        ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)

我们可以定义该函数的逆函数，它将join用于Monad.

inside :: (Diff' t, Diff' (D' t)) => Unzipper t (Unzipper t a) -> Unzipper t a
inside (There x) = x
inside (Unzip u) = Unzip . down' . fmap f $ u
    where
        f (There u') = There u'
        f (Unzip u') = up' u'

这允许我们Monad为Unzipper.

instance (Diff' t, Diff' (D' t)) => Monad (Unzipper t) where
    return = There
    -- join = inside
    x >>= f = inside . fmap f $ x

此实例Comonad与Zipper.

instance (Diff t, Diff (D t)) => Comonad (Zipper t) where
    extract   = here
    duplicate = around
于 2014-12-11T21:02:23.120 回答