Re: Diagonalization/ dupe for monads and tuples?

For the tuple monomorphic one id probably ageee with Dan. On Thu, Sep 17, 2020 at 1:13 AM chessai 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 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 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 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

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

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

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 > > 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 > > > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > > > > > > >

_______________________________________________

Libraries mailing list

Libraries@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________

Libraries mailing list

Libraries@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________

Libraries mailing list

Libraries@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________

Libraries mailing list

Libraries@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________

Libraries mailing list

Libraries@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries