Zulip Chat Archive

Stream: general

Topic: products


Patrick Massot (Jul 29 2018 at 23:00):

If I have (a b c : Type) (f : a → b) (g : a → c), do we have a name or notation for the function mapping x to (f x, g x)?

Sebastian Ullrich (Jul 29 2018 at 23:20):

We probably don't yet, but Haskell has one, if anyone wants to copy that

> :t (&&&)
(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c')
> :t snd &&& fst
snd &&& fst :: (a, c) -> (c, a)

where Arrow is an abstraction of functions https://wiki.haskell.org/Arrow_tutorial

Simon Hudon (Jul 29 2018 at 23:25):

For this particular operator, applicative is sufficient: x &&& y = prod.mk <$> x <*> y

(that is to say, we only need applicative (a b))

Patrick Massot (Jul 29 2018 at 23:27):

You're trying to scare me with your notations

Patrick Massot (Jul 29 2018 at 23:27):

It works pretty well

Simon Hudon (Jul 29 2018 at 23:28):

What works well? Scaring you or using the notation?

Patrick Massot (Jul 29 2018 at 23:28):

scaring me

Simon Hudon (Jul 29 2018 at 23:29):

Oh, good, so my work here is done

Simon Hudon (Jul 29 2018 at 23:32):

As far as I know, the definition is not in mathlib so you make it as simple as you need and leave it to others to generalize so that it looks more like Haskell (the generalization has a few stumbling blocks I think)

Patrick Massot (Jul 29 2018 at 23:34):

Ok, I may do that. But first I'll sleep. Thanks!

Simon Hudon (Jul 29 2018 at 23:36):

:+1:

Simon Hudon (Jul 29 2018 at 23:36):

Good night!

Nicholas Scheel (Jul 30 2018 at 14:47):

here’s some discussion on the Arrow class: https://www.eyrie.org/~zednenem/2017/07/twist

PureScript has opted not to create an Arrow class (see link 3 above); instead it just defined (&&&) using Strong and Category: https://pursuit.purescript.org/packages/purescript-profunctor/4.0.0/docs/Data.Profunctor.Strong#v:fanout

Simon Hudon (Jul 30 2018 at 15:32):

I think in Haskell as well, people think Arrow might not have been the right abstraction

Sebastian Ullrich (Jul 30 2018 at 15:46):

PureScript has opted not to create an Arrow class (see link 3 above); instead it just defined (&&&) using Strong and Category: https://pursuit.purescript.org/packages/purescript-profunctor/4.0.0/docs/Data.Profunctor.Strong#v:fanout

Is there actually any implementation anywhere apart from Function :sweat_smile: ? But thanks for the information!

Nicholas Scheel (Jul 30 2018 at 16:19):

haha, we can go one step away from Function with Star :wink: https://github.com/purescript/purescript-profunctor/blob/v4.0.0/src/Data/Profunctor/Star.purs#L70 (actually that package has a variety of profunctors, a number of which implement Strong)


Last updated: Dec 20 2023 at 11:08 UTC