ComonadApply instances for StoreT and NonEmpty violates its laws

[KingoftheHomeless]

StoreT violates the law that extract (p <@> q) = extract p (extract q)

> let p = store (++) [1]
> let q = store id [2]
> extract (p <@> q) == extract p (extract q)
False

NonEmpty violates the law that duplicate (p <@> q) = (<@>) <$> duplicate p <@> duplicate q

> let p = (,) <$> fromList [1,2,3]
> let q = fromList [4,5]
> duplicate (p <@> q) == ((<@>) <$> duplicate p <@> duplicate q)
False

Note that having (<@>) = zipWith id would be a legal ComonadApply instance for NonEmpty. (Sloppy) proof here. Using this instance would, however, violate (<@>) = (<*>).

[KingoftheHomeless]

Looks like the instance for Tree from Data.Tree violates the laws, too.

> let ff = (,) <$> 59 `Node` [14 `Node` [13 `Node` []],66 `Node` [33 `Node` []]]
> let fa = 23 `Node` [22 `Node` [26 `Node` []],86 `Node` []]
> duplicate (ff <@> fa) == ((<@>) <$> duplicate ff <@> duplicate fa)
False

Note that a zipWith instance for Tree would also seem to make it a legal ComonadApply:

instance ComonadApply Tree where
  Node f fs <@> Node a as = Node (f a) (zipWith (<@>) fs as)

I haven't proven this, though.

[code5hot]

I think this requirement should be removed:

If our type is both a ComonadApply and Applicative we further require (<*>) = (<@>)

as explained in https://www.youtube.com/watch?v=F7F-BzOB670, <@> must be zippy, and this is despite the fact that <*> doesn't have to be and often shouldn't be.

Is there a logical demand for this equality?

[code5hot]

Also, why is ComonadApply a direct subclass of Comonad? Intuitively I expect there must be a variety of comonad-like typeclasses whose laws can be constrained in ComonadApply where Comonad is just one special case. Partial and superposition/seive-like objects with totalExtract :: w a -> x a and totalExtend :: (w a -> x b) -> w a -> w b, etc

[KingoftheHomeless]

ComonadApply stems from "ComonadZip" as presented in "The Essence of Dataflow Programming" by Tarmo Uustalu and Varmo Vene. Mathematically, it corresponds to symmetric semi-monoidal comonads (equipped with tensorial strength). It could be that there are more general set of laws that enforce "zippyness" that ComonadApply's laws simply imply, but for the purposes of the comonad package, the interest is simply on how (<@>) interacts with extract and extend/duplicate, so no need to generalize it. At least, that's what I wager the reason is.

Kmett has previously stated (somewhere, don't remember where) that although he would like to keep (<*>) = (<@>), dropping it if it becomes too unwieldy was a sacrifice he was ready to make. Not sure what the pros are of keeping it outside of consistency in semantics.

I agree with dropping (<*>) = (<@>), but I'm not for generalizing ComonadApply. Not in this package, anyway.

[code5hot]

I wonder if ComonadApply laws can be stated in terms of https://hackage.haskell.org/package/semigroupoids-5.2.1/docs/Data-Functor-Extend.html#v:extended instead of extract and would this allow us to define a zip operation <.> for []? Giving us dot-product and cross-product quite freely for types that are both ZipApply and Apply. This might give a good intuition of the true range of relationships between <*> and <@> (lets call it <.> to express that relationship, should it exist).

class Extend w => ZipApply w where (<.>) :: w (a -> b) -> w a -> w b infixl 4 <.>

instance ZipApply [] where (<.>) = zipWith ($)

perhaps semigroupoids would be the right package to [try to] generalise ComonadZip to ZipApply, but there's also a package somewhere containing a zippy class of some sort and maybe that's ZipApply without the relation to Extend and laws.

[code5hot]

I was looking at the Tree implementation too. It's not entirely zippy but it's root has only one value so at that point <*> and <@> are the same and I don't know for sure that it's not valid for the branches to be combined with <@>.

Can anyone point me to some reasoning for which way it should/must be done?

[code5hot]

well, at least I just showed with == that <*> is right out because duplicate (p <*> q) /= ((<*>) <$> duplicate p <*> duplicate q) which is one of the laws

[code5hot]

I've discovered that there's such a thing as a Cosemigroupad which doesn't have extract and some of its instances are also zippy applicatives.

Also there's a more interesting typeclass which doesn't have a dual and which provides parallels to duplicate and extend where a Cosemigroupad's duplicate method gives a related comonad (eg class (Cosemigroupad w, Comonad w') => Focal w w' where focii :: w a -> w' a).

Can anyone recommend how I can develop this idea and where/how it should be discussed? I'm quite intermediate with Haskell and very beginner with category theory.

This Focal typeclass also provides demotion from a Comonad to it's counterpart Cosemigroupad and direct promotion (cf. duplicate) along with an instance-specific HyperMaybe datatype - which gives zero or more variants of Nothing - one for each Cosemigroupad value that isn't represented in the Comonad; parPromote :: w -> HyperMaybe w'. For the (List, NonEmpty) pair HyperMaybe = Maybe and the parPromote equals nonEmpty :: List a -> NonEmpty a. Every Comonad w is a Cosemigroupad w where Focal w w so we can say class Cosemigroupad w => Comonad w and instance Comonad w => Focal w w and that for Focal w w, HyperMaybe = Identity and there is therefore a subclass of Focal with totPromote :: w -> w' = id.

[tuckergs]

I have an incredibly stupid ComonadApply instance for Store that satisfies the laws:

data Store s a = Store (s -> a) s
Store f1 s1 <@> Store f2 s2 = Store (\_ -> f1 s1 (f2 s2)) undefined

The analogue for StoreT I wasn't able to prove the laws, and I think that I would need some more laws to show it

StoreT wf1 s1 <@> StoreT wf2 s2 = StoreT (liftW2 (\f1 f2 _ -> f1 s1 (f2 s2)) wf1 wf2) undefined

[tuckergs]

Actually, just realized that my proof of the duplicate law is wrong, and it turns out it's almost true, but not quite equal:

duplicate (Store f1 s1 <@> Store f2 s2)
= Store (\x -> Store (const $ f1 s1 (f2 s2)) x) undefined
(<@>) <$> duplicate (Store f1 s1) <@> duplicate (Store f2 s2)
= Store (\_ -> Store (const $ f1 s1 (f2 s2)) undefined) undefined

[tuckergs]

I now have an instance for Store that I'm pretty sure obeys the laws Store f1 s1 <@> Store f2 s2 = Store (\s -> f1 s (f2 s2)) s1 Here's a proof of it: https://gist.github.com/tuckergs/f97b97a2dc8607e8ebc0fd0a77cd75c0