合理的Comonad实现

Question

我们可以将monad描述为计算上下文,monad实现完全保留了该上下文的含义.例如Option - 上下文含义是值可能存在.给定Option数据类型,唯一有意义的实现是pure = some, flatMap f = {none => none; some x => f x } 正如我对monad的理解,通过遵循类型签名 - 对于任何monad只有一个合理的实现.换句话说,如果要为值/计算添加一些有意义的上下文,则只有一种方法可以为任何特定的monad执行此操作.
另一方面,当涉及到comonad时,它突然开始感觉完全奇怪,就像有很多方法来实现给定类型的comonad,你甚至可能为每个实现赋予一定的意义.
NEL考虑一下copure = head. cojoin通过实现tails,完全满足类型.如果我们实现了cojoin通过permutations或fa map (_ => fa) map f将无法满足comonad法律.
但循环实施是有效的:

override def cobind[A, B](fa: NonEmptyList[A])(f: (NonEmptyList[A]) => B): NonEmptyList[B] = {
  val n: NonEmptyList[NonEmptyList[A]] = fa.map(_ => fa).zipWithIndex.map { case (li , i ) =>
    val(h: List[A], t: List[A]) = li.list.splitAt(i)
    val ll: List[A] = t ++ h
    NonEmptyList.nel(ll.head, ll.tail)
  }
  n map f
}

即使有法律限制我们,我认为,如果在Monad我们在某些情况下限制自己(我们有点不能"创造"新的信息),在Comonad中我们是进一步扩展了这个背景(有很多方法可以列出列表中的列表),这为我们提供了更多的可能性.在我的头脑中,比喻是:对于Monad,我们站在路上,想要达到一些目的地点A =因此只有有意义的最短路径可供选择.在命令中,我们站在A中,并想从它那里去,所以有更多方法可以做到.
所以我的问题是 - 我实际上是对吗？我们可以用不同的方式实现命令,每次都进行另一个有意义的抽象吗？或者只有尾部实现是合理的,因为comonad假设引入了抽象.

Answer 1

非空列表由两个标准结构作为两个不同的共同体出现.

首先,由此给出了cofree comonad.

data Cofree f x = x :& f (Cofree f x)  -- every node is labelled with an x

instance Functor f => Functor (Cofree f) where
  fmap f (x :& fcx) = f x :& fmap (fmap f) fcx

instance Functor f => Comonad (Cofree f) where
  extract (x :& _) = x   -- get the label of the top node
  duplicate cx@(_ :& fcx) = cx :& fmap duplicate fcx

非空列表可以给出

type Nellist1 = Cofree Maybe

因此自动地是comonadic.那给你"尾巴"comonad.

同时,作为"元素拉链"的结构的分解诱导了共同结构.正如我详细解释的那样,

可分性相当于拉链上的这一系列操作(从其上下文中挑选出的单个元素并将其置于"焦点")

class (Functor f, Functor (DF f)) => Diff1 f where
  type DF f :: * -> *
  upF      ::  ZF f x  ->  f x           -- defocus
  downF    ::  f x     ->  f (ZF f x)    -- find all ways to focus
  aroundF  ::  ZF f x  ->  ZF f (ZF f x) -- find all ways to *re*focus

data ZF f x = (:<-:) {cxF :: DF f x, elF :: x}

所以我们得到了一个仿函数和一个comonad

instance Diff1 f => Functor (ZF f) where
  fmap f (df :<-: x) = fmap f df :<-: f x

instance Diff1 f => Comonad (ZF f) where
  extract    = elF
  duplicate  = aroundF

原则上,这种结构也会产生非空的列表.问题是,在Haskell中表达差异的仿函数并不那么容易,即使导数是合理的.让我们疯了......

非空列表等于ZF thingy x哪里DF thingy = [].我们可以整合列表吗？以代数方式愚弄可能会给我们一个线索

[x] = Either () (x, [x]) = 1 + x * [x]

所以作为一个动力系列,我们得到

[x] = Sum(n :: Nat). x^n

我们可以集成电源系列

Integral [x] dx = Sum(n :: Nat). x^(n+1)/(n+1)

这意味着我们得到某种大小的任意元组(n + 1),但是我们必须将它们识别为等价类具有大小(n + 1)的某种关系.一种方法是识别直到旋转的元组,因此您不知道哪个(n + 1)位置是"第一".

也就是说,列表是非空循环的衍生物.想想在圆桌上打牌(可能是单人纸牌)的一群人.旋转桌子,你会得到同样的一堆人打牌.但是一旦你指定了经销商,你就可以按顺序修改其他玩家的名单,从经销商的左边顺时针方向开始.

两种标准结构; 同一仿函数的两个comonads.

(在我之前的评论中,我评论了多个monad的可能性.它有点涉及,但这是一个起点.每个monad m也是适用的,并且应用法则是m ()一个幺半群.相应地,每个monoid结构m ()至少给出一个作为monad结构的候选者m.在作家monads的情况下(,) s,我们得到monad的候选者是与幺半群(s,())相同的幺半群s.)

编辑非空列表至少有两种不同的方式也是monadic.

我为仿函数定义了身份和配对,如下所示.

newtype I         x = I x
data    (f :*: g) x = (:&:) {lll :: f x, rrr :: g x}

现在,我可以按如下方式引入非空列表,然后定义连接.

newtype Ne x = Ne ((I :*: []) x)

cat :: Ne x -> Ne x -> Ne x
cat (Ne (I x :&: xs)) (Ne (I y :&: ys)) = Ne (I x :&: (xs ++ y : ys))

这些是monadic,就像空列表一样:

instance Monad Ne where
  return x = Ne (I x :&: [])
  Ne (I x :&: xs) >>= k = foldl cat (k x) (map k xs)

但是,I是monad:

instance Monad I where
  return = I
  I a >>= k = k a

此外,monads在配对下关闭:

instance (Monad f, Monad g) => Monad (f :*: g) where
  return x = return x :&: return x
  (fa :&: ga) >>= k = (fa >>= (lll . k)) :&: (ga >>= (rrr . k))

所以我们可以写完

newtype Ne x = Ne ((I :*: []) x) deriving (Monad, Applicative, Functor)

但return那个monad给了我们双重视野.

return x = Ne (I x :&: [x])

所以你有:非空列表是comonadic两种方式,monadic两种方式,应用六种方式,...

(关于这个问题还有很多话要说,但我必须在某个地方停下来.)

Answer 2

这是相同的反例，显示 Monad 有多个可能的实例，来自 Pigworker 的评论，但更多的工作完成了（虽然没有进行类型检查，所以请原谅任何错误）。

data WithBool a = WB Bool a deriving Functor

instance Monad WithBool where
     return = WB z
     (WithBool b a) >>= f =
           case f a of (WithBool b2 r) -> WithBool (b `op` b2) r

-- This holds if op = (&&) and z = True
-- This also holds if op = (||) and z = False
-- It should also work if op = const or `flip const` and z = True _or_ False

正如 Bakuriu 所说，“默认”实现的选择在某种程度上是任意的，并且取决于人们期望的需求。