Diagonalization/ dupe for monads and tuples?

[Edward Kmett]

For what it's worth, I'd just like to see a no-nonsense

dup : a -> (a,a)
dup a = (a,a)

in Data.Tuple, where it is out of the way, but right where you'd expect it
to be when looking for something for working with tuples.

Yes, bipure and id &&& id exist, and generalize it on two incompatible
axes, and if we had a proper cartesian category we'd be able to supply this
in full generality, as a morphism to the diagonal functor, but all of these
require a level of rocket science to figure out.

I'd also happily support adding the equivalent in Data.Either for Either a
a -> a, which invites bikeshedding names.

-Edward

On Wed, Sep 16, 2020 at 6:10 PM Emily Pillmore <emilypi at cohomolo.gy> wrote:

> Just to clarify, that's not the "real" diagonal in the space, but it is a
> super useful translation that I'd like for free :)
>
>
> On Wed, Sep 16, 2020 at 9:08 PM, Emily Pillmore <emilypi at cohomolo.gy>
> wrote:
>
>> @Asad that's a perfectly reasonable way to think about diagonal
>> operations: as the data of a cartesian monoidal category, and the laws are
>> correct in this case. I think we can get away with the additional
>> abstraction to `Biapplicative` in this case, though.
>>
>> wouldn't the existence of appropriate `forall a. a -> t a a` and `forall
>> a. x -> Unit t` functions pigeonhole it into being "the" cartesian monoidal
>> structure on `->` (and thus naturally isomorphic to `(,)`)?
>>
>>
>> Only if you chose that particular unit and that particular arrow. But
>> there are other places where having a general `Biapplicative` contraint
>> would make it useful. For example,  i'd like to use this in `smash` with
>> `diag :: a → Smash a a`, defining the adjoining of a point to `a` and
>> creating a diagonal in the subcategory of pointed spaces in Hask, so that I
>> don't have to redefine this as `diag' = quotSmash . view _CanIso . diag .
>> Just`.
>>
>> Cheers,
>> Emily
>>
>>
>>
>>
>>
>>
>>
>> On Wed, Sep 16, 2020 at 6:35 PM, Asad Saeeduddin <masaeedu at gmail.com>
>> wrote:
>>
>>> Whoops, I just realized I've been responding to Carter specifically
>>> instead of to the list.
>>>
>>> I was having some trouble understanding the `unJoin` stuff but I read it
>>> a few more times and I think I understand it a little better now.
>>>
>>> In my personal experience the "abstracted version" of `x -> (x, x)` I
>>> use most often looks like this:
>>>
>>> ```
>>>
>>> class SymmetricMonoidal t i p => CartesianMonoidal t i p
>>>
>>>   where
>>>
>>>   duplicate :: p x (x `t` x)
>>>
>>>   discard :: p x i
>>>
>>>
>>> -- Laws:
>>>
>>> -- duplicate >>> first  discard = fwd lunit
>>>
>>> -- duplicate >>> second discard = fwd runit
>>>
>>>
>>> -- where
>>>
>>> -- lunit :: Monoidal t i p => Iso p x (i `t` x)
>>>
>>> -- runit :: Monoidal t i p => Iso p x (x `t` i)
>>>
>>> ```
>>>
>>> i.e. adding a suitable duplicate and discard to some symmetric monoidal
>>> structure gives us a cartesian monoidal structure.
>>>
>>> This doesn't really seem to be relevant to what you folks are looking
>>> for, but it does bring up a question. If some `Bifunctor` `t` happens to
>>> form a monoidal structure on `->`, wouldn't the existence of appropriate
>>> `forall a. a -> t a a` and `forall a. x -> Unit t` functions pigeonhole it
>>> into being "the" cartesian monoidal structure on `->` (and thus naturally
>>> isomorphic to `(,)`)?
>>> On 9/16/20 5:26 PM, Emily Pillmore wrote:
>>>
>>> Nice!
>>>
>>> That's kind of what I was going for with Carter earlier in the day,
>>> thanks Matthew.
>>>
>>> I think a diagonalization function and functor are both very sensible
>>> additions to `bifunctors` and `Data.Bifunctor`. The theory behind this is
>>> sound: The diagonalization functor Δ: Hask → Hask^Hask, forms the center of
>>> the adjoint triple `colim -| Δ -| lim : Hask → Hask^Hask`.
>>>
>>> Certainly the function `diag :: a → (a,a)` is something I've seen
>>> written in several libraries, and should be included in `Data.Tuple` as a
>>> `base` function. The clear generalization of this function is `diag ::
>>> Biapplicative f ⇒ a → f a a`. I'm in favor of both existing in their
>>> separate capacities.
>>>
>>> Thoughts?
>>>
>>> Emily
>>>
>>>
>>> On Wed, Sep 16, 2020 at 3:49 PM, Carter Schonwald <
>>> carter.schonwald at gmail.com> wrote:
>>>
>>>> Is the join bipure definition taking advantage of the (a->) monad
>>>> instance?  Slick!
>>>>
>>>>
>>>> On Wed, Sep 16, 2020 at 3:39 PM Matthew Farkas-Dyck <
>>>> strake888 at gmail.com> wrote:
>>>>
>>>>> We also have
>>>>>
>>>>>
>>>>>
>>>>> diag = join bipure
>>>>>
>>>>>
>>>>>
>>>>> and (in pseudo-Haskell)
>>>>>
>>>>>
>>>>>
>>>>> diag = unJoin . pure
>>>>>
>>>>>   where
>>>>>
>>>>>     newtype Join f a = Join { unJoin :: f a a } deriving (Functor)
>>>>>
>>>>>     deriving instance Biapplicative f => Applicative (Join f)
>>>>>
>>>>>
>>>>>
>>>>> The latter seems on its face potentially related to the instance for
>>>>>
>>>>> lists of fixed length, but i am not sure how deep the connection may
>>>>>
>>>>> be.
>>>>>
>>>>> _______________________________________________
>>>> Libraries mailing list
>>>> Libraries at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>
>>>
>>>
>>> _______________________________________________
>>> Libraries mailing listLibraries at haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>> _______________________________________________
>>> Libraries mailing list
>>> Libraries at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200916/018ad9eb/attachment.html>