Logs: freenode/#haskell
| 2021-04-25 01:13:57 | <zebrag> | yes |
| 2021-04-25 01:14:40 | <zebrag> | duplicate duplicate must go to duplicate |
| 2021-04-25 01:14:41 | <edwardk> | extract :: Monoid a => [a] -> a -- gets to be 'fold' basically. knowing the target monoid. |
| 2021-04-25 01:14:48 | <edwardk> | U here is basically invisible in haskell |
| 2021-04-25 01:14:59 | <edwardk> | i can put it in for clarity if needs must |
| 2021-04-25 01:15:08 | <zebrag> | no it ok |
| 2021-04-25 01:16:47 | <zebrag> | it's* |
| 2021-04-25 01:16:49 | <edwardk> | and duplicate takes FU -> FUFU by fmapping the 'pure' over the list you gave. dup :: [a] -> [[a]] -- is also a monoid homomorphism, but which takes [1,2,3] -> [[1],[2],[3]] iirc |
| 2021-04-25 01:17:01 | <edwardk> | its been a while since i worked this through in detail. |
| 2021-04-25 01:17:28 | <zebrag> | hehe |
| 2021-04-25 01:17:50 | <edwardk> | and yes, it sounds like some anime villainess going on about fufufufu... |
| 2021-04-25 01:18:03 | <zebrag> | I think I got where I've made a mistake: in the duplicate |
| 2021-04-25 01:18:17 | <edwardk> | great |
| 2021-04-25 01:18:23 | <edwardk> | lemme know if you're still stuck |
| 2021-04-25 01:18:31 | <zebrag> | nice, thaks |
| 2021-04-25 01:19:15 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-25 01:19:41 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 240 seconds) |
| 2021-04-25 01:19:56 | <zebrag> | Really helpful, great |
| 2021-04-25 01:22:51 | → | nineonine joins (~nineonine@50.216.62.2) |
| 2021-04-25 01:24:47 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 2021-04-25 01:27:23 | → | shailangsa joins (~shailangs@host86-185-58-137.range86-185.btcentralplus.com) |
| 2021-04-25 01:27:41 | × | nineonine quits (~nineonine@50.216.62.2) (Ping timeout: 265 seconds) |
| 2021-04-25 01:27:54 | <shachaf> | You have a function eta : a -> [a] and a a monoid homomorphism eps : [m] -> m, and the two triangle laws are that eps . F eta = id and U eps . eta = id |
| 2021-04-25 01:28:22 | <shachaf> | That is, fold (map (:[]) xs) = xs, and fold [x] = x |
| 2021-04-25 01:28:55 | <shachaf> | You can make join and duplicate out of those. |
| 2021-04-25 01:29:21 | <shachaf> | In particular, join out of eps, and duplicate out of eta. Just by fmapping. |
| 2021-04-25 01:29:50 | <zebrag> | okay |
| 2021-04-25 01:31:57 | × | CrazyPython quits (~crazypyth@98.122.164.118) (Ping timeout: 260 seconds) |
| 2021-04-25 01:32:36 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 2021-04-25 01:33:06 | <shachaf> | Ah, now I see the original question. |
| 2021-04-25 01:33:16 | → | stree joins (~stree@68.36.8.116) |
| 2021-04-25 01:33:18 | <shachaf> | I think you're right, and you just had the wrong duplicate. |
| 2021-04-25 01:33:28 | <zebrag> | I think my problem was I thought `duplicate [1,2,3]` was `[[1,2,3]]`, when it seems it really is `[[1],[2],[3]]`, and consequently everything was failing |
| 2021-04-25 01:33:56 | <shachaf> | Yes, that's right. |
| 2021-04-25 01:34:58 | <shachaf> | This notation makes a lot of things almost implicit. But when you have something like "Fη" you need to remember that the F is an fmap. |
| 2021-04-25 01:35:34 | <shachaf> | Whereas when you have "ηU" the U is not an fmap, and is completely implicit in Haskell. |
| 2021-04-25 01:37:43 | <zebrag> | One is lifted the other isn't. |
| 2021-04-25 01:38:06 | <zebrag> | definition of duplicate in terms of fmap pure? |
| 2021-04-25 01:38:25 | <shachaf> | duplicate = fmap pure |
| 2021-04-25 01:38:31 | <zebrag> | hehe |
| 2021-04-25 01:39:17 | <shachaf> | If the goal is to get a better feel for adjunctions, it might be better to take one where the right adjoint isn't quite so forgetful. |
| 2021-04-25 01:39:59 | <zebrag> | yes, but no |
| 2021-04-25 01:40:40 | <zebrag> | as comonad goes, this might not be the best one |
| 2021-04-25 01:40:58 | <zebrag> | anyway, thanks a lot |
| 2021-04-25 01:41:33 | <shachaf> | The classic one, in Haskell, is (e,) -| (e->), of course. |
| 2021-04-25 01:41:37 | × | honigkuchen quits (~honigkuch@ip5b429953.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2021-04-25 01:41:45 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-04-25 01:41:54 | <shachaf> | You get a good monad and a good comonad and everything is explicit. |
| 2021-04-25 01:42:08 | <edwardk> | another fun haskell one is (_ -> r) -| (_ -> r) -- which is frustrating until suddenly it is not. |
| 2021-04-25 01:42:23 | ski | . o O ( ⌜ε F ∘ F η = id⌝ and ⌜id = U ε ∘ η U⌝ ) |
| 2021-04-25 01:42:50 | <zebrag> | I'll sure look into it |
| 2021-04-25 01:43:30 | <shachaf> | Yes, of course what ski said is the real deal law. |
| 2021-04-25 01:44:04 | <ski> | looking into adjunctions for products and coproducts (or limits and colimits, in general) might also be useful |
| 2021-04-25 01:44:19 | <zebrag> | I really was reading the Paolo Perrone tutorial on categories, and the free monoid comonad was nagging me |
| 2021-04-25 01:44:57 | <shachaf> | Yes, the example ski mentioned is also good. |
| 2021-04-25 01:44:58 | <ski> | (of course, i don't write those laws quite like that, in private notes) |
| 2021-04-25 01:45:55 | <shachaf> | You have the "diagonal" functor Δ : C -> CxC. It has a left and a right adjoint. Can you figure out what they are? |
| 2021-04-25 01:45:56 | ski | was idly considering the "reverse" adjunction isomorphism, for products, the other day |
| 2021-04-25 01:46:11 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 240 seconds) |
| 2021-04-25 01:46:17 | <shachaf> | ski: How do you write them in private notes? |
| 2021-04-25 01:46:22 | <zebrag> | Elementary examples of adjoint functor theorem were really enlightening. |
| 2021-04-25 01:47:04 | × | xff0x quits (~xff0x@2001:1a81:5345:1000:6c4e:76aa:9183:d81d) (Ping timeout: 245 seconds) |
| 2021-04-25 01:47:53 | <ski> | (if a product is the "greatest" object "before" two given objects .. then the diagonal of an object is the "least" pair of objects "after" the given objects) |
| 2021-04-25 01:49:02 | → | xff0x joins (~xff0x@2001:1a81:5378:d500:70a3:57b2:577c:e365) |
| 2021-04-25 01:50:14 | <zebrag> | before/after? |
| 2021-04-25 01:50:28 | <zebrag> | oh yes |
| 2021-04-25 01:50:39 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-04-25 01:50:44 | <zebrag> | nice |
| 2021-04-25 01:51:03 | <ski> | (er, s/the given objects/the given object/) |
| 2021-04-25 01:51:11 | × | shailangsa quits (~shailangs@host86-185-58-137.range86-185.btcentralplus.com) (Ping timeout: 240 seconds) |
| 2021-04-25 01:51:37 | <zebrag> | this sort of vernacular is very useful |
| 2021-04-25 01:52:38 | <zebrag> | and you really can say it to yourself, when the formula above can't easily be pronounced |
| 2021-04-25 01:53:35 | <ski> | reading out "adjunctiony formulae" out aloud, in terms of "greatest", and "least", is great :) |
| 2021-04-25 01:54:37 | <zebrag> | If you have a list of such "out aloud" sentences, feel free to post the link ;) |
| 2021-04-25 01:55:12 | <zebrag> | It is so helpful to be able to really say things |
| 2021-04-25 01:56:27 | <ski> | consider e.g. expressing the order ⌜n⌝ of an element ⌜g⌝, in a group : |
| 2021-04-25 01:56:34 | <ski> | ℴ g ∣ n |
| 2021-04-25 01:56:38 | <ski> | ⇔ gⁿ = 1 |
| 2021-04-25 01:56:59 | × | hypercube quits (~hypercube@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Ping timeout: 250 seconds) |
| 2021-04-25 01:58:04 | <ski> | the order ⌜ℴ g⌝ of an element ⌜g⌝ in a group is the least (in the divisibility ordering) integer ⌜n⌝, such that the ⌜n⌝-fold product of ⌜g⌝ (⌜g⌝ raised to the power of ⌜n⌝) is the neutral element |
| 2021-04-25 01:59:07 | <ski> | (that is how i read such a statement. and i'm on the lookout for such "adjunctiony" ways of phrasing characterizations) |
| 2021-04-25 01:59:08 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-79-166.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-04-25 01:59:26 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-79-166.w86-212.abo.wanadoo.fr) |
| 2021-04-25 01:59:43 | <zebrag> | I must call it a day: I'll read the logs |
| 2021-04-25 01:59:47 | <jollygood2> | is ghc with improved records out yet? |
| 2021-04-25 02:00:07 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-79-166.w86-212.abo.wanadoo.fr) (Client Quit) |
| 2021-04-25 02:00:37 | × | Neuromancer quits (~Neuromanc@unaffiliated/neuromancer) (Ping timeout: 260 seconds) |
| 2021-04-25 02:01:05 | <ski> | note that the set of all ⌜n⌝s such that ⌜ℴ g ∣ n⌝ is an upper set (it's closed under adding multiples of elements already in the set). therefore, for there to be an equivalence here (for all ⌜n⌝), ⌜gⁿ = 1⌝ must also be increasing / order-preserving / monotone / upper, in ⌜n⌝ .. and indeed it is |
| 2021-04-25 02:02:37 | <ski> | and because it is (but isn't, if we consider the usual additive ordering ⌜≤⌝ for ⌜n⌝), that is evidence that the divisibility ordering here is the correct ordering to consider |
| 2021-04-25 02:03:05 | → | rajivr joins (uid269651@gateway/web/irccloud.com/x-tixhxbhwulglbevd) |
| 2021-04-25 02:04:32 | × | kilolympus quits (~kilolympu@5.151.5.180) (Ping timeout: 268 seconds) |
| 2021-04-25 02:05:04 | × | usr25_tm quits (~usr25@unaffiliated/usr25) (Quit: Leaving) |
| 2021-04-25 02:05:46 | <ski> | you may contrast this with the situation for nilpotency index/degree ⌜n⌝ of an element ⌜a⌝ in a ring. in this case, if ⌜aⁿ = 0⌝ holds for some ⌜n⌝, then it also holds for all additively / arithmetically greater, ⌜≤⌝, (as opposed to multiplicatively / geometrically, iow considering the divisibility ordering ⌜∣⌝) ⌜n⌝ |
| 2021-04-25 02:06:34 | <ski> | (it doesn't hold for the multiplicative ordering, specifically for ⌜n = 0⌝, unless we're in the trivial ring, with ⌜1 = 0⌝) |
| 2021-04-25 02:07:12 | × | Guest6509 quits (~laudiacay@67.176.215.84) (Ping timeout: 240 seconds) |
| 2021-04-25 02:08:11 | <ski> | (is there a standard notation for nilpotency index/degree ? .. i'll write ⌜𝓃 a⌝, i guess) |
| 2021-04-25 02:08:23 | <ski> | 𝓃 a ≤ n |
| 2021-04-25 02:08:32 | <ski> | ⇔ aⁿ = 0 |
| 2021-04-25 02:08:41 | <ski> | is thus the correct statement, here |
| 2021-04-25 02:13:17 | <ski> | (one could wonder if one could turn the equality into an inequality, with the goal of making these proper adjunctions, rather than just "adjunctiony", by which i mean a statement of the general form ⌜∀ x. c ≤ x ⇔ P x⌝ expressing that ⌜c⌝ is the least ⌜x⌝ satisfying ⌜P x⌝, for some preorder ⌜≤⌝, and inhabited upper ⌜P⌝. compare with ⌜∀ x. c = x ⇔ P x⌝ expressing that |
All times are in UTC.