Zulip Chat Archive

Stream: general

Topic: products


view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip Patrick Massot (Jul 29 2018 at 23:27):

You're trying to scare me with your notations

view this post on Zulip Patrick Massot (Jul 29 2018 at 23:27):

It works pretty well

view this post on Zulip Simon Hudon (Jul 29 2018 at 23:28):

What works well? Scaring you or using the notation?

view this post on Zulip Patrick Massot (Jul 29 2018 at 23:28):

scaring me

view this post on Zulip Simon Hudon (Jul 29 2018 at 23:29):

Oh, good, so my work here is done

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jul 29 2018 at 23:34):

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

view this post on Zulip Simon Hudon (Jul 29 2018 at 23:36):

:+1:

view this post on Zulip Simon Hudon (Jul 29 2018 at 23:36):

Good night!

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:32):

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

view this post on Zulip 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!

view this post on Zulip 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: May 16 2021 at 05:21 UTC