haskell - 为什么我找不到 NotQuiteCofree not-quite-comonad 的任何违法行为？

Question

在 Twitter 上，Chris Penner 提出了一个有趣的 comonad instance用于“使用默认值增强的 map ”。相关类型构造函数和实例在此处转录(有外观差异):

data MapF f k a = f a :< Map k (f a)
  deriving (Show, Eq, Functor, Foldable, Traversable)

instance (Ord k, Comonad f) => Comonad (MapF f k)
  where
  extract (d :< _) = extract d

  duplicate :: forall a. MapF f k a -> MapF f k (MapF f k a)
  duplicate (d :< m) = extend (:< m) d :< M.mapWithKey go m
    where
    go :: k -> f a -> f (MapF f k a)
    go k = extend (:< M.delete k m)

我对这个comonad 实例有点怀疑，所以我尝试使用 hedgehog-classes 测试法律。 .我为 f 选择了我能想到的最简单的仿函数; Identity共:

genMap :: Gen a -> Gen (Map Int a)
genMap g = G.map (R.linear 0 10) ((,) <$> G.int (R.linear 0 10) <*> f g)

genMapF :: (Gen a -> Gen (f a)) -> Gen a -> Gen (MapF f Int a)
genMapF f g = (:<) <$> f g <*> genMap g

genId :: Gen a -> Gen (Identity a)
genId g = Identity <$> g

main :: IO Bool
main = do
  lawsCheck $ comonadLaws $ genMapF genId

根据hedgehog-classes，除了代表关联性的“双重复制”之外，所有测试都通过了:

    ━━━ Context ━━━
    When testing the Double Duplicate law(†), for the Comonad typeclass, the following test failed:

    duplicate . duplicate $ x ≡ fmap duplicate . duplicate $ x, where
      x = Identity 0 :< fromList [(0,Identity 0),(1,Identity 0)]


    The reduced test is:
      Identity (Identity (Identity 0 :< fromList [(0,Identity 0),(1,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList [(1,Identity 0)])),(1,Identity (Identity 0 :< fromList [(0,Identity 0)]))]) :< fromList [(0,Identity (Identity (Identity 0 :< fromList [(1,Identity 0)]) :< fromList [(1,Identity (Identity 0 :< fromList [(0,Identity 0)]))])),(1,Identity (Identity (Identity 0 :< fromList [(0,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList [(1,Identity 0)]))]))]
      ≡
      Identity (Identity (Identity 0 :< fromList [(0,Identity 0),(1,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList [(1,Identity 0)])),(1,Identity (Identity 0 :< fromList [(0,Identity 0)]))]) :< fromList [(0,Identity (Identity (Identity 0 :< fromList [(1,Identity 0)]) :< fromList [(1,Identity (Identity 0 :< fromList []))])),(1,Identity (Identity (Identity 0 :< fromList [(0,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList []))]))]

    The law in question:
      (†) Double Duplicate Law: duplicate . duplicate ≡ fmap duplicate . duplicate

    ━━━━━━━━━━━━━━━

不幸的是，即使对于所示的极其简单的输入，这个反例也很难解析。
幸运的是，我们可以稍微简化问题，注意到 f参数是一个红鲱鱼。如果comonad 实例适用于显示的类型，它也应该适用于 Identity。共生。此外，对于任何 f , Map f k a可以分解为 Compose (Map Identity k a) f ，所以我们不会失去任何一般性。
因此我们可以摆脱 f通过将其专门用于 Identity始终:

data MapF' k a = a ::< Map k a
  deriving (Show, Eq, Functor)

instance Ord k => Comonad (MapF' k)
  where
  extract (a ::< _) = a
  duplicate (d ::< m) = (d ::< m) ::< M.mapWithKey (\k v -> v ::< M.delete k m) m

genMapF' :: Gen a -> Gen (MapF' Int a)
genMapF' g = (::<) <$> g <*> genMap g

main :: IO Bool
main = do
  -- ...
  lawsCheck $ comonadLaws $ genMapF'

正如我们所料，这再次失败了相同的结合律，但这次反例更容易阅读:

    ━━━ Context ━━━
    When testing the Double Duplicate law(†), for the Comonad typeclass, the following test failed:

    duplicate . duplicate $ x ≡ fmap duplicate . duplicate $ x, where
      x = 0 ::< fromList [(0,0),(1,0)]


    The reduced test is:
      ((0 ::< fromList [(0,0),(1,0)]) ::< fromList [(0,0 ::< fromList [(1,0)]),(1,0 ::< fromList [(0,0)])]) ::< fromList [(0,(0 ::< fromList [(1,0)]) ::< fromList [(1,0 ::< fromList [(0,0)])]),(1,(0 ::< fromList [(0,0)]) ::< fromList [(0,0 ::< fromList [(1,0)])])]
      ≡
      ((0 ::< fromList [(0,0),(1,0)]) ::< fromList [(0,0 ::< fromList [(1,0)]),(1,0 ::< fromList [(0,0)])]) ::< fromList [(0,(0 ::< fromList [(1,0)]) ::< fromList [(1,0 ::< fromList [])]),(1,(0 ::< fromList [(0,0)]) ::< fromList [(0,0 ::< fromList [])])]

    The law in question:
      (†) Double Duplicate Law: duplicate . duplicate ≡ fmap duplicate . duplicate

    ━━━━━━━━━━━━━━━

使用 show 的一些编造语法-ing MapF' s，反例可以更容易阅读:

x =
{ _: 0, 0: 0, 1: 0 }

duplicate . duplicate $ x =
{
  _: ...,
  0: {
    _: ...,
    1: {
      _: 0,
      0: 0  # notice the extra field here 
    }
  },
  1: {
    _: ...,
    0: {
      _: 0,
      1: 0 # ditto
    }
  }
}


fmap duplicate . duplicate $ x =
{
  _: ...,
  0: {
    _: ...,
    1: {
      _: 0 # it's not present here
    }
  },
  1: {
    _: ...,
    0: {
      _: 0 # ditto
    }
  }
}

所以我们可以看到不匹配是由于在 duplicate 的实现中被删除的键引起的。 .

所以看起来那个comonad不太有效。但是，鉴于结果非常接近，我很想看看是否有某种方法可以挽救它。例如，如果我们只保留 map 而不是删除键会发生什么？

instance Ord k => Comonad (MapF' k)
  where
  extract (a ::< _) = a

{-
  -- Old implementation
  duplicate (d ::< m) = (d ::< m) ::< M.mapWithKey (\k v -> v ::< M.delete k m) m
-}

  -- New implementation
  duplicate (d ::< m) = (d ::< m) ::< fmap (::< m) m

令我惊讶的是，这通过了所有测试(包括重复/重复测试):

Comonad: Extend/Extract Identity    ✓ <interactive> passed 100 tests.
Comonad: Extract/Extend    ✓ <interactive> passed 100 tests.
Comonad: Extend/Extend    ✓ <interactive> passed 100 tests.
Comonad: Extract Right Identity    ✓ <interactive> passed 100 tests.
Comonad: Extract Left Identity    ✓ <interactive> passed 100 tests.
Comonad: Cokleisli Associativity    ✓ <interactive> passed 100 tests.
Comonad: Extract/Duplicate Identity    ✓ <interactive> passed 100 tests.
Comonad: Fmap Extract/Duplicate Identity    ✓ <interactive> passed 100 tests.
Comonad: Double Duplication    ✓ <interactive> passed 100 tests.
Comonad: Extend/Fmap . Duplicate Identity    ✓ <interactive> passed 100 tests.
Comonad: Duplicate/Extend id Identity    ✓ <interactive> passed 100 tests.
Comonad: Fmap/Extend Extract    ✓ <interactive> passed 100 tests.
Comonad: Fmap/LiftW Isomorphism    ✓ <interactive> passed 100 tests.

奇怪的是，这个实例与 Map 没有任何关系。 s了。它所要求的只是第二个字段中的东西是我们可以 fmap 的东西。结束，即 Functor .所以这个类型的一个更贴切的名字可能是 NotQuiteCofree :

--   Cofree         f a = a :< f (Cofree f a)
data NotQuiteCofree f a = a :< f a

instance Functor f => Comonad (NotQuiteCofree f)
  where
  duplicate (a :< m) = (a :< m) :< fmap (:< m) m -- Exactly what we had before
  extract (a :< _) = a

现在我们可以测试一组随机选择的 f 的共素定律。 s(包括 Map k s):

genNQC :: (Gen a -> Gen (f a)) -> Gen a -> Gen (NotQuiteCofree f a)
genNQC f g = (:<) <$> g <*> f g

-- NotQuiteCofree Identity ~ Pair
genId :: Gen a -> Gen (Identity a)
genId g = Identity <$> g

-- NotQuiteCofree (Const x) ~ (,) x
genConst :: Gen a -> Gen (Const Int a)
genConst g = Const <$> G.int (R.linear 0 10)

-- NotQuiteCofree [] ~ NonEmpty
genList :: Gen a -> Gen [a]
genList g = G.list (R.linear 0 10) g

-- NotQuiteCofree (Map k) ~ ???
genMap :: Gen a -> Gen (Map Int a)
genMap g = G.map (R.linear 0 10) ((,) <$> (G.int $ R.linear 0 10) <*> g)

main :: IO Bool
main = do
  lawsCheck $ comonadLaws $ genNQC genId
  lawsCheck $ comonadLaws $ genNQC genConst
  lawsCheck $ comonadLaws $ genNQC genList
  lawsCheck $ comonadLaws $ genNQC genMap

瞧，刺猬类发现这些实例中的任何一个都没有问题。
NotQuiteCofree 的事实从所有这些仿函数生成所谓的有效共单子(monad)对我来说有点担心。 NotQuiteCofree f a很明显不与 Cofree f a 同构.
根据我有限的理解，来自 Functor 的 cofree 仿函数转至 Comonad s 在唯一同构之前必须是唯一的，因为根据定义它是附加词的右半部分。 NotQuiteCofree与 Cofree 明显不同，所以我们希望至少有一些 f NotQuiteCofree f不是comonad。
现在来回答实际问题。事实上，我没有发现任何失败是因为我编写生成器的方式有误，或者可能是刺猬类中的错误，或者只是盲目的运气？如果没有， NotQuiteCofree {Identity | Const x | [] | Map k}真的是comonads，你能想到一些其他的 f NotQuiteCofree f不是comonad吗？
或者，对于每一个可能的 f，真的是这样吗？ , NotQuiteCofree f是comonad？如果是这样，我们如何解决两个不同的 cofree 共单胞之间没有自然同构的矛盾？

Answer 1

这真是太棒了。我设法让它在 Set 中工作，但我怀疑我们应该能够概括。然而，这个证明使用了我们可以很好地计算 Set 的事实。 ，所以一般形式要困难得多。
这是 Agda 中的证明，使用 https://github.com/agda/agda-categories图书馆:

{-# OPTIONS --without-K --safe #-}

module Categories.Comonad.Morphism where

open import Level
open import Data.Product hiding (_×_)

open import Categories.Category.Core

open import Categories.Comonad
open import Categories.Functor renaming (id to Id)
open import Categories.NaturalTransformation hiding (id)
open import Categories.Category.Cartesian
open import Categories.Category.Product
import Categories.Morphism.Reasoning as MR
open import Relation.Binary.PropositionalEquality

module Cofreeish-F {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Products : BinaryProducts 𝒞) where
  open BinaryProducts 𝒞-Products hiding (_⁂_)
  open Category 𝒞
  open MR 𝒞
  open HomReasoning

  Cofreeish : (F : Endofunctor 𝒞) → Endofunctor 𝒞
  Cofreeish F = record
    { F₀ = λ X → X × F₀ X
    ; F₁ = λ f → ⟨ f ∘ π₁ , F₁ f ∘ π₂ ⟩
    ; identity = λ {A} → unique id-comm (id-comm ○ ∘-resp-≈ˡ (⟺ identity)) ; homomorphism = λ {X} {Y} {Z} {f} {g} →
      unique (pullˡ project₁ ○ pullʳ project₁ ○ ⟺ assoc) (pullˡ project₂ ○ pullʳ project₂ ○ pullˡ (⟺ homomorphism))
    ; F-resp-≈ = λ eq → unique (project₁ ○ ∘-resp-≈ˡ (⟺ eq)) (project₂ ○ ∘-resp-≈ˡ (F-resp-≈ (⟺ eq)))
    }
    where
      open Functor F

  Strong : (F : Endofunctor 𝒞) → Set (o ⊔ ℓ ⊔ e)
  Strong F = NaturalTransformation (-×- ∘F (F ⁂ Id)) (F ∘F -×-)


open import Categories.Category.Instance.Sets
open import Categories.Category.Monoidal.Instance.Sets

module _ (c : Level) where
  open Cofreeish-F (Sets c) Product.Sets-has-all
  open Category (Sets c)
  open MR (Sets c)
  open BinaryProducts {𝒞 = Sets c} Product.Sets-has-all
  open ≡-Reasoning

  strength : ∀ (F : Endofunctor (Sets c)) → Strong F
  strength F = ntHelper record
    { η = λ X (fa , b) → F.F₁ (_, b) fa
    ; commute = λ (f , g) {(fa , b)} → trans (sym F.homomorphism) F.homomorphism
    }
    where
      module F = Functor F

  Cofreeish-Comonad : (F : Endofunctor (Sets c)) → Comonad (Sets c)
  Cofreeish-Comonad F = record
    { F = Cofreeish F
    ; ε = ntHelper record
      { η = λ X → π₁
      ; commute = λ f → refl
      }
    ; δ = ntHelper record
      { η = λ X → ⟨ id , F-strength.η _ ∘ Δ ∘ π₂ ⟩
      ; commute = λ f → cong₂ _,_ refl (trans (sym F.homomorphism) F.homomorphism)
      }
    ; assoc = δ-assoc
    ; sym-assoc = sym δ-assoc
    ; identityˡ = ε-identityˡ
    ; identityʳ = ε-identityʳ
    }
    where
      module F = Functor F
      module F-strength = NaturalTransformation (strength F)

      δ : ∀ X → X × F.F₀ X → (X × F.F₀ X) × F.F₀ (X × F.F₀ X)
      δ _ = ⟨ id , F-strength.η _ ∘ Δ ∘ π₂ ⟩

      ε : ∀ X → X × F.F₀ X → X
      ε _ = π₁

      δ-assoc : ∀ {X} → δ (X × F.F₀ X) ∘ δ X ≈ ⟨ id , F.F₁ (δ X) ∘ π₂ ⟩ ∘ δ X
      δ-assoc {X} {(x , fx)} = cong₂ _,_ refl (trans (sym F.homomorphism) F.homomorphism)

      ε-identityˡ : ∀ {X} → ⟨ ε X ∘ π₁ , F.F₁ (ε X) ∘ π₂ ⟩ ∘ δ X ≈ id
      ε-identityˡ {X} {(x , fx)} = cong₂ _,_ refl (trans (sym F.homomorphism) F.identity)

      ε-identityʳ : ∀ {X} → ε (X × F.F₀ X) ∘ δ X ≈ id
      ε-identityʳ {X} {(x , fx)} = refl