Summable arrows - Haskell

Can anyone think of any type constructors which have a useful implementation of:

class Fill (p :: k -> k -> *)
  where
  fillInTheBlank :: Either (p b c) (p a b) -> p a c

The law for that class is:

eassoc :: Either x (Either y z) -> Either (Either x y) z
eassoc = ...

f, g :: Fill p => Either (p c d) (Either (p b c) (p a b)) -> p a d
f = fillInTheBlank . second fillInTheBlank
g = fillInTheBlank . first fillInTheBlank . eassoc

-- Law: f = g

i swear you are the modern ekmett

"here is some code i wrote. does anyone know what it might be good for?"

next time we hang out i'd love to see where these things come from :)

next time we hang out i'd love to see where these things come from

which is when? :P

we almost got around to it last time but then we started talking about rap songs

Is this dual to composition? It feels like sort of "pipeline extension" - like ability to extend some arrow doing something useful "further", without changing it's actual effect

And id :: p a a would be base from which you can build "non-effectful" arrows? :big_smile:

Asad Saeeduddin said:

we almost got around to it last time but then we started talking about rap songs

i blame the "sandy almost died" part for that

not sure when. ever been to victoria?

nope. is that where you're at now?

yup

with a year long lease

so probably for some time

@TheMatten it's a "coproduct enriched" category (normal categories are product enriched)

I’m tempted to say there’s not many things in Hask have a useful operation here. Tuple, Either, These, and (->) are all out.

I mean, where does the information from b go? With normal composition we are able to use one b to plug into the other b, but when we’re only given one _or_ the other to work with, I’m not sure what to do with it, especially since we then need to somehow come up with a p that uses a or c when we don’t have one of those lying around.

Wait.

If we rephrase it, we have fillL : p b c -> p a c and fillR : p a b -> p a c, and this essentially says that both arguments are phantom, so nothing interesting satisfies it. q.e.d.

Wait, I guess there is at least one thing that satisfies it: TupleMaybe a b = TupleMaybe (Maybe a) (Maybe b). I think it’s associative ...

It still seems very weird to me.

Challenge: is there anything that does NOT admit a function empty : forall a b. p a b?

@Nicholas Scheel I definitely don't think the operation is impossible to implement. If anything it's too easy to implement. E.g. the identity for it assumes the form:

ez :: Void -> p a a

which is trivial to implement, it's always just absurd.

regarding the challenge, yes:

{-# LANGUAGE EmptyDataDecls #-}
data Void2 a b