Why can't I find any law violations for the NotQuiteCofree not-quite-comonad?

Question

On Twitter, Chris Penner suggested an interesting comonad instance for "maps augmented with a default value". The relevant type constructor and instance are transcribed here (with cosmetic differences):

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)

I was a little bit suspicious of this comonad instance, so I tried testing the laws using hedgehog-classes. I picked the simplest functor I could think of for f; the 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

According to hedgehog-classes, all the tests pass except for the "double duplication" one, which represents associativity:

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

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

---

Unfortunately this counterexample is pretty difficult to parse, even for the extremely simple input shown.

Luckily we can simplify the problem a bit, by noticing that the f parameter is a red-herring. If the comonad instance works for the type shown, it should also work for the Identity comonad. Moreover for any f, Map f k a can be decomposed into Compose (Map Identity k a) f, so we do not lose any generality.

Thus we can get rid of the f by specializing it to Identity throughout:

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

Now we can test the comonad laws for a bunch of randomly selected fs (including 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

Lo and behold, hedgehog-classes finds no problem with any of these instances.

---

The fact that NotQuiteCofree generates supposedly valid comonads from all these functors is a bit concerning to me. NotQuiteCofree f a is quite obviously not isomorphic to Cofree f a.

From my limited understanding, a cofree functor from Functors to Comonads must be unique up to unique isomorphism, given that it is by definition the right half of an adjunction. NotQuiteCofree is pretty obviously distinct from Cofree, so we would hope that there is at least some f for which NotQuiteCofree f is not a comonad.

Now for the actual question. Is the fact that I'm not finding any failures above an artifact of a mistake in how I'm writing the generators, or perhaps a bug in hedgehog-classes, or just blind luck? If not, and NotQuiteCofree {Identity | Const x | [] | Map k} really are comonads, can you think of some other f for which NotQuiteCofree f is not a comonad?

Alternatively, is it really the case that for every possible f, NotQuiteCofree f is a comonad? If so, how do we resolve the contradiction of having two distinct cofree comonads with no natural isomorphism between them?

Answer 1

This was a doozy. I managed to get this working in Set, but I suspect that we should be able to generalize. However, this proof uses the fact that we can compute nicely in Set, so the general form is much, much, much more difficult.

Here's the proof in Agda, using the https://github.com/agda/agda-categories library:

{-# 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

Answer 2

NotQuiteCofree is pretty obviously distinct from Cofree, so we would hope that there is at least some f for which NotQuiteCofree f is not a comonad.

This does not follow. There is no contradiction between:

1. NotQuiteCofree f is a comonad for every functor f
2. NotQuiteCofree f is not a cofree comonad

"Generate a cofree comonad (from any functor)" is a strictly stronger requirement than "generate a comonad".