2026/06/29

Newest at the top

2026-06-29 01:12:56 +0000 <schuelermine> so is the adjoint Two ⊢ Id?
2026-06-29 01:06:52 +0000tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: dnvln)
2026-06-29 01:06:25 +0000czan(~czan@user/mange) czan
2026-06-29 00:58:08 +0000vgtw(~vgtw@user/vgtw) vgtw
2026-06-29 00:55:37 +0000vgtw(~vgtw@user/vgtw) (Ping timeout: 276 seconds)
2026-06-29 00:44:07 +0000mikess(~sam@S010664777dafd303.cg.shawcable.net) (Ping timeout: 265 seconds)
2026-06-29 00:34:48 +0000ttybitnik(~ttybitnik@user/wolper) (Quit: Fading out...)
2026-06-29 00:33:03 +0000finsternis(~X@23.226.237.192) finsternis
2026-06-29 00:26:17 +0000xff0x(~xff0x@2405:6580:b080:900:f87a:2927:c6fc:9f80) (Ping timeout: 248 seconds)
2026-06-29 00:24:56 +0000xff0x_(~xff0x@2405:6580:b080:900:2b7:99fc:bbb9:7b1b)
2026-06-29 00:07:09 +0000 <monochrom> Err, Two is the diagonal functor itself heh.
2026-06-28 23:52:51 +0000weary-traveler(~user@user/user363627) (Ping timeout: 252 seconds)
2026-06-28 23:50:46 +0000acidjnk(~acidjnk@p200300d6e74def721d5abc156f9177ce.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2026-06-28 23:50:44 +0000acidjnk_new3(~acidjnk@p200300d6e74def721d5abc156f9177ce.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
2026-06-28 23:50:14 +0000user363627(~user@user/user363627) user363627
2026-06-28 23:47:04 +0000YoungFrog(~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) youngfrog
2026-06-28 23:45:15 +0000 <EvanR> Functor + ContraFunctor was the one that requires triviality
2026-06-28 23:44:40 +0000 <schuelermine> I see
2026-06-28 23:44:20 +0000 <EvanR> it's both
2026-06-28 23:43:27 +0000 <monochrom> Perhaps it's both.
2026-06-28 23:43:09 +0000 <monochrom> (That was what I spent one hour on. To obtain a formula for join, I factored Two, then used the well-known formula from the factoring.)
2026-06-28 23:42:37 +0000 <schuelermine> monochrom: I thought Stream was a comonad
2026-06-28 23:41:49 +0000 <monochrom> There is a pun/irony in this. Every monad can be factored as the composition of a pair of adjoint functors. If you do this to Two or Stream, the corresponding "diagonal functor" shows up.
2026-06-28 23:38:34 +0000 <monochrom> To be sure, the slick way is, just like (a,a) being Bool->a, Stream a is Natural->a.
2026-06-28 23:36:15 +0000 <monochrom> haha
2026-06-28 23:35:56 +0000 <EvanR> yeah but (b,x) is also a diagonal see xD (one that the infinite matrix doesn't have)
2026-06-28 23:35:29 +0000 <monochrom> Analogously, if you write (a,b) and (x,y) on two rows and see a 2x2 matrix, (a,y) is the diagonal.
2026-06-28 23:34:28 +0000YoungFrog(~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Ping timeout: 256 seconds)
2026-06-28 23:34:14 +0000 <monochrom> Or rather, the two identity laws want join to take the diagonal.
2026-06-28 23:33:42 +0000marinelli(~weechat@gateway/tor-sasl/marinelli) marinelli
2026-06-28 23:33:39 +0000 <monochrom> Stream (Stream a) is a infinite matrix. join will want its diagonal.
2026-06-28 23:33:15 +0000 <monochrom> Now generalize to "data Stream a = S a (Stream a)"!
2026-06-28 23:31:31 +0000marinelli(~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 245 seconds)
2026-06-28 23:30:35 +0000 <EvanR> (A,B) is the type which keeps on giving
2026-06-28 23:29:42 +0000 <monochrom> :)
2026-06-28 23:29:38 +0000 <EvanR> ok got it
2026-06-28 23:29:09 +0000 <schuelermine> uhhh I’m confused
2026-06-28 23:28:59 +0000 <schuelermine> sry I got it wrong
2026-06-28 23:28:55 +0000 <schuelermine> wait
2026-06-28 23:28:45 +0000 <EvanR> 🤔
2026-06-28 23:28:44 +0000 <schuelermine> *fmap id
2026-06-28 23:28:41 +0000 <schuelermine> do you mean join . fmap pure = id
2026-06-28 23:21:34 +0000 <monochrom> Breaks join . pure = id
2026-06-28 23:20:21 +0000 <EvanR> use platonic / morally correct / vibes haskell
2026-06-28 23:20:05 +0000 <EvanR> that's fine
2026-06-28 23:19:57 +0000 <schuelermine> which is annoying
2026-06-28 23:19:50 +0000 <schuelermine> join isn’t in Monad so you can’t define join and have bind automatically work
2026-06-28 23:19:22 +0000 <EvanR> join ((a,b),(x,y)) = (b,x) ought to also work?
2026-06-28 23:18:51 +0000tremon(~tremon@83-80-159-219.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in)
2026-06-28 23:15:00 +0000 <schuelermine> courtesy of pointfree.io