Diagonalization/ dupe for monads and tuples?

Asad Saeeduddin masaeedu at gmail.com
Thu Sep 17 04:55:08 UTC 2020


`Either a a -> a` is another very handy operation. That and `a -> (a, 
a)` together make up 90% of use cases for `duplicate :: p x (t x x)`.

On 9/17/20 12:49 AM, Edward Kmett wrote:
> 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 
> <mailto: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 <mailto: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 <mailto: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
>>             <mailto: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 <mailto: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 <mailto:Libraries at haskell.org>
>>                 http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>>
>>
>>             _______________________________________________
>>             Libraries mailing list
>>             Libraries at haskell.org  <mailto:Libraries at haskell.org>
>>             http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>             _______________________________________________
>             Libraries mailing list
>             Libraries at haskell.org <mailto:Libraries at haskell.org>
>             http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
>     _______________________________________________
>     Libraries mailing list
>     Libraries at haskell.org <mailto: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/20200917/dfde86a2/attachment-0001.html>


More information about the Libraries mailing list