Opened 3 years ago

Last modified 3 years ago

#13026 new feature request

RFC functions for sums and products

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: libraries/base Version: 8.0.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

I'll ask on the libraries mailing list depending on feedback.

Adding these to Data.Functor.Sum, Data.Functor.Product a la Control.Arrow

(||||) :: (f a -> b) -> (g a -> b) -> ((Sum f g) a -> b)
f |||| g = \case
  InL fa -> f fa
  InR ga -> g ga

(&&&&) :: (a -> f b) -> (a -> g b) -> (a -> (Product f g) b)
(f &&&& g) a = f a `Pair` g a

|||| is used in "Monad transformers and modular algebraic effects: What binds them together" in section 2.4, the names are up for discussion

Edit: coproduct is one name for ||||

Change History (12)

comment:1 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 3 years ago by Iceland_jack

Some other

type f ~> g = forall x. f x -> g x

(****) :: f ~> f' -> g ~> g' -> Product f g ~> Product f' g'
(f **** g) (fa `Pair` ga) = f fa `Pair` g ga

first' :: f ~> f' -> Product f g ~> Product f' g
first' = (**** id)

second' :: g ~> g' -> Product f g ~> Product f g'
second' = (id ****)

(++++) :: f ~> f' -> g ~> g' -> Sum f g ~> Sum f' g'
f ++++ g = \case
  InL fa -> InL (f fa)
  InR ga -> InR (g ga)

left' :: f ~> f' -> Sum f g ~> Sum f' g
left' = (++++ id)

right' :: g ~> g' -> Sum f g ~> Sum f g'
right' = (id ++++)

comment:3 Changed 3 years ago by Iceland_jack

Stolen from Data.Tuple, I have never needed them but who knows

fst' :: Product f g ~> f
fst' (Pair fa _) = fa

snd' :: Product f g ~> g
snd' (Pair _ ga) = ga

curry' :: (Product f g ~> h) -> (forall a. f a -> g a -> h a)
curry' nat fa ga = nat (Pair fa ga) 

uncurry' :: (forall a. f a -> g a -> h a) -> (Product f g ~> h)
uncurry' f (Pair fa ga) = f fa ga

swap' :: Product f g ~> Product g f
swap' (Pair fa ga) = Pair ga fa

and from Data.Either

lefts' :: [(Sum f g) a] -> [f a]
lefts' sums = [ fa | InL fa <- sums ]

rights' :: [(Sum f g) a] -> [g a]
rights' sums = [ ga | InR ga <- sums ]

isInL :: Sum f g a -> Bool
isInL InL{} = True
isInL _     = False

isInR :: Sum f g a -> Bool
isInR InR{} = True
isInR _     = False

partitionSums :: [Sum f g a] -> ([f a], [g a])
partitionSums = foldr (left |||| right) ([], [])
 where
   left  a ~(l, r) = (a:l, r)
   right a ~(l, r) = (l, a:r)

With the lens vocabulary we could write

_InL :: Prism (Sum f g a) (Sum f' g a) (f a) (f' a)
_InL = prism
  InL
  (\case
    InL fa -> Right fa
    InR ga -> Left (InR ga))

_InR :: Prism (Sum f g a) (Sum f g' a) (g a) (g' a)
_InR = prism
  InR
  (\case
    InR ga -> Right ga
    InL fa -> Left (InL fa))

instance Field1 (Product f g a) (Product f' g a) (f a) (f' a) where
  _1 :: Lens (Product f g a) (Product f' g a) (f a) (f' a)
  _1 = lens
    fst'
    (\(Pair _ ga) fa -> Pair fa ga)

instance Field2 (Product f g a) (Product f g' a) (g a) (g' a) where
  _2 :: Lens (Product f g a) (Product f g' a) (g a) (g' a)
  _2 = lens
    snd'
    (\(Pair fa _) ga -> Pair fa ga)
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:5 Changed 3 years ago by Iceland_jack

Some more functions (would be Isos in lens)

runSum :: Sum f g a -> Either (f a) (g a)
runSum = Left |||| Right

runProduct :: Product f g a -> (f a, g a)
runProduct (Pair fa ga) = (fa, ga)

And their inverses, used here to define ++++, **** in terms of +++, ***.

This is how Purescript defines Product, Coproduct.

Purescript calls **** and ||||

bihoistProduct :: forall f g h i. (f ~> h) -> (g ~> i) -> (Product f g) ~> (Product h i)

coproduct :: forall f g a b. (f a -> b) -> (g a -> b) -> Coproduct f g a -> b
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:6 Changed 3 years ago by Iceland_jack

These functions and more are defined here

(.|||.) :: (f1 :~> g) -> (f2 :~> g) -> ((f1 :+: f2) :~> g)
(<|||>) :: (f1 :~> (m :. g)) -> (f2 :~> (m :. g)) -> ((f1 :+: f2) :~> (m :. g)

getFirst,  outL :: (f :*: g) :~> f
getSecond, inL  :: (f :*: g) :~> g

(.&&&.) :: (f :~> g1) -> (f :~> g2) -> (f :~> (g1 :*: g2))
(<&&&>) :: (Applicative m) => (f :~> (m :. g1)) -> (f :~> (m :. g2)) -> (f :~> (m :. (g1 :*: g2)))
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:7 Changed 3 years ago by Iceland_jack

Purescript also includes this function for Data.Functor.Compose

bihoistCompose
  :: forall f g h i
   . Functor f
  => (f ~> h)
  -> (g ~> i)
  -> Compose f g
  ~> Compose h i
bihoistCompose natF natG (Compose fga) = Compose (natF (map natG fga))

And

o :: (Functor m, Functor n) => (b -> n c) -> (a -> m b) -> (a -> Compose m n c)
o f g = Compose . fmap f . g

From here.

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:8 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:9 Changed 3 years ago by Iceland_jack

Here is an interesting one, witnessing the isomorphism between Sum Identity and Control.Applicative.Lift.Lift

toLift :: Sum Identity g ~> Lift g
toLift = \case
  InL (Identity a) -> Pure a
  InR ga           -> Other ga

if it ever gets added to base, I emailed Ross Paterson about adding it along with some other functions to transformers.

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:10 Changed 3 years ago by Iceland_jack

e1 :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b
e1 f _ (L1 l) = f l
e1 _ f (R1 r) = f r

fst1 :: (f :*: g) a -> f a
fst1 (l :*: _) = l
snd1 :: (f :*: g) a -> g a
snd1 (_ :*: r) = r

are defined in one-liner

comment:11 Changed 3 years ago by Iceland_jack

Functions from some StackOverflow answer,

liftO :: (Functor f, Applicative g) => f ~> Compose f g
liftO = Compose . fmap pure

liftI :: Applicative f => g ~> Compose f g
liftI = Compose . pure

hoistO :: f ~> f' -> Compose f g ~> Compose f' g
hoistO eta = Compose . eta . getCompose

hoistI :: Functor f => g ~> g' -> Compose f g ~> Compose f g'
hoistI eta = Compose . fmap eta . getCompose

mapI :: Functor f => (g a -> g' a') -> ((Compose f g) a -> (Compose f g') a')
mapI f = Compose . fmap f . getCompose

mapI2 :: Applicative f => (g a -> g' a' -> g'' a'') -> ((Compose f g) a -> (Compose f g') a' -> (Compose f g'') a'')
mapI2 f (Compose fga) (Compose fhb) = Compose (fmap f fga <*> fhb)

Some of them may belong in Data.Functor.Compose.

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:12 Changed 3 years ago by RyanGlScott

Can I give you some honest advice, Iceland_jack?

I barely have any idea what this proposal is even about anymore. That's because you have been clogging this thread with clutter that doesn't pertain to the original proposal. Your argument doesn't become more convincing the more definitions you throw at us - in fact, it has quite the opposite effect! This thread is now so overloaded with tangentially related cruft that I suspect no one except the most masochistic lurkers will dare attempt to read it.

Sorry if that was harsh, but I feel that it needed to be said.

Proposals are best kept to a small, self-contained unit of information that is easily digestible. You did the right thing by starting a libraries mailing list discussion about (||||) and (&&&&) (and only (||||) and (&&&&))! In the particular case of this proposal, it hasn't seemed to have reached a consensus on the naming - and that's fine! All you need to do is figure out names that a majority of the community can agree with, and argue convincingly for it.

These other functions that you've put above are just distracting from the main thing you're trying to advocate for. Perhaps small subsets of them could be interesting proposals on their own. If so, start separate libraries discussions for them! But please don't bog down your own proposal by including everything under the sun.

Note: See TracTickets for help on using tickets.