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

Question

在 Twitter 上，Chris Penner 为“使用默认值增强的地图”提出了一个有趣的comonad 实例。相关类型构造函数和实例在此处转录（有外观差异）：

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 实例适用于显示的类型，它也应该适用于Identitycomonad。而且对于 any 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-ingMapF'的一些组合语法，可以更容易地阅读反例：

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不太有效。但是，鉴于结果非常接近，我很想看看是否有某种方法可以挽救它。例如，如果我们只保留地图而不是删除键会发生什么？

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.

奇怪的是，这个实例与 s 没有任何关系Map了。它所需要的只是第二个字段中的东西是我们可以克服的东西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 ks）的共单子定律：

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从所有这些函子生成所谓有效的共单子的事实让我有点担心。NotQuiteCofree f a很明显不与同构Cofree f a。

根据我有限的理解，从Functors 到Comonads 的 cofree 函子必须是唯一的，直到唯一的同构，因为它根据定义是附加的右半部分。NotQuiteCofree与很明显不同Cofree，所以我们希望至少有f一些NotQuiteCofree f不是comonad。

现在来回答实际问题。事实上，我没有发现任何失败是因为我编写生成器的方式有误，或者可能是刺猬类中的错误，或者只是盲目的运气？如果不是，而且NotQuiteCofree {Identity | Const x | [] | Map k}确实是共单胞，你能想出其他不是f共单胞的吗？NotQuiteCofree f

或者，对于每一个可能的情况，是否真的f是NotQuiteCofree f一个共胞？如果是这样，我们如何解决两个不同的 cofree 共单胞之间没有自然同构的矛盾？

score 4 · Accepted Answer

NotQuiteCofree与非常明显不同Cofree，因此我们希望至少有一些f不是NotQuiteCofree fcomonad。

这不遵循。之间没有矛盾：

NotQuiteCofree f是每一个函子的一个comonadf
NotQuiteCofree f不是cofree comonad

“Generate a cofree comonad (from any functor)”是比“generate a comonad”更严格的要求。

score 4 · Accepted Answer

这真是太棒了。我设法让这个工作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

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

2 回答 2

Related

Reference