问题描述
在Twitter上，克里斯·彭纳（Chris Penner）提出了一个有趣的comonad instance，用于“使用默认值增强的地图”。相关的类型构造函数和实例在此处转录（具有外观差异）：
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)
我对此共同实例有点怀疑，因此我尝试使用hedgehog-classes测试法律。我选择了f可以想到的最简单的函子； Identity comonad：
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
根据刺猬类，所有测试均通过，除了代表关联性的“双重重复”测试之外。
━━━ 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)]) :< fromList [(0,Identity (Identity 0 :< fromList [(1,Identity 0)])),Identity (Identity 0 :< fromList [(0,Identity 0)]))]) :< fromList [(0,Identity (Identity (Identity 0 :< fromList [(1,Identity 0)]) :< fromList [(1,Identity 0)]))])),Identity (Identity (Identity 0 :< fromList [(0,Identity 0)]))]))]
≡
Identity (Identity (Identity 0 :< fromList [(0,Identity (Identity 0 :< fromList []))])),Identity (Identity 0 :< fromList []))]))]
The law in question:
(†) Double Duplicate Law: duplicate . duplicate ≡ fmap duplicate . duplicate
━━━━━━━━━━━━━━━
不幸的是，即使显示了极其简单的输入，该反例也很难解析。
幸运的是，我们注意到f参数是红色鲱鱼，因此可以稍微简化问题。如果comonad实例适用于所示类型，则它也应适用于Identity comonad。此外，对于任何f，Map f k a都可以分解为Compose (Map Identity k a) f，因此我们不会失去任何一般性。
因此，我们可以通过在整个过程中将其专门化为f来摆脱Identity：
data MapF' k a = a ::< Map k a
deriving (Show,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(†),where
x = 0 ::< fromList [(0,0),0)]
The reduced test is:
((0 ::< fromList [(0,0)]) ::< fromList [(0,0 ::< fromList [(1,0)]),0 ::< fromList [(0,0)])]) ::< fromList [(0,(0 ::< fromList [(1,0)]) ::< fromList [(1,0)])]),(0 ::< fromList [(0,0)])])]
≡
((0 ::< fromList [(0,0 ::< fromList [])]),0 ::< fromList [])])]
The law in question:
(†) Double Duplicate Law: duplicate . duplicate ≡ fmap duplicate . duplicate
━━━━━━━━━━━━━━━
使用show-ing MapF'中的一些组合语法，可以更轻松地阅读反例：
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 =
{
_: ...,1: {
_: 0 # it's not present here
}
},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.
奇怪的是，该实例与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（包括Map k）的comonad定律：
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同构。
根据我的有限理解，从Functor到Comonad的共游离函子必须是唯一的，直到唯一的同构，因为从定义上说，它是附加词的右半部分。 NotQuiteCofree很明显与Cofree不同，因此我们希望至少有一些f不是{em> 的NotQuiteCofree f。
现在回答实际问题。我没有发现任何故障，而不是因为我在编写发电机的方式上出现了错误，或者是刺猬类中的错误，或者仅仅是运气不佳？如果不是，并且NotQuiteCofree {Identity | Const x | [] | Map k}确实是同名的，您能想到其他f不是 同名的NotQuiteCofree f吗？
或者，对于每一个可能的f，NotQuiteCofree f都是同一个事实吗？如果是这样，我们如何解决具有两个不同的共游离共轭分子之间没有自然同构的矛盾？
解决方法
NotQuiteCofree与Cofree明显不同，因此我们希望至少有一些f并不陌生。{p>
这不遵循。之间没有矛盾：
-
NotQuiteCofree f是每个函子NotQuiteCofree f的象征 -
f并非自由自在的同伴
“从任何函子生成共游离的共轭”是比“生成共价的”严格更严格的要求。
,这太傻了。我设法在Set中使它起作用，但是我怀疑我们应该能够一概而论。但是，此证明使用了一个事实，即我们可以在Set中很好地进行计算，因此一般形式要困难得多。
以下是使用https://github.com/agda/agda-categories库的Agda证明：
{-# 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,_ refl (trans (sym F.homomorphism) F.identity)
ε-identityʳ : ∀ {X} → ε (X × F.F₀ X) ∘ δ X ≈ id
ε-identityʳ {X} {(x,fx)} = refl