products

Stream: general

[Patrick Massot]

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]

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]

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]

You're trying to scare me with your notations

[Patrick Massot]

It works pretty well

[Simon Hudon]

What works well? Scaring you or using the notation?

[Patrick Massot]

scaring me

[Simon Hudon]

Oh, good, so my work here is done

[Simon Hudon]

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]

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

[Simon Hudon]

:+1:

[Simon Hudon]

Good night!

[Nicholas Scheel]

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]

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

[Sebastian Ullrich]

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]

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)