Diagonalization/ dupe for monads and tuples?
Emily Pillmore
emilypi at cohomolo.gy
Thu Sep 17 05:09:41 UTC 2020
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@ cohomolo. gy (
>> 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@ cohomolo. gy (
>>> 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@ gmail. com (
>>>> 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@ gmail.
>>>>>> com ( 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@ gmail. com
>>>>>>> ( 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@ haskell. org ( Libraries at haskell.org )
>>>>>>> http:/ / mail. haskell. org/ cgi-bin/ mailman/ listinfo/ libraries (
>>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries )
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>> _______________________________________________
>>>>>> Libraries mailing list
>>>>>> Libraries@ haskell. org ( Libraries at haskell.org )
>>>>>> http:/ / mail. haskell. org/ cgi-bin/ mailman/ listinfo/ libraries (
>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries )
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> Libraries mailing list
>>>>> Libraries@ haskell. org ( Libraries at haskell.org )
>>>>> http:/ / mail. haskell. org/ cgi-bin/ mailman/ listinfo/ libraries (
>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries )
>>>>>
>>>>>
>>>>>
>>>>
>>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> Libraries mailing list
>>> Libraries@ haskell. org ( Libraries at haskell.org )
>>> http:/ / mail. haskell. org/ cgi-bin/ mailman/ listinfo/ libraries (
>>> 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/518ba505/attachment.html>
More information about the Libraries
mailing list