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?
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 inSet, 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: