# A notion dual to a product type having a given type

Consider this class:

class Has record part where
extract :: record -> part
update :: (part -> part) -> record -> record


It captures the notion of some product type record having a field of the type part which can be extracted from the record, or the functions on which can be used to update the whole record (in a lens-ish manner).

What happens if we turn the arrows? Following the types and noting that a sum type is dual to a product type, and a "factor" in a product type is analogous to an option in a sum type, we get

class CoHas sum option where
coextract :: option -> sum
coupdate :: (sum -> sum) -> option -> option


Firstly, is this line of reasoning correct at all?

If it is, what is the meaning of coextract and coupdate? Obviously, coextract produces the sum out of one of its options, so it might as well be called inject or something similar.

coupdate is more interesting. My intuition is that, given a function f that updates a sum type, it gives us a function that can be used to update one of its options. But, obviously, not every f is fit for this! Consider

badF :: Either Int Char -> Either Int Char
badF (Right _) = Left 0


then coupdate badF does not make sense where coupdate is taken from CoHas (Either Int Char) Char. One requirement seems to be that the function passed to coupdate must not change the tags of the sum type.

So here's the second question: what's the dual of this requirement in the Has/update case?

My intuition is that it's not as straightforward because Has produces a function and CoHas consumes a function. Things get more symmetric if we consider the rules for the type classes, something along the lines of

1. update f . update g = update (f . g)
2. update id = id
3. extract . update f = f . extract

Now we can actually talk about bad instances of Has producing update functions breaking these rules. But even with this additional constraint, I'm not sure I follow what the laws for the functions that coupdate accepts should be and how one could derive them from such duality-based reasoning.

• Where is the category theory in this? Have you tried setting up any commutative diagrams to see what arrows it makes sense to reverse? – pyon Oct 31 '19 at 21:00
• I'd say the main CT part is resorting to duality. In particular, $\mathbf{Hask}$ is the category (with the well-known caveats). I couldn't come up with a non-trivial diagram except for the diagram for the laws I mentioned, but it seems a bit artificial. – 0xd34df00d Oct 31 '19 at 21:04
• When you want to dualize a categorical construction, say, monoid objects, you first write down the equational laws as commutative diagrams, then flip the arrows in the diagrams. This tells you what arrows you need to flip in the type signatures (protip: not necessarily all of them). – pyon Oct 31 '19 at 21:41
• What if I didn't have update/coupdate in this particular case? I cannot think about any laws wrt extract alone, so how would I obtain coextract? – 0xd34df00d Oct 31 '19 at 21:54