<div dir="auto">Out of curiosity what have been your uses for symmetric monoidal categories?</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">Few things I’d like to remark upon : </div><div dir="auto">1) in many models that are monoidal braided categories , Eg full linear logic, there’s at least two sum types and two product types.  </div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">  Eg dup:: DupProof a p => a-> p-> (a,a)</div><div dir="auto">(And in fact something like this is needed to enable njce desugaring for pattern matching guard computations for stuff like linear Haskell I think.  </div><div dir="auto"><br></div><div dir="auto">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 </div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto"><br></div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Sep 17, 2020 at 12:56 AM Asad Saeeduddin <<a href="mailto:masaeedu@gmail.com">masaeedu@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"><br><br>  <br><br>    <br><br>  <br><br>  <div><br><br>    <p>`Either a a -> a` is another very handy operation. That and `a<br><br>      -> (a, a)` together make up 90% of use cases for `duplicate ::<br><br>      p x (t x x)`.<br><br><br>    </p></div><div><br><br>    <div>On 9/17/20 12:49 AM, Edward Kmett<br><br>      wrote:<br><br><br>    </div><br><br>    <blockquote type="cite"><br><br>      <br><br>      <div dir="ltr">For what it's worth, I'd just like to see a<br><br>        no-nonsense <br><br>        <div><br><br><br>        </div><br><br>        <div><font face="monospace" style="font-family:monospace;color:rgb(0,0,0)">dup : a -> (a,a)</font></div><br><br>        <div><font face="monospace" style="font-family:monospace;color:rgb(0,0,0)">dup a = (a,a)</font></div><br><br>        <div><br><br><br>        </div><br><br>        <div>in <font face="monospace" style="font-family:monospace;color:rgb(0,0,0)">Data.Tuple</font>, where it is<br><br>          out of the way, but right where you'd expect it to be when<br><br>          looking for something for working with tuples.</div><br><br>        <div><br><br><br>        </div><br><br>        <div>Yes, <font face="monospace" style="font-family:monospace;color:rgb(0,0,0)">bipure</font> and <font face="monospace" style="font-family:monospace;color:rgb(0,0,0)">id &&& id</font> exist, and<br><br>          generalize it on two incompatible axes, and if we had a proper<br><br>          cartesian category we'd be able to supply this in full<br><br>          generality, as a morphism to the diagonal functor, but all of<br><br>          these require a level of rocket science to figure out.</div><br><br>        <div><br><br><br>        </div><br><br>        <div>I'd also happily support adding the equivalent in <font face="monospace" style="font-family:monospace;color:rgb(0,0,0)">Data.Either</font> for <font face="monospace" style="font-family:monospace;color:rgb(0,0,0)">Either a a -> a</font>, which invites<br><br>          bikeshedding names.</div><br><br>        <div><br><br><br>        </div><br><br>        <div>-Edward</div><br><br>      </div><br><br>      <br><br><br>      <div class="gmail_quote"><br><br>        <div dir="ltr" class="gmail_attr">On Wed, Sep 16, 2020 at 6:10<br><br>          PM Emily Pillmore <<a href="mailto:emilypi@cohomolo.gy" target="_blank">emilypi@cohomolo.gy</a>> wrote:<br><br><br>        </div><br><br>        <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"><br><br>          <div><br><br>            <div><br><br>              <div><br><br>                <div style="display:none;border:0px;width:0px;height:0px;overflow:hidden"><img src="https://r.superhuman.com/0Wx-exEsht6lpb99fo4UQiWIkL98SYOEzLJUv1QFFhli5bllkNoHDBLsayQDodhx8cUxnSyJTqe7dnp6-rT9qAIxGYEoTGbjxFniaPkNXNYPNGwW28U3w7OH-Ha5dqTJNOY5Lv3a8yLSaZJO9r_ZF2xLtuAYQQTH7MWHJvQSHLQU2hbjV-rdY8M.gif" alt="" style="display: none; border: 0px; width: 0px; height: 0px; overflow: hidden;" width="1" height="0"></div><br><br>                <div><br><br>                  <div><br><br>                    <div>Just to clarify, that's not the "real" diagonal<br><br>                      in the space, but it is a super useful translation<br><br>                      that I'd like for free :)</div><br><br>                  </div><br><br>                  <br><br><br>                </div><br><br>                <br><br><br>                <div><br><br>                  <div class="gmail_quote">On Wed, Sep 16, 2020 at 9:08<br><br>                    PM, Emily Pillmore <span dir="ltr"><<a href="mailto:emilypi@cohomolo.gy" target="_blank">emilypi@cohomolo.gy</a>></span><br><br>                    wrote:<br><br><br>                    <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"><br><br>                      <div class="gmail_extra"><br><br>                        <div class="gmail_quote" id="m_5621040664659163393gmail-m_7220689800887981291null"><br><br>                          <div><br><br>                            <div><br><br>                              <div><br><br>                                <div>@Asad that's a perfectly reasonable<br><br>                                  way to think about diagonal<br><br>                                  operations: as the data of a cartesian<br><br>                                  monoidal category, and the laws are<br><br>                                  correct in this case. I think we can<br><br>                                  get away with the additional<br><br>                                  abstraction to `Biapplicative` in this<br><br>                                  case, though.<br><br><br>                                </div><br><br>                                <div><br><br><br>                                </div><br><br>                                <blockquote><br><br>                                  <div style="text-decoration:none"><br><br>                                    <div style="text-decoration:none"><br><br>                                      <div><br><br>                                        <div><br><br>                                          <div><br><br>                                            <div><br><br>                                              <div><br><br>                                                <div><br><br>                                                  <div><br><br>                                                    <p style="margin:0px">wouldn't<br><br>                                                      the existence of<br><br>                                                      appropriate<br><br>                                                      `forall a. a -><br><br>                                                      t a a` and `forall<br><br>                                                      a. x -> Unit t`<br><br>                                                      functions<br><br>                                                      pigeonhole it into<br><br>                                                      being "the"<br><br>                                                      cartesian monoidal<br><br>                                                      structure on<br><br>                                                      `->` (and thus<br><br>                                                      naturally<br><br>                                                      isomorphic to<br><br>                                                      `(,)`)?<br><br><br>                                                    </p><br><br>                                                  </div><br><br>                                                </div><br><br>                                              </div><br><br>                                            </div><br><br>                                          </div><br><br>                                        </div><br><br>                                      </div><br><br>                                    </div><br><br>                                  </div><br><br>                                </blockquote><br><br>                                <div><br><br>                                  <div><br><br><br>                                  </div><br><br>                                  <div>Only if you chose that particular<br><br>                                    unit and that particular arrow. But<br><br>                                    there are other places where having<br><br>                                    a general `Biapplicative` contraint<br><br>                                    would make it useful. For example,<br><br>                                     i'd like to use this in `smash`<br><br>                                    with `diag :: a → Smash a a`,<br><br>                                    defining the adjoining of a point to<br><br>                                    `a` and creating a diagonal in the<br><br>                                    subcategory of pointed spaces in<br><br>                                    Hask, so that I don't have to<br><br>                                    redefine this as `diag' = quotSmash<br><br>                                    . view _CanIso . diag . Just`. <br><br><br>                                  </div><br><br>                                  <div><br><br><br>                                  </div><br><br>                                  <div>Cheers,<br><br><br>                                  </div><br><br>                                  <div>Emily</div><br><br>                                  <div><br><br><br>                                  </div><br><br>                                  <div><br><br><br>                                  </div><br><br>                                  <div><br><br><br>                                  </div><br><br>                                  <div><br><br><br>                                  </div><br><br>                                </div><br><br>                                <div><br><br><br>                                </div><br><br>                              </div><br><br>                              <br><br><br>                            </div><br><br>                            <br><br><br>                            <div><br><br>                              <div class="gmail_quote">On Wed, Sep 16,<br><br>                                2020 at 6:35 PM, Asad Saeeduddin <span dir="ltr"><<a href="mailto:masaeedu@gmail.com" rel="noopener noreferrer" target="_blank">masaeedu@gmail.com</a>></span><br><br>                                wrote:<br><br><br>                                <blockquote style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)" class="gmail_quote"><br><br>                                  <div class="gmail_extra"><br><br>                                    <div id="m_5621040664659163393gmail-m_7220689800887981291null" class="gmail_quote"><br><br>                                      <p>Whoops, I just realized I've<br><br>                                        been responding to Carter<br><br>                                        specifically instead of to the<br><br>                                        list.<br><br><br>                                        <br><br><br>                                        I was having some trouble<br><br>                                        understanding the `unJoin` stuff<br><br>                                        but I read it a few more times<br><br>                                        and I think I understand it a<br><br>                                        little better now.<br><br><br>                                        <br><br><br>                                        In my personal experience the<br><br>                                        "abstracted version" of `x -><br><br>                                        (x, x)` I use most often looks<br><br>                                        like this:<br><br><br>                                        <br><br><br>                                        ```<br><br><br>                                      </p><br><br>                                      <pre style="font-family:monospace">class SymmetricMonoidal t i p => CartesianMonoidal t i p</pre><br><br>                                      <pre style="font-family:monospace">  where</pre><br><br>                                      <pre style="font-family:monospace">  duplicate :: p x (x `t` x)</pre><br><br>                                      <pre style="font-family:monospace">  discard :: p x i<br><br><br><br></pre><br><br>                                      <pre style="font-family:monospace">-- Laws:</pre><br><br>                                      <pre style="font-family:monospace">-- duplicate >>> first  discard = fwd lunit</pre><br><br>                                      <pre style="font-family:monospace">-- duplicate >>> second discard = fwd runit<br><br><br><br></pre><br><br>                                      <pre style="font-family:monospace">-- where</pre><br><br>                                      <pre style="font-family:monospace">-- lunit :: Monoidal t i p => Iso p x (i `t` x)</pre><br><br>                                      <pre style="font-family:monospace">-- runit :: Monoidal t i p => Iso p x (x `t` i)</pre><br><br>                                      <p>```<br><br><br>                                        <br><br><br>                                        i.e. adding a suitable duplicate<br><br>                                        and discard to some symmetric<br><br>                                        monoidal structure gives us a<br><br>                                        cartesian monoidal structure.<br><br><br>                                        <br><br><br>                                        This doesn't really seem to be<br><br>                                        relevant to what you folks are<br><br>                                        looking for, but it does bring<br><br>                                        up a question. If some<br><br>                                        `Bifunctor` `t` happens to form<br><br>                                        a monoidal structure on `->`,<br><br>                                        wouldn't the existence of<br><br>                                        appropriate `forall a. a -> t<br><br>                                        a a` and `forall a. x -> Unit<br><br>                                        t` functions pigeonhole it into<br><br>                                        being "the" cartesian monoidal<br><br>                                        structure on `->` (and thus<br><br>                                        naturally isomorphic to `(,)`)?</p><br><br>                                      <div>On 9/16/20 5:26 PM, Emily<br><br>                                        Pillmore wrote:<br><br><br>                                      </div><br><br>                                      <blockquote type="cite"><br><br>                                        <div><br><br>                                          <div><br><br>                                            <div><br><br>                                              <div><br><br>                                                <div>Nice! <br><br><br>                                                  <br><br><br>                                                  That's kind of what I<br><br>                                                  was going for with<br><br>                                                  Carter earlier in the<br><br>                                                  day, thanks Matthew. </div><br><br>                                                <div><br><br><br>                                                </div><br><br>                                                <div>I think a<br><br>                                                  diagonalization<br><br>                                                  function and functor<br><br>                                                  are both very sensible<br><br>                                                  additions to<br><br>                                                  `bifunctors` and<br><br>                                                  `Data.Bifunctor`. The<br><br>                                                  theory behind this is<br><br>                                                  sound: The<br><br>                                                  diagonalization<br><br>                                                  functor Δ: Hask →<br><br>                                                  Hask^Hask, forms the<br><br>                                                  center of the adjoint<br><br>                                                  triple `colim -| Δ -|<br><br>                                                  lim : Hask →<br><br>                                                  Hask^Hask`. <br><br><br>                                                  <br><br><br>                                                  Certainly the function<br><br>                                                  `diag :: a → (a,a)` is<br><br>                                                  something I've seen<br><br>                                                  written in several<br><br>                                                  libraries, and should<br><br>                                                  be included in<br><br>                                                  `Data.Tuple` as a<br><br>                                                  `base` function. The<br><br>                                                  clear generalization<br><br>                                                  of this function is<br><br>                                                  `diag :: Biapplicative<br><br>                                                  f ⇒ a → f a a`. I'm in<br><br>                                                  favor of both existing<br><br>                                                  in their separate<br><br>                                                  capacities. </div><br><br>                                                <div><br><br><br>                                                </div><br><br>                                                <div>Thoughts? <br><br><br>                                                </div><br><br>                                                <div><br><br><br>                                                </div><br><br>                                                <div>Emily</div><br><br>                                              </div><br><br>                                              <br><br><br>                                            </div><br><br>                                            <br><br><br>                                            <div><br><br>                                              <div class="gmail_quote">On<br><br>                                                Wed, Sep 16, 2020 at<br><br>                                                3:49 PM, Carter<br><br>                                                Schonwald <span dir="ltr"><<a rel="noopener<br><br>                                                    noreferrer" href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>></span><br><br>                                                wrote:<br><br><br>                                                <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"><br><br>                                                  <div class="gmail_extra"><br><br>                                                    <div class="gmail_quote" id="m_5621040664659163393gmail-m_7220689800887981291null"><br><br>                                                      <div dir="auto">Is<br><br>                                                        the join bipure<br><br>                                                        definition<br><br>                                                        taking advantage<br><br>                                                        of the (a->)<br><br>                                                        monad instance? <br><br>                                                        Slick!</div><br><br>                                                      <div dir="auto"><br><br><br>                                                      </div><br><br>                                                      <div dir="auto"><br><br><br>                                                      </div><br><br>                                                      <div><br><br>                                                        <div class="gmail_quote"><br><br>                                                          <div class="gmail_attr" dir="ltr">On<br><br>                                                          Wed, Sep 16,<br><br>                                                          2020 at 3:39<br><br>                                                          PM Matthew<br><br>                                                          Farkas-Dyck<br><br>                                                          <<a href="mailto:strake888@gmail.com" rel="noopener<br><br>                                                          noreferrer" target="_blank">strake888@gmail.com</a>> wrote:<br><br><br>                                                          </div><br><br>                                                          <blockquote style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)" class="gmail_quote">We also have<br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          diag = join<br><br>                                                          bipure<br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          and (in<br><br>                                                          pseudo-Haskell)<br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          diag = unJoin<br><br>                                                          . pure<br><br><br>                                                          <br><br><br>                                                            where<br><br><br>                                                          <br><br><br>                                                              newtype<br><br>                                                          Join f a =<br><br>                                                          Join { unJoin<br><br>                                                          :: f a a }<br><br>                                                          deriving<br><br>                                                          (Functor)<br><br><br>                                                          <br><br><br>                                                              deriving<br><br>                                                          instance<br><br>                                                          Biapplicative<br><br>                                                          f =><br><br>                                                          Applicative<br><br>                                                          (Join f)<br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          <br><br><br>                                                          The latter<br><br>                                                          seems on its<br><br>                                                          face<br><br>                                                          potentially<br><br>                                                          related to the<br><br>                                                          instance for<br><br><br>                                                          <br><br><br>                                                          lists of fixed<br><br>                                                          length, but i<br><br>                                                          am not sure<br><br>                                                          how deep the<br><br>                                                          connection may<br><br><br>                                                          <br><br><br>                                                          be.<br><br><br>                                                          <br><br><br>                                                          </blockquote><br><br>                                                        </div><br><br>                                                      </div><br><br>                                                      <p>_______________________________________________<br><br>                                                        <br><br><br>                                                        Libraries<br><br>                                                        mailing list <br><br><br>                                                        <a rel="noopener<br><br>                                                          noreferrer" href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a> <br><br><br>                                                        <a rel="noopener<br><br>                                                          noreferrer" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a></p><br><br>                                                    </div><br><br>                                                  </div><br><br>                                                </blockquote><br><br>                                              </div><br><br>                                            </div><br><br>                                            <br><br><br>                                          </div><br><br>                                        </div><br><br>                                        <br><br><br>                                        <fieldset></fieldset><br><br>                                        <pre style="font-family:monospace">_______________________________________________<br><br>Libraries mailing list<br><br><a rel="noopener noreferrer" href="mailto:Libraries@haskell.org" target="_blank" style="font-family:monospace">Libraries@haskell.org</a><br><br><a rel="noopener noreferrer" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank" style="font-family:monospace">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br><br></pre><br><br>                                      </blockquote><br><br>                                      <p>_______________________________________________<br><br>                                        <br><br><br>                                        Libraries mailing list<br><br>                                        <br><br><br>                                        <a href="mailto:Libraries@haskell.org" rel="noopener noreferrer" target="_blank">Libraries@haskell.org</a><br><br>                                        <br><br><br>                                        <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noopener noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a></p><br><br>                                    </div><br><br>                                  </div><br><br>                                </blockquote><br><br>                              </div><br><br>                            </div><br><br>                          </div><br><br>                        </div><br><br>                      </div><br><br>                    </blockquote><br><br>                  </div><br><br>                </div><br><br>                <br><br><br>              </div><br><br>            </div><br><br>          </div><br><br>          _______________________________________________<br><br><br>          Libraries mailing list<br><br><br>          <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br><br><br>          <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br><br><br>        </blockquote><br><br>      </div><br><br>    </blockquote><br><br>  </div><br><br><br><br>_______________________________________________<br><br>Libraries mailing list<br><br><a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br><br></blockquote></div></div>