Diagonalization/ dupe for monads and tuples?
Carter Schonwald
carter.schonwald at gmail.com
Thu Sep 17 13:48:10 UTC 2020
Out of curiosity what have been your uses for symmetric monoidal categories?
Few things I’d like to remark upon :
1) in many models that are monoidal braided categories , Eg full linear
logic, there’s at least two sum types and two product types.
2) in my own experience in that setting, at least for modelling
authorization, I wind up wanting dup to take an evidence argument, which
leads to duplicate With proof being in its own class and the proof term
being an associated type / fun dep wrt the thing we duplicate.
Eg dup:: DupProof a p => a-> p-> (a,a)
(And in fact something like this is needed to enable njce desugaring for
pattern matching guard computations for stuff like linear Haskell I think.
3) the in practice dual for duplicate with evidence seems to be more like
use :: UseProof a p => (a,p) -> (), at least in general and ignoring a
bunch of nuances that can lead to different choices in signatures
On Thu, Sep 17, 2020 at 12:56 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200917/f649bd8f/attachment.html>
More information about the Libraries
mailing list