emilypi / smash

Smash products, Wedge products, and other Pointed stuff
34 stars 11 forks source link

Unzipping and undeciding works for any functor #1

Closed masaeedu closed 4 years ago

masaeedu commented 4 years ago

I was reading through some of the code and spotted this thing:

-- | Distribute a 'Can' value over a product.
--
distributeCan :: Can (a,b) c -> (Can a c, Can b c)
distributeCan = \case
    Non -> (Non, Non)
    One (a,b) -> (One a, One b)
    Eno c -> (Eno c, Eno c)
    Two (a,b) c -> (Two a c, Two b c)

-- | Codistribute a coproduct over a 'Can' value.
--
codistributeCan :: Either (Can a c) (Can b c) -> Can (Either a b) c
codistributeCan = \case
    Left ac -> case ac of
      Non -> Non
      One a -> One (Left a)
      Eno c -> Eno c
      Two a c -> Two (Left a) c
    Right bc -> case bc of
      Non -> Non
      One b -> One (Right b)
      Eno c -> Eno c
      Two b c -> Two (Right b) c

I think we can reuse some of the other work in the module by writing:

distributeCan :: Can (a,b) c -> (Can a c, Can b c)
distributeCan fabc = (first fst fabc, first snd fabc)

codistributeCan :: Either (Can a c) (Can b c) -> Can (Either a b) c
codistributeCan (Left fac) = first Left fac
codistributeCan (Right fbc) = first Right fbc

or more generally by just writing:

unzipFirst :: Bifunctor f => f (a, b) c -> (f a c, f b c)
unzipFirst fabc = (first fst fabc, first snd fabc)

undecideFirst :: Bifunctor f => Either (f a c) (f b c) -> f (Either a b) c
undecideFirst (Left fac) = first Left fac
undecideFirst (Right fbc) = first Right fbc
emilypi commented 4 years ago

Hmmm. I suppose this is just a general Fact About Hask! I'd love a PR which does the same for Wedge and Can as well. I think i repeat myself a bit (co)distributing over both of those as well.

emilypi commented 4 years ago

Sorry, wrong button 😅

masaeedu commented 4 years ago

It is indeed a general fact about Hask. Every endofunctor on Hask is oplax monoidal between the (,) structure and itself, and also lax monoidal between the Either structure and itself.

I can take a crack at a PR. Do you want a general purpose unzip and undecide or one for each data type?

emilypi commented 4 years ago

i think it would be useful to write an Internal.hs module where we abstract away some of this work, and yes, i'd love an unzip and undecide for each module! Thank you 😄

masaeedu commented 4 years ago

Only tangetially related, but I think the fact in question actually holds for arbitrary categories with products and coproducts, i.e. every endofunctor in a cartesian category oplaxly preserves the product, and every endofunctor in a cocartesian category laxly preserves the coproduct.

So with these things:

undistributeSmash :: Wedge (Smash a c) (Smash b c) -> Smash (Wedge a b) c

pairSmashCan :: Smash (Can a b) c -> Can (Smash a c) (Smash b c)

the code is doing the same thing, but for a non-Bifunctor bifunctor, a non-Either coproduct, and a non-(,) product.

emilypi commented 4 years ago

Yes, they are intended to be very general facts about how additive and multiplicative conjunctions and disjunctions play with each other. The second fact was taken from the coherence maps between the conjunctions in a linear logical view of symm. mon. cats.