Блог

В Twitter Крис Пеннер предложил интересный экземпляр 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 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
  

Согласно 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 comonad. Более того, для любого 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'
  

This fails the same associativity law again, as we expect, but this time the counterexample is marginally easier to read:

     ━━━ 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

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

With some made up syntax for show -ing MapF' s, the counterexample can be read more easily:

 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
    }
  }
}
  

So we can see the mismatch arises from the keys being deleted in the implementation of duplicate .

So it looks like that comonad doesn’t quite work out. However I was interested in seeing if there’s some way to salvage it, given that the result is pretty close. For example, what happens if we just leave the map alone instead of deleting keys?

 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
  

To my surprise, this passes all the tests (including the duplicate/duplicate one):

 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.
  

The strange thing is, this instance doesn’t have anything to do with Map s anymore. All it requires is that the thing in the second field is something we can fmap over, i.e. a Functor . So a more apt name for this type is perhaps 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
  

Теперь мы можем протестировать законы comonad для группы случайно выбранных 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
  

О чудо, hedgehog-classes не находит проблем ни с одним из этих экземпляров.

Тот факт, что NotQuiteCofree генерирует предположительно допустимые сомонады из всех этих функторов, меня немного беспокоит. NotQuiteCofree f a совершенно очевидно, что он не изоморфен Cofree f a .

Из моего ограниченного понимания, функтор cofree от Functor s до Comonad s должен быть уникальным с точностью до уникального изоморфизма, учитывая, что он по определению является правой половиной присоединения. NotQuiteCofree довольно очевидно отличается от Cofree , поэтому мы надеемся, что есть хотя бы некоторые f , для которых NotQuiteCofree f это не comonad.

Теперь к самому вопросу. Является ли тот факт, что я не нахожу никаких сбоев выше артефакта ошибки в том, как я пишу генераторы, или, возможно, ошибка в классах hedgehog, или просто слепая удача? Если нет, и NotQuiteCofree {Identity | Const x | [] | Map k} действительно являются comonads, можете ли вы придумать какой-нибудь другой f , который NotQuiteCofree f не является comonad?

В качестве альтернативы, действительно ли так, что для каждого возможного f NotQuiteCofree f является comonad? Если да, то как нам разрешить противоречие наличия двух различных cofree comonads без естественного изоморфизма между ними?

Это было глупо. Мне удалось заставить это работать 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
  

NotQuiteCofree довольно очевидно отличается от Cofree , поэтому мы надеемся, что есть хотя бы некоторые f , для которых NotQuiteCofree f это не comonad.

Этого не следует. Нет противоречия между:

1. NotQuiteCofree f является ли comonad для каждого функтора f
2. NotQuiteCofree f не является cofree comonad

«Сгенерировать cofree comonad (из любого функтора)» является строго более строгим требованием, чем «сгенерировать comonad».