In real world application I noticed a pattern that could be generalized to something like:
purescript:
class Profunctor p <= Zero p where
pzero :: forall a b. p a b -- such that `forall f g. dimap f g pzero == pzero`
It seems basic enough to have its own name in literature and libraries out there.
So what is its name? (Zero
and pzero
are made up by me.)
UPDATE
I realized I made wrong generalization. My real world data type could provide infinitely many pzero
implementations while what I really meant was a unique pzero
that was identity for psum :: forall a b . p a b -> p a b -> p a b
. So what I was looking a name for was rather:
purescript:
class Profunctor p <= Sum p where
psum :: forall a b . p a b -> p a b -> p a b -- such that `psum a (psum b c) == psum (psum a b) c
class (Profunctor p, Sum p) <= Zero p where
pzero :: forall a b. p a b -- such that `psum pzero p == p == psum p pzero`
(possibly without Profunctor p
constrain).
This looks like a dual of Product Profunctor so I would call it Sum Profunctor, unless the literature and libraries discovered it already under a different name.
pzero
appears to be a fixed point fordimap f g
. Is it supposed to be the same value for allf
andg
? – Lavonnadimap f g
as the left-handpzero
is of different type than right-handpzero
. – Jetport==
, because for arbitraryf :: a -> b
andg :: c -> d
,dimap f g pzero
cannot be compared withpzero
itself. – Lavonna==
in terms of equational reasoning. – Jetportp () Void
. – Mastin