Diagonalization/ dupe for monads and tuples?
Emily Pillmore
emilypi at cohomolo.gy
Thu Sep 17 01:08:35 UTC 2020
@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@ 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 )
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200917/2d4d93dc/attachment.html>
More information about the Libraries
mailing list