Diagonalization/ dupe for monads and tuples?

[Carter Schonwald]

For the tuple monomorphic one id probably ageee with Dan.

On Thu, Sep 17, 2020 at 1:13 AM chessai <chessai1996 at gmail.com> wrote:

> dup and dedup? Just throwing out names. Not sure I'm a fan of diag/coding.
>
> On Thu, Sep 17, 2020, 00:10 Emily Pillmore <emilypi at cohomolo.gy> wrote:
>
>> Proposing the following names then to start, and we can talk about
>> expanding this at a later date:
>>
>> ```
>> -- In Data.Tuple
>> diag :: a → (a,a)
>> diag a = (a, a)
>>
>> -- In Data.Either
>> codiag :: Either a a → a
>> codiag = either id id
>> ```
>>
>> Thoughts?
>> Emily
>>
>>
>>
>> On Thu, Sep 17, 2020 at 12:55 AM, Asad Saeeduddin <masaeedu at gmail.com>
>> wrote:
>>
>>> `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> 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 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
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>>
>>>>
>>>> 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
>>
>>
>>
>
> _______________________________________________
>
> 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/20200917/850ffe53/attachment-0001.html>