Logs on 2022-10-28 (liberachat/#haskell)
| 00:00:40 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 00:01:58 | → | nilradical joins (~nilradica@user/naso) |
| 00:02:41 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 00:02:50 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 00:03:02 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 00:03:07 | → | ubert1 joins (~Thunderbi@178.165.186.249.wireless.dyn.drei.com) |
| 00:03:27 | × | ubert quits (~Thunderbi@178.165.169.91.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 00:03:27 | ubert1 | is now known as ubert |
| 00:03:54 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 00:05:16 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 00:05:39 | → | gurkenglas joins (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
| 00:06:25 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 00:06:38 | × | polo quits (~polo@user/polo) (Ping timeout: 276 seconds) |
| 00:06:44 | <EvanR> | one of the monad laws is μ∘Tμ = μ∘μT where wikipedia says the thing to the right is horizontal composition of natural transformations. But T is a functor. So does it mean upgrade T to a natural transformation in the dumbest most obvious way first? |
| 00:07:03 | × | ft quits (~ft@p3e9bc845.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 00:08:09 | → | ft joins (~ft@p508dbd59.dip0.t-ipconnect.de) |
| 00:11:31 | → | polo joins (~polo@user/polo) |
| 00:11:54 | → | redmp joins (~redmp@mobile-166-170-43-64.mycingular.net) |
| 00:12:03 | <monochrom> | No. Instead, μT is shorthand for μ :: T a -> T (T a). It is a natural transformation from T to Compose T T. |
| 00:12:54 | <monochrom> | Wait, is μ retunr? is μ join? |
| 00:12:58 | <EvanR> | join |
| 00:13:10 | <monochrom> | Ah OK, I need a correction then. |
| 00:13:20 | <geekosaur> | looked more like a comonad to me… |
| 00:14:08 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
| 00:14:15 | <monochrom> | μT is shorthand for μ :: T (T (T a)) -> T (T a). It is a natural transformation from TTT to TT. |
| 00:14:28 | <EvanR> | (either way I'm annoyed that the article is trying to pass this off as something else) |
| 00:14:31 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
| 00:14:41 | <dolio> | But which one? |
| 00:14:58 | <dolio> | The answer is, the one that isn't Tμ. |
| 00:15:20 | <monochrom> | heh yeah |
| 00:16:17 | <monochrom> | In Haskell you would write "join . fmap join = join . join", but this could be annoying in not explicating which join acts on which type, in particular how many T's. |
| 00:17:12 | <monochrom> | The mathematicians' favourite notation can be derived this way. |
| 00:17:14 | <EvanR> | nice use of overloading of μ there |
| 00:17:21 | <EvanR> | I am quite confused |
| 00:18:11 | <monochrom> | First we agree that mathematicians have a notation equivalent to Haskell's type application. The two are not very different, so I'll write in the Haskell notation. |
| 00:18:46 | <monochrom> | Given for example reverse :: [a] -> [a], we can write "reverse @ Int" for the [Int]->[Int] version. |
| 00:19:42 | <EvanR> | is horizontal composition going to be in at any point xD |
| 00:20:02 | <EvanR> | or is that a red herring |
| 00:20:39 | → | slack4673 joins (~slack1256@191.125.99.208) |
| 00:22:25 | <jackdk> | Lens question: I have `list :: [A]`, `p :: Prism' A B` and `f :: B -> m C` for some monad `m`. I want to construct an `m [C]` that is built up by applying `f` to every `B` in `list` that can be found with `p`. The best I have is to `traverse f $ list ^.. folded . p`, but is there something better that I'm missing? |
| 00:22:31 | <EvanR> | ok natural transformations produce morphisms for each type, so I think I see where you're doing with that |
| 00:22:49 | <monochrom> | With this, the monad law can be written μ . (T . μ) = μ . (μ @ T a), to just explicate the type instantiation of one of the μ's. |
| 00:23:15 | <EvanR> | you just composed a functor with a natural transformation... |
| 00:23:31 | × | slack1256 quits (~slack1256@186.11.17.82) (Ping timeout: 272 seconds) |
| 00:24:03 | <monochrom> | Actually μ . T . (μ @ a) = μ . (μ @ T a) so both sides end with some kind of @ to make my next sentence go nicer. |
| 00:24:25 | <dolio> | Category theorists use the functor's name for its map operation. |
| 00:24:46 | <geekosaur> | remember the Haskell version was `fmap ...` |
| 00:24:48 | <EvanR> | yeah I get that, but functors map morphisms not N.T.s |
| 00:24:53 | <monochrom> | Then we "eta-reduce" away the "a" on both sides. At this points mathematicians also notice that they can conflate "." with "@" with no loss of ambiguity. |
| 00:25:07 | <dolio> | Also, I think μT is equivalent to horizontal composition with the identity transformation from T to T. |
| 00:25:16 | <geekosaur> | "loss of ambiguity"? |
| 00:25:24 | <EvanR> | hence the "dumbest most obvious way" |
| 00:25:53 | <monochrom> | With "." and "@" unified, they replace both by juxtaposition, thus μ . Tμ = μ . μT |
| 00:26:01 | <EvanR> | oh, monochrom is using haskell, right |
| 00:26:05 | <monochrom> | Err loss of unambiguity! Heh. |
| 00:26:25 | <monochrom> | I was starting with Haskell then showed the transition to math notation. |
| 00:26:56 | <monochrom> | Lastly, horizontal composition of natural transformation is just Haskell composition of polymorphic functions. |
| 00:27:25 | <monochrom> | If you have "reverse . reverse" it's a horizontal composition of natural transformations. |
| 00:27:35 | <dolio> | No, that one's vertical. |
| 00:28:20 | <monochrom> | OK I had a typo. That ruined everything didn't it? |
| 00:28:24 | <dolio> | Horizontal is where you compose α with fmap β, and it doesn't matter which order. |
| 00:28:38 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 00:28:50 | <monochrom> | μ . (T μ) = μ . (μ @ T a) is the right starting point. |
| 00:30:10 | <monochrom> | It is also μ . (T (μ @ a)) = μ . (μ @ T a) |
| 00:30:47 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 00:31:09 | <EvanR> | the thing is, μ is something already, and it's not polymorphic, so what are you doing |
| 00:31:49 | × | hueso quits (~root@user/hueso) (Quit: No Ping reply in 180 seconds.) |
| 00:31:59 | <EvanR> | when reading the "math version" what does your polymorphism correspond to |
| 00:32:29 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 00:32:38 | <monochrom> | I don't understand those questions and I don't know how to answer them. |
| 00:32:42 | <EvanR> | μ : T² -> T |
| 00:32:49 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 00:33:06 | <EvanR> | T : C -> C |
| 00:33:09 | → | hueso joins (~root@user/hueso) |
| 00:33:28 | Batzy_ | is now known as Batzy |
| 00:33:28 | <EvanR> | so wtf is μT and Tμ xD |
| 00:33:59 | <dolio> | Natural transformations are families of arrows that commute with arrows. |
| 00:34:01 | <geekosaur> | are you missing that Haskell's Monad is specialized to Hask (to the extent that it's a category) but CT monads aren't? |
| 00:34:12 | × | mmhat quits (~mmh@p200300f1c730768bee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.7.1) |
| 00:34:15 | <EvanR> | (dolio says it's horizontal composition after upgrading T to a N.T., which is what I guessed originally) |
| 00:34:20 | <monochrom> | Tμ is fmap μ. μT is μ @ T a then eta away the "a". |
| 00:34:21 | <dolio> | Polymorphic definitions are families of arrows that commute with relations. |
| 00:35:26 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 00:35:26 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 00:35:26 | → | wroathe joins (~wroathe@user/wroathe) |
| 00:35:41 | × | mtjm quits (~mutantmel@2604:a880:2:d0::208b:d001) (Remote host closed the connection) |
| 00:36:11 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 244 seconds) |
| 00:36:27 | <EvanR> | geekosaur, no but now I'm wondering what difference that makes, which I'll have to come back to |
| 00:36:54 | → | mtjm joins (~mutantmel@2604:a880:2:d0::208b:d001) |
| 00:37:01 | <geekosaur> | I'm probably confused, but in CT terms the Haskell one isn't polymorphic |
| 00:37:05 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 00:37:13 | <geekosaur> | I think |
| 00:37:30 | <monochrom> | Sure. But if you s/polymorphic/natural tranformation/ then you get the CT one. |
| 00:37:36 | <geekosaur> | that said, when you wrote "μ : T² -> T", that looks to me polymorphic in T |
| 00:37:37 | × | caryhartline quits (~caryhartl@107.140.218.181) (Quit: caryhartline) |
| 00:38:12 | <geekosaur> | unless the uppercase means a specific type/NT? |
| 00:38:32 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 00:38:55 | <EvanR> | T is a constant xD |
| 00:38:56 | <monochrom> | No. Instead, where Haskell writes "foo :: F a -> G a", CT writes "foo :: F => G". Then you find yourself going out of your way to write pointfree at the type level. |
| 00:39:12 | <EvanR> | (functor) |
| 00:39:13 | <monochrom> | T is the functor being declared as a monad. |
| 00:39:41 | <geekosaur> | oh, but we're talking about join so the inner Functor must be the same as the outer? |
| 00:40:40 | <EvanR> | monads are endofunctors so were only dealing in 1 category at a time |
| 00:40:41 | <monochrom> | With join you have "T (T a) -> T a" but remember you have to write it pointfree i.e. without "a" so now you have to invent some kind of T². |
| 00:41:15 | <EvanR> | yeah T . T |
| 00:43:25 | → | jargon joins (~jargon@184.101.208.112) |
| 00:44:14 | <EvanR> | you're saying Tμ is fmap join, while T is defined to map morphisms in C, rather than natural transformations or the associated map that takes objects... |
| 00:45:03 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 00:45:06 | <monochrom> | "T" is fmap, more precisely fmap@T, when used in the context of "T <morphism here>" |
| 00:45:33 | <EvanR> | I get that fmap is involved, I'll do some more noodling with the definition of horizontal composition, and hopefully jackdk gets their lens question answered |
| 00:45:41 | <monochrom> | Yes, whereas Haskell writes "fmap @ Maybe", math writes "Maybe". |
| 00:47:49 | <monochrom> | μ is a natural transformation therefore is instantiatable to a morphism, in particular in this context μ@a. |
| 00:47:49 | <EvanR> | maybe the missing link here is how you're going from μ the N.T. to a morphism join in the category |
| 00:48:04 | <EvanR> | ooooh |
| 00:48:13 | <EvanR> | that's the instantiation step |
| 00:48:31 | → | Midjak joins (~Midjak@82.66.147.146) |
| 00:48:50 | <monochrom> | The whole equation begins as (μ @ a) . (T (μ @ a)) = (μ @ a) . (μ @ T a) |
| 00:49:22 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Ping timeout: 250 seconds) |
| 00:50:07 | × | gurkenglas quits (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 00:51:04 | <EvanR> | so Tμ involves fmap and μT doesn't |
| 00:51:05 | <monochrom> | I have given a not-so-good explanation of how to get to the usual math notation. Many CT books have good explanations. |
| 00:51:53 | <EvanR> | in any case this text "here Tμ and μT are formed by 'horizontal composition'" didn't immediately explain it |
| 00:51:56 | <monochrom> | Emily Riehl's has one. I think Fokkingga's "gentle introduction to category theory" has one too. |
| 00:52:08 | <monochrom> | To be honest I hate this math notation though. |
| 00:52:18 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 00:52:29 | <monochrom> | Well yeah one has to learn "horizontal composition" first. |
| 00:53:00 | <EvanR> | well that's what I was doing, and on THAT page, it says it's an operation between two natural transformations and doesn't seem to explain the functor notation |
| 00:54:07 | <EvanR> | but now I gather it's like a functor preprocessor or postprocessor or something |
| 00:55:24 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:56:07 | <EvanR> | though in 1 of the 2 you didn't use fmap... |
| 00:56:38 | <monochrom> | Right. |
| 00:57:24 | <monochrom> | μT really comes from (μ @ T a) then dropping the a and the @ |
| 00:57:51 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 00:58:10 | <monochrom> | In actual math notation it's μ<sub>T a</sub> then dropping the a and promoting the T from subscript to normal text. |
| 00:58:17 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
| 00:59:38 | <monochrom> | In Haskell it's "join . join = join . fmap join" so fmap happens on one side only. |
| 00:59:45 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
| 00:59:48 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 01:00:09 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 01:00:32 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 01:01:26 | <monochrom> | You should also try to independently imagine how to write code for the type sig "T (T (T a)) -> T a", you will find two ways, and they are the two sides of the law. |
| 01:02:15 | <EvanR> | and in a monad, the two ways are equivalent? |
| 01:02:33 | <monochrom> | Yeah the monad law says we want them to do the same thing. |
| 01:02:49 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 01:04:12 | → | cytokine_storm joins (~cytokine_@user/cytokine-storm/x-1083107) |
| 01:04:42 | × | crns quits (~netcrns@user/crns) (Ping timeout: 260 seconds) |
| 01:05:44 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 01:06:05 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 01:06:09 | → | crns joins (~netcrns@p5dc33bf3.dip0.t-ipconnect.de) |
| 01:06:09 | × | crns quits (~netcrns@p5dc33bf3.dip0.t-ipconnect.de) (Changing host) |
| 01:06:09 | → | crns joins (~netcrns@user/crns) |
| 01:06:39 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 01:07:11 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 244 seconds) |
| 01:07:17 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 01:07:36 | <EvanR> | alright wikipedia calls Fμ and μF whiskering, there it is explained |
| 01:08:05 | × | codedmart quits (codedmart@2600:3c01::f03c:92ff:fefe:8511) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 01:08:20 | → | codedmart joins (codedmart@2600:3c01::f03c:92ff:fefe:8511) |
| 01:08:26 | <monochrom> | Yeah. I should have mentioned that name. I wasn't confident; I only saw it once (in Riehl's), wasn't sure it's the common name. |
| 01:08:42 | <monochrom> | (Then again I didn't read many CT books. Just maybe 3.) |
| 01:09:27 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 01:09:59 | <EvanR> | I already knew this notation and what it meant, forget it, but never heard of whiskering before |
| 01:10:04 | <EvanR> | forgot* |
| 01:10:06 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 01:10:36 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:12:33 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Quit: Lost terminal) |
| 01:13:09 | <EvanR> | why do I care, well I was trying to follow this blog post which says 1. a monoid is a special case of a category 2. a category is special case of a monad and 3. a monad is a special case of a monoid |
| 01:13:17 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 01:13:29 | <EvanR> | so I got stuck making sure I knew what a monad is before he goes off the deep end making a category a monad |
| 01:14:07 | <EvanR> | https://graphicallinearalgebra.net/2017/04/16/a-monoid-is-a-category-a-category-is-a-monad-a-monad-is-a-monoid/ |
| 01:15:37 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 01:16:43 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:18:04 | → | polo_ joins (~polo@user/polo) |
| 01:18:28 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 01:20:31 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
| 01:20:44 | × | polo quits (~polo@user/polo) (Ping timeout: 276 seconds) |
| 01:22:07 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 01:23:20 | × | polo_ quits (~polo@user/polo) (Ping timeout: 276 seconds) |
| 01:25:24 | × | cytokine_storm quits (~cytokine_@user/cytokine-storm/x-1083107) (Quit: Quit) |
| 01:26:13 | × | Natch quits (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Ping timeout: 272 seconds) |
| 01:26:56 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 01:27:18 | × | xff0x quits (~xff0x@2405:6580:b080:900:4ce0:8375:d2a4:aff0) (Ping timeout: 255 seconds) |
| 01:28:05 | → | zaquest joins (~notzaques@5.130.79.72) |
| 01:29:23 | → | Natch joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
| 01:30:26 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 244 seconds) |
| 01:32:42 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 01:33:59 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 01:39:13 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 01:39:38 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
| 01:40:50 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 01:42:49 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 01:43:26 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 01:45:57 | → | boxscape joins (~boxscape@81.191.27.107) |
| 01:46:02 | boxscape | is now known as boxscape_1 |
| 01:47:24 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 01:48:25 | × | nilradical quits (~nilradica@user/naso) () |
| 01:49:22 | × | boxscape_ quits (~boxscape@81.191.27.107) (Ping timeout: 244 seconds) |
| 01:50:04 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 01:51:25 | × | jargon quits (~jargon@184.101.208.112) (Remote host closed the connection) |
| 01:55:13 | × | hsw quits (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Ping timeout: 246 seconds) |
| 01:55:26 | × | gqplox quits (~textual@2a02:c7c:941d:fd00:4102:e413:2c06:9bc1) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 01:55:52 | → | Kaipei joins (~Kaiepi@108.175.84.104) |
| 01:56:04 | → | gqplox joins (~textual@2a02:c7c:941d:fd00:4102:e413:2c06:9bc1) |
| 01:58:09 | × | nisstyre quits (~wes@li798-187.members.linode.com) (Changing host) |
| 01:58:09 | → | nisstyre joins (~wes@user/nisstyre) |
| 02:01:12 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:07:10 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:08:51 | × | td_ quits (~td@83.135.9.51) (Ping timeout: 260 seconds) |
| 02:09:10 | → | king_gs joins (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
| 02:10:20 | → | td_ joins (~td@83.135.9.42) |
| 02:13:25 | → | hsw joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 02:16:25 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
| 02:16:39 | → | polo joins (~polo@user/polo) |
| 02:17:00 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 02:18:47 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:25:17 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 240 seconds) |
| 02:26:34 | → | nate3 joins (~nate@98.45.169.16) |
| 02:28:58 | × | polo quits (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 02:30:29 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 02:31:27 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:36:12 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 02:36:30 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 02:36:33 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 02:37:28 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 02:38:59 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 02:43:13 | × | terrorjack quits (~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat) |
| 02:44:07 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
| 02:44:32 | → | terrorjack joins (~terrorjac@2a01:4f8:1c1e:509a::1) |
| 02:45:18 | × | mzan quits (~quassel@mail.asterisell.com) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 02:46:19 | → | mzan joins (~quassel@mail.asterisell.com) |
| 02:46:47 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 02:46:50 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 02:48:58 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 246 seconds) |
| 02:49:23 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 258 seconds) |
| 02:49:33 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 02:51:23 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 02:52:26 | → | polo joins (~polo@user/polo) |
| 02:52:27 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:53:38 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 02:53:45 | <talismanick> | Is there a built-in function (context: using RIO) which is like `either` but auto-returns "mempty" on Right? |
| 02:54:25 | <talismanick> | something like `\handleErr -> either handleErr mempty` |
| 02:55:58 | <talismanick> | I wrote "flip either mempty <handle Left error case>" and now hlint won't shut up about "redundant flip" |
| 02:58:03 | × | iteratee quits (~kyle@162.218.222.107) (Ping timeout: 272 seconds) |
| 02:59:30 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 03:00:36 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 03:01:39 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 258 seconds) |
| 03:03:35 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 03:03:42 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 250 seconds) |
| 03:08:19 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 03:09:26 | × | polo quits (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:10:38 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 03:10:49 | × | king_gs quits (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Remote host closed the connection) |
| 03:11:08 | → | king_gs joins (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
| 03:11:37 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 258 seconds) |
| 03:12:09 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:12:37 | → | polo joins (~polo@user/polo) |
| 03:13:46 | × | vglfr quits (~vglfr@145.224.100.164) (Ping timeout: 244 seconds) |
| 03:16:18 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 252 seconds) |
| 03:17:36 | × | rembo10 quits (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 03:20:06 | → | cyphase joins (~cyphase@user/cyphase) |
| 03:20:10 | → | rembo10 joins (~rembo10@main.remulis.com) |
| 03:21:02 | × | nate3 quits (~nate@98.45.169.16) (Ping timeout: 250 seconds) |
| 03:23:09 | × | polo quits (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:23:24 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 03:23:24 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 03:23:24 | → | wroathe joins (~wroathe@user/wroathe) |
| 03:24:11 | × | AlexNoo quits (~AlexNoo@178.34.162.124) (Read error: Connection reset by peer) |
| 03:24:12 | → | polo joins (~polo@user/polo) |
| 03:24:34 | → | AlexNoo joins (~AlexNoo@178.34.162.124) |
| 03:28:50 | × | polo quits (~polo@user/polo) (Client Quit) |
| 03:29:24 | → | polo joins (~polo@user/polo) |
| 03:33:26 | × | slack4673 quits (~slack1256@191.125.99.208) (Read error: Connection reset by peer) |
| 03:34:38 | × | king_gs quits (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 252 seconds) |
| 03:36:30 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 03:38:30 | × | boxscape_1 quits (~boxscape@81.191.27.107) (Remote host closed the connection) |
| 03:44:37 | × | Vajb quits (~Vajb@2001:999:504:1841:9e47:1ec7:a52e:1d57) (Read error: Connection reset by peer) |
| 03:44:49 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) |
| 03:47:18 | → | causal joins (~user@50.35.83.177) |
| 03:49:36 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 03:53:57 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 240 seconds) |
| 03:54:33 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 258 seconds) |
| 03:57:39 | × | polo quits (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 04:00:25 | → | polo joins (~polo@user/polo) |
| 04:03:13 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 04:11:52 | × | polo quits (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 04:12:15 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 04:14:42 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 255 seconds) |
| 04:17:47 | × | arahael quits (~arahael@14-202-55-135.tpgi.com.au) (Ping timeout: 260 seconds) |
| 04:18:16 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Quit: ZNC - https://znc.in) |
| 04:20:29 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 04:22:07 | → | mbuf joins (~Shakthi@49.204.132.19) |
| 04:22:42 | → | k8yun joins (~k8yun@user/k8yun) |
| 04:25:55 | × | gqplox quits (~textual@2a02:c7c:941d:fd00:4102:e413:2c06:9bc1) (Quit: Textual IRC Client: www.textualapp.com) |
| 04:30:48 | → | troydm joins (~troydm@host-176-37-124-197.b025.la.net.ua) |
| 04:31:01 | → | arahael joins (~arahael@14-200-56-241.tpgi.com.au) |
| 04:31:09 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 04:31:23 | → | Vajb joins (~Vajb@85-76-71-213-nat.elisa-mobile.fi) |
| 04:33:18 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 04:33:58 | × | k8yun quits (~k8yun@user/k8yun) (Quit: Leaving) |
| 04:35:39 | → | jonathanx joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
| 04:37:16 | → | jonathanx_ joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
| 04:39:43 | → | bgs joins (~bgs@212-85-160-171.dynamic.telemach.net) |
| 04:40:20 | × | jonathanx quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 250 seconds) |
| 04:40:26 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 04:44:37 | × | king_gs quits (~Thunderbi@187.201.83.115) (Ping timeout: 240 seconds) |
| 04:45:55 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
| 04:56:33 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:59:50 | × | raym quits (~ray@user/raym) (Ping timeout: 250 seconds) |
| 05:01:21 | → | tjakway joins (~tjakway@184.170.241.65) |
| 05:07:53 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 272 seconds) |
| 05:11:56 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 05:13:10 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 05:14:00 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 05:14:00 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 05:14:00 | → | wroathe joins (~wroathe@user/wroathe) |
| 05:15:55 | × | tjakway quits (~tjakway@184.170.241.65) (Quit: WeeChat 3.5) |
| 05:17:43 | × | king_gs quits (~Thunderbi@187.201.83.115) (Ping timeout: 255 seconds) |
| 05:18:45 | → | tjakway joins (~tjakway@cpe-107-184-74-161.socal.res.rr.com) |
| 05:27:41 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 05:28:29 | → | jtomas joins (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) |
| 05:28:45 | → | polo joins (~polo@user/polo) |
| 05:29:54 | × | polo quits (~polo@user/polo) (Client Quit) |
| 05:36:11 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 276 seconds) |
| 05:36:46 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 05:40:40 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 05:42:02 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 05:43:16 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
| 05:44:22 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 05:46:31 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 272 seconds) |
| 05:47:01 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 05:54:23 | × | nshepperd quits (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) (Quit: quit) |
| 05:54:31 | → | nshepperd joins (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) |
| 05:56:55 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
| 05:57:34 | → | nate3 joins (~nate@98.45.169.16) |
| 05:58:30 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 06:00:57 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:01:19 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Client Quit) |
| 06:02:22 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 06:02:40 | × | nate3 quits (~nate@98.45.169.16) (Ping timeout: 250 seconds) |
| 06:21:43 | × | hsw quits (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
| 06:21:49 | → | hsw_ joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 06:27:06 | → | mixfix41 joins (~sdenynine@user/mixfix41) |
| 06:27:48 | × | detuneattune quits (~detuneatt@user/detuneattune) (Quit: The Lounge - https://thelounge.chat) |
| 06:28:04 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 246 seconds) |
| 06:28:50 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:29:07 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 06:32:08 | × | mixfix41 quits (~sdenynine@user/mixfix41) (Ping timeout: 250 seconds) |
| 06:33:03 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 06:33:26 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
| 06:35:13 | × | king_gs quits (~Thunderbi@187.201.83.115) (Read error: Connection reset by peer) |
| 06:35:33 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 06:35:45 | → | king_gs joins (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
| 06:37:46 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 250 seconds) |
| 06:41:25 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 06:42:06 | → | detuneattune joins (~detuneatt@user/detuneattune) |
| 06:43:08 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 06:43:10 | × | hsw_ quits (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
| 06:43:19 | → | hsw_ joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 06:45:37 | → | mixfix41 joins (~sdenynine@user/mixfix41) |
| 06:48:01 | → | raym joins (~ray@user/raym) |
| 06:52:14 | × | king_gs quits (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 276 seconds) |
| 06:52:27 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 06:52:59 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 06:55:57 | × | echoreply quits (~echoreply@45.32.163.16) (Quit: WeeChat 2.8) |
| 06:57:14 | → | echoreply joins (~echoreply@45.32.163.16) |
| 06:57:16 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
| 07:01:48 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:e14a:54e1:f555:fbc8) |
| 07:04:55 | → | michalz joins (~michalz@185.246.207.200) |
| 07:06:14 | → | danza joins (~francesco@151.82.113.246) |
| 07:06:48 | → | gmg joins (~user@user/gehmehgeh) |
| 07:12:11 | × | jtomas quits (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) (Ping timeout: 260 seconds) |
| 07:13:07 | → | acidjnk_new joins (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
| 07:13:07 | → | acidjnk joins (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
| 07:15:34 | × | m5zs7k quits (aquares@web10.mydevil.net) (Ping timeout: 244 seconds) |
| 07:16:32 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:16:38 | → | m5zs7k joins (aquares@web10.mydevil.net) |
| 07:17:22 | → | CiaoSen joins (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 07:18:43 | → | mncheck joins (~mncheck@193.224.205.254) |
| 07:20:15 | × | king_gs quits (~Thunderbi@187.201.83.115) (Ping timeout: 272 seconds) |
| 07:22:37 | × | mixfix41 quits (~sdenynine@user/mixfix41) (Remote host closed the connection) |
| 07:25:48 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:25:59 | × | ft quits (~ft@p508dbd59.dip0.t-ipconnect.de) (Quit: leaving) |
| 07:26:14 | × | tjakway quits (~tjakway@cpe-107-184-74-161.socal.res.rr.com) (Quit: WeeChat 3.5) |
| 07:26:41 | → | kenran joins (~user@user/kenran) |
| 07:26:49 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 07:28:37 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 07:28:58 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 07:31:06 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 07:31:08 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
| 07:31:46 | → | mixfix41 joins (~sdenynine@user/mixfix41) |
| 07:34:44 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 07:36:24 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 07:39:15 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
| 07:45:48 | × | raym quits (~ray@user/raym) (Ping timeout: 250 seconds) |
| 07:46:09 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 07:46:21 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 07:46:26 | → | infinity0_ joins (~infinity0@pwned.gg) |
| 07:46:29 | infinity0_ | is now known as infinity0 |
| 07:46:40 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 07:46:40 | → | zeenk joins (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) |
| 07:46:52 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 07:48:07 | × | mixfix41 quits (~sdenynine@user/mixfix41) (Ping timeout: 272 seconds) |
| 07:50:16 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 07:51:32 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 07:52:05 | → | fserucas|eod joins (~fserucas|@2001:818:e376:a400:fb92:70c1:dd88:c7d7) |
| 07:52:36 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 264 seconds) |
| 07:56:57 | × | redmp quits (~redmp@mobile-166-170-43-64.mycingular.net) (Ping timeout: 240 seconds) |
| 07:58:09 | → | mmhat joins (~mmh@p200300f1c730768bee086bfffe095315.dip0.t-ipconnect.de) |
| 08:02:01 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 08:05:19 | × | mbuf quits (~Shakthi@49.204.132.19) (Quit: Leaving) |
| 08:12:15 | × | danza quits (~francesco@151.82.113.246) (Read error: Connection reset by peer) |
| 08:12:28 | → | cfricke joins (~cfricke@user/cfricke) |
| 08:18:10 | → | chele joins (~chele@user/chele) |
| 08:22:40 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 08:23:35 | × | jonathanx_ quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 272 seconds) |
| 08:24:20 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 08:29:27 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 08:30:05 | → | nate3 joins (~nate@98.45.169.16) |
| 08:30:33 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 08:32:53 | → | king_gs1 joins (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
| 08:32:55 | × | king_gs quits (~Thunderbi@187.201.83.115) (Read error: Connection reset by peer) |
| 08:32:55 | king_gs1 | is now known as king_gs |
| 08:33:44 | × | shriekingnoise quits (~shrieking@186.137.167.202) (Quit: Quit) |
| 08:35:37 | × | nate3 quits (~nate@98.45.169.16) (Ping timeout: 272 seconds) |
| 08:38:02 | → | chele joins (~chele@user/chele) |
| 08:43:14 | → | erisco_ joins (~erisco@d24-141-66-165.home.cgocable.net) |
| 08:45:07 | × | erisco quits (~erisco@d24-141-66-165.home.cgocable.net) (Ping timeout: 272 seconds) |
| 08:45:07 | erisco_ | is now known as erisco |
| 08:46:02 | × | king_gs quits (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 250 seconds) |
| 08:47:43 | → | Kaipii joins (~Kaiepi@108.175.84.104) |
| 08:50:45 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 08:51:27 | × | Kaipei quits (~Kaiepi@108.175.84.104) (Ping timeout: 272 seconds) |
| 08:55:08 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Ping timeout: 250 seconds) |
| 08:57:43 | → | __monty__ joins (~toonn@user/toonn) |
| 09:08:01 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
| 09:08:32 | → | jonathanx_ joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 09:11:59 | × | acidjnk quits (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 09:13:00 | → | kenran joins (~user@user/kenran) |
| 09:13:07 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 09:17:54 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:e14a:54e1:f555:fbc8) (Quit: WeeChat 2.8) |
| 09:20:15 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 09:21:09 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
| 09:22:16 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 09:22:36 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
| 09:23:49 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 09:27:28 | Kaipii | is now known as Kaiepi |
| 09:28:43 | → | axeman joins (~quassel@212.129.76.63) |
| 09:29:27 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 09:31:27 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:33:04 | <probie> | Is there a convenient way to recurse over type-level naturals, or am I stuck defining something like `data N = Z | S N` and `type family ToNat (n :: Nat) :: N where`? |
| 09:34:50 | → | gmg joins (~user@user/gehmehgeh) |
| 09:35:12 | → | frost24 joins (~frost@user/frost) |
| 09:35:37 | <merijn> | There is a convenient way! It's called "writing your code in Idris" :D |
| 09:35:42 | <probie> | I wrote iterated fmap (i.e `fmapn @2 (*2) [[1..4::Int],[2..7]] = [[2,4,6,8],[4,6,8,10,12,14]]`), but to use `Nat` I ended up needing a type like `fmapn :: forall n x y a b . FmapN (ToN n) x y a b => (a -> b) -> x -> y` |
| 09:36:27 | <probie> | s/(*2)/(*2::Int)/ (type inference does not play nicely here) |
| 09:38:57 | <probie> | merijn: and give up my laziness? |
| 09:41:09 | → | gurkenglas joins (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
| 09:41:26 | <tomsmeding> | some of us need to be strict and get some productive work done, once in a while, otherwise nothing would happen ;) |
| 09:42:03 | <merijn> | There's a threshold past which writing type level stuff is more pain than gain, and this seems well past this threshold, unless your name is Oleg :p |
| 09:42:59 | <tomsmeding> | but unless such a way has come into existence in the last two ghc versions or so, there is no way to conveniently recurse over ghc typelevel nats |
| 09:43:01 | × | king_gs quits (~Thunderbi@187.201.83.115) (Read error: Connection reset by peer) |
| 09:43:01 | → | king_gs1 joins (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
| 09:43:21 | <tomsmeding> | but iirc there was a package that already had conversions back and forth to an actual inductive natural number type |
| 09:45:20 | king_gs1 | is now known as king_gs |
| 09:50:30 | → | raym joins (~ray@user/raym) |
| 09:50:50 | × | axeman quits (~quassel@212.129.76.63) (Ping timeout: 252 seconds) |
| 09:51:23 | → | axeman joins (~quassel@212.129.77.169) |
| 09:54:30 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 258 seconds) |
| 09:55:52 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 09:57:05 | → | eaxli joins (~eax@user/eaxli) |
| 09:58:06 | × | eaxli quits (~eax@user/eaxli) (Quit: leaving) |
| 09:58:09 | <tomsmeding> | talismanick: hlint not shutting up is easily solved by adding a .hlint.yaml file (if I remember the file name correctly) with some hints to ignore |
| 09:58:35 | <merijn> | I have this one simpel trick for shutting up hlint (Neil Mitchell hates him!) |
| 10:04:14 | <tomsmeding> | settings = { haskell = { plugin = { hlint = { globalOn = false } } } } |
| 10:08:10 | <merijn> | tomsmeding: I was thinking "rm `which hlint`", but sure :p |
| 10:08:52 | <tomsmeding> | merijn: I remember that at some point the path for that HLS setting changed, so I randomly got hlint notices again at some point |
| 10:08:53 | × | frost24 quits (~frost@user/frost) (Quit: Client closed) |
| 10:09:07 | <tomsmeding> | I was like wait what no what changed |
| 10:14:23 | × | CiaoSen quits (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 10:14:57 | × | axeman quits (~quassel@212.129.77.169) (Ping timeout: 240 seconds) |
| 10:15:02 | <Profpatsch> | newtype RevList a = RevList [a] |
| 10:15:04 | <Profpatsch> | deriving (Semigroup) via (Dual [a]) |
| 10:15:07 | <Profpatsch> | Can I make this work somehow? |
| 10:16:43 | <tomsmeding> | > :set -XDerivingVia -XDerivingStrategies |
| 10:16:45 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
| 10:16:52 | <tomsmeding> | % :set -XDerivingVia -XDerivingStrategies |
| 10:16:52 | <yahb2> | <no output> |
| 10:16:54 | <Profpatsch> | I guess I can add the Dual constructor to the RevList constructor |
| 10:16:54 | <tomsmeding> | % import Data.Monoid |
| 10:16:54 | <yahb2> | <no output> |
| 10:17:00 | <tomsmeding> | % newtype RevList a = RevList [a] deriving (Semigroup) via (Dual [a]) deriving (Show) |
| 10:17:00 | <yahb2> | <no output> |
| 10:17:05 | <tomsmeding> | % RevList [1..4] <> RevList [5..8] |
| 10:17:05 | <yahb2> | RevList [5,6,7,8,1,2,3,4] |
| 10:17:09 | <tomsmeding> | Profpatsch: seems to work |
| 10:17:18 | <Profpatsch> | tomsmeding: huuuh |
| 10:17:29 | <Profpatsch> | maybe I’m missing an extension |
| 10:17:54 | <tomsmeding> | both extensions that you need to enable are clearly indicated in the error you get |
| 10:17:56 | <tomsmeding> | so unlikely |
| 10:18:12 | <Profpatsch> | tomsmeding: one sec |
| 10:18:26 | <Profpatsch> | tomsmeding: https://zerobin.verklagmichdo.ch/paste/oQbaRRFW#pMEIil63xvsyWeAlN1n0kd2MhmNBpfvG6z1bK+Uo2OV |
| 10:18:37 | <Profpatsch> | Oh I should read the error message |
| 10:18:41 | <Profpatsch> | I have to import the Dual constructor |
| 10:18:46 | <tomsmeding> | :) |
| 10:18:47 | <tomsmeding> | yes |
| 10:18:55 | <Profpatsch> | lol |
| 10:18:57 | <Profpatsch> | sorry |
| 10:19:07 | <tomsmeding> | 'coerce' will try to not "use" stuff that you wouldn't be able to use normally |
| 10:19:24 | <Profpatsch> | prime hls potential |
| 10:19:36 | <Profpatsch> | but prob nontrivial to implement a suggestion to import Dual |
| 10:19:48 | × | td_ quits (~td@83.135.9.42) (Ping timeout: 252 seconds) |
| 10:19:49 | <Profpatsch> | I really need to get into hls dev |
| 10:20:02 | <merijn> | Sure, but do you wanna implement custom warnings for every newtype in hls? |
| 10:20:27 | <merijn> | Would be more sensible to work on the machine interface for GHC errors and have that integrated in there |
| 10:20:33 | <tomsmeding> | merijn: I guess it could recognise "The data constructor `bla' of newtype `bla' is not in scope", and suggest import |
| 10:20:37 | <tomsmeding> | yes for sure |
| 10:20:43 | <Profpatsch> | well the GHC error would have to be structured enough |
| 10:21:00 | <Profpatsch> | to turn the part that says “you might not have imported Dual” into a hls suggestion |
| 10:21:10 | <merijn> | Profpatsch: There's a running project for structured GHC errors |
| 10:21:21 | <Profpatsch> | So I guess by extension I’d have to get into GHC development lol |
| 10:21:27 | <Profpatsch> | neverending rabbit holes |
| 10:21:44 | <merijn> | tbh, GHC is pretty easy to work on if you're not touching the scary parts (type checker) |
| 10:21:54 | <Profpatsch> | every nix user is a nix developer |
| 10:21:58 | <Profpatsch> | every haskell user is a ghc developer |
| 10:22:01 | <merijn> | One of my first ever Haskell contributions was a GHC patch |
| 10:22:28 | <merijn> | The problem is that not every Haskell user is a GHC developer :p |
| 10:22:29 | <geekosaur> | I have yet to contrib a patch but I review RTS code |
| 10:22:58 | <Profpatsch> | the structured errors would be exposed via the GHC lib? |
| 10:23:22 | <merijn> | Actually my *two* first Haskell contributiosn where GHC and I'm kinda proud of both, despite being trivial :p |
| 10:23:48 | <Profpatsch> | https://gitlab.haskell.org/ghc/ghc/-/issues/18516 |
| 10:24:42 | → | beteigeuze joins (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) |
| 10:26:02 | <Profpatsch> | I feel like this is too abstract tho |
| 10:26:31 | <Profpatsch> | It would be better to just start with ideas for hls suggestions, and push them upstream by implementing the minimal amount of structure needed for these suggestions in GHC lib |
| 10:27:05 | <Profpatsch> | (keeping that interface unstable between GHC versions until a nice interface is reached by experimentation) |
| 10:27:55 | <tomsmeding> | I think programming against another unstable ghc interface is the absolute last thing that hls developers are looking for |
| 10:27:57 | <Profpatsch> | then hls can add more and more stuff per GHC version without having to resort to dump string parsing |
| 10:28:14 | <Profpatsch> | *dumb |
| 10:28:30 | <Profpatsch> | tomsmeding: anything is more stable than parsing string output |
| 10:28:41 | → | xff0x joins (~xff0x@2405:6580:b080:900:2e5f:ef77:7c98:ca52) |
| 10:29:19 | <Profpatsch> | well, string is the universal interface :P |
| 10:29:26 | → | td_ joins (~td@83.135.9.42) |
| 10:29:37 | <Profpatsch> | as per the unix philosophy |
| 10:29:40 | <merijn> | Profpatsch: hls is already ginormous |
| 10:29:48 | <Profpatsch> | merijn: why? |
| 10:29:53 | <merijn> | Profpatsch: Making it bigger with tons of custom code is undesirable |
| 10:30:44 | → | axeman joins (~quassel@212.129.78.247) |
| 10:31:04 | <Profpatsch> | merijn: by that metric we should just outright delete 3 quarters of the Cabal codebase :) |
| 10:31:54 | <Profpatsch> | which reminds me, I still have to finish the hoogle patches I submitted |
| 10:32:20 | <merijn> | Except deleting that cabal could would break working things, I'm saying we shouldn't *add more* if possible |
| 10:32:41 | <Profpatsch> | merijn: is anybody using backpack? :) |
| 10:32:54 | × | mmhat quits (~mmh@p200300f1c730768bee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.7.1) |
| 10:33:01 | <tomsmeding> | kmett is, I think |
| 10:33:12 | <Franciman> | i am |
| 10:33:14 | <Franciman> | in ocaml |
| 10:33:16 | <Franciman> | way better |
| 10:33:18 | <Profpatsch> | lol |
| 10:33:22 | <Profpatsch> | touche |
| 10:33:25 | <merijn> | backpack is kinda dead due to ezyang getting hired away from Haskell into writing pytorch stuff |
| 10:33:26 | <Profpatsch> | éééé |
| 10:33:38 | <merijn> | As he was the driving force behind its implementation |
| 10:33:44 | × | perrierjouet quits (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) (Ping timeout: 252 seconds) |
| 10:34:14 | <Profpatsch> | Oh you can derive multiple things in the same clause super cool deriving (Semigroup, Monoid) via (Dual [a]) |
| 10:41:36 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 10:42:20 | × | acidjnk_new quits (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 10:42:46 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 10:47:46 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 10:59:44 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
| 10:59:44 | → | acidjnk_new joins (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
| 11:00:20 | × | acidjnk_new quits (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Client Quit) |
| 11:00:30 | × | axeman quits (~quassel@212.129.78.247) (Ping timeout: 252 seconds) |
| 11:05:01 | → | birdgoose joins (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) |
| 11:13:45 | × | Kaiepi quits (~Kaiepi@108.175.84.104) (Quit: Leaving) |
| 11:15:18 | → | Kaiepi joins (~Kaiepi@108.175.84.104) |
| 11:29:13 | → | shriekingnoise joins (~shrieking@186.137.167.202) |
| 11:30:16 | → | frost53 joins (~frost@user/frost) |
| 11:32:21 | → | Midjak joins (~Midjak@82.66.147.146) |
| 11:42:50 | × | birdgoose quits (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) (Ping timeout: 250 seconds) |
| 11:47:33 | → | jtomas joins (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) |
| 11:49:25 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 11:53:05 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 11:56:15 | × | frost53 quits (~frost@user/frost) (Quit: Client closed) |
| 11:57:43 | → | frost70 joins (~frost@user/frost) |
| 12:04:50 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
| 12:09:32 | → | yuzhao joins (~yuzhao@36.112.45.73) |
| 12:15:03 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Quit: Leaving) |
| 12:15:37 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 12:15:57 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 240 seconds) |
| 12:16:36 | × | yuzhao quits (~yuzhao@36.112.45.73) (Read error: Connection reset by peer) |
| 12:17:36 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 12:17:54 | <MangoIV[m]> | Does anybody here have know a good library to work with formal grammars? I mainly need cf. |
| 12:19:48 | × | cheater quits (~Username@user/cheater) (Quit: BitchX: fit to feel groovy) |
| 12:19:53 | → | chomwitt joins (~chomwitt@2a02:587:dc10:8200:1ac0:4dff:fedb:a3f1) |
| 12:20:36 | → | cheater joins (~Username@user/cheater) |
| 12:21:44 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 12:22:20 | <MangoIV[m]> | s/have// |
| 12:22:39 | <merijn> | Work in what way? |
| 12:23:44 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 12:23:47 | <MangoIV[m]> | construct them in an eDSL, do algorithms on them, generate strings from them, stuff like that. |
| 12:24:24 | → | leagueoflegends joins (~leagueofl@user/leagueoflegends) |
| 12:24:34 | → | raek joins (raek@2a01:7e01::f03c:93ff:fedf:bffe) |
| 12:24:37 | <leagueoflegends> | what is a monad and can you give a code example/ |
| 12:24:50 | → | yuzhao joins (~yuzhao@36.112.45.73) |
| 12:26:41 | <geekosaur> | http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html |
| 12:27:17 | <geekosaur> | you don't care about anything beyond that |
| 12:27:58 | × | frost70 quits (~frost@user/frost) (Ping timeout: 244 seconds) |
| 12:28:59 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
| 12:31:22 | <leagueoflegends> | wait |
| 12:31:22 | × | yuzhao quits (~yuzhao@36.112.45.73) (Ping timeout: 250 seconds) |
| 12:31:36 | → | nate3 joins (~nate@98.45.169.16) |
| 12:31:49 | <leagueoflegends> | leading up to a monad is a function that returns two separate times |
| 12:31:56 | <leagueoflegends> | or at the same time |
| 12:32:53 | <probie> | What is an iterable and can you give a code example? |
| 12:34:10 | × | king_gs quits (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 246 seconds) |
| 12:34:27 | <leagueoflegends> | in what languge |
| 12:34:29 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 12:34:29 | <leagueoflegends> | language |
| 12:35:18 | <merijn> | leagueoflegends: Trying to understand the idea behind "monad" without first learning Haskell's type system and typeclasses is kinda futile, it won't make much sense. And once you understand how the types and typeclasses work then it's mostly obvious |
| 12:36:05 | <geekosaur> | returning two things at the same time is just a tuple |
| 12:36:13 | <probie> | leagueoflegends: In doesn't matter which language. The "joke" is that it defines an interface and many things satisfy that interface. |
| 12:36:13 | <leagueoflegends> | oh |
| 12:36:28 | × | nate3 quits (~nate@98.45.169.16) (Ping timeout: 255 seconds) |
| 12:38:05 | → | nilradical joins (~nilradica@user/naso) |
| 12:39:13 | <leagueoflegends> | what's the preferred way to install haskell on windows |
| 12:39:17 | <probie> | For an example of a valid, but useless monad `data AMonad a = AMonad`, `instance Functor AMonad where fmap _ _ = AMonad` `instance Applicative AMonad where {pure _ = AMonad; (<*>) _ _ = AMonad}` `instance Monad AMonad where (>>=) _ _ = AMonad` |
| 12:39:47 | <probie> | On all platforms, if you're not using nix, via ghcup |
| 12:40:07 | <leagueoflegends> | why can't I just download an installer |
| 12:41:46 | <geekosaur> | people use installers these days? |
| 12:42:34 | <leagueoflegends> | never mind |
| 12:42:37 | <leagueoflegends> | I'll use ghcip |
| 12:42:40 | <leagueoflegends> | ghcup |
| 12:44:11 | <leagueoflegends> | what is stack? |
| 12:44:23 | → | CiaoSen joins (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 12:46:39 | <leagueoflegends> | should I install stack? |
| 12:47:00 | <probie> | A build tool. It used to very popular, but it's less popular these days after many of the good ideas it introduced landed in cabal. Unless you're learning by following a tutorial that explicitly uses it, I wouldn't worry about it |
| 12:47:09 | <probie> | s/used to very/used to be very/ |
| 12:47:12 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:16c5:7e8f:5f7a:cef6) |
| 12:47:48 | <leagueoflegends> | I said yes to the haskell language server as I want to use vscode or vim etc with haskell |
| 12:48:03 | <leagueoflegends> | unless I'm doing something very wrong |
| 12:48:39 | <probie> | Installing hls is probably a good idea |
| 12:52:34 | <leagueoflegends> | is there any reason why GHC is so big say compared to a C compiler/ |
| 12:52:42 | <leagueoflegends> | ?* |
| 12:52:42 | <lambdabot> | Maybe you meant: v @ ? . |
| 12:55:03 | <geekosaur> | it's doing a lot more than a C compiler |
| 12:55:52 | <leagueoflegends> | ghc is .5gb while gcc is like .05gb |
| 12:58:34 | <merijn> | leagueoflegends: A lot of gcc's install size is hidden inside your OS :p I have a user install of gcc in my homedir, it's 1.6 GB. Clang is well over 4-5 GB |
| 12:58:34 | <leagueoflegends> | oops I accidentally install stack |
| 12:58:43 | <leagueoflegends> | oh |
| 12:58:55 | <leagueoflegends> | installed* |
| 12:59:07 | <leagueoflegends> | will it conflict with cabal |
| 12:59:20 | <probie> | The source for gcc is larger than the source for GHC thought :p |
| 12:59:27 | <probie> | stack doesn't conflict with cabal |
| 12:59:38 | <probie> | in fact, stack still needs cabal |
| 12:59:49 | → | littlefinger joins (~littlefin@pool-100-15-237-121.washdc.fios.verizon.net) |
| 12:59:53 | <probie> | s/thought/though/ |
| 12:59:58 | → | constxd joins (~brad@47.55.121.233) |
| 13:03:02 | <merijn> | probie: stack still needs Cabal it doesn't need cabal (the executable, aka cabal-install) |
| 13:03:52 | <leagueoflegends> | do you recommend vim or neovim |
| 13:04:10 | <leagueoflegends> | and ghcup installed haskell successfully |
| 13:04:15 | <leagueoflegends> | I guess that's a start |
| 13:05:10 | <probie> | merijn: does ghcup install them separately? I live in a nix world |
| 13:06:17 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:16c5:7e8f:5f7a:cef6) (Ping timeout: 240 seconds) |
| 13:07:38 | <geekosaur> | ghcup initially installs just ghc (9.2.4 currently) and HLS. `ghcup tui` lets you install stack and/or cabal |
| 13:07:51 | <geekosaur> | (or `ghcup install stack`/`ghcup install cabal`) |
| 13:07:57 | × | troydm quits (~troydm@host-176-37-124-197.b025.la.net.ua) (Ping timeout: 272 seconds) |
| 13:08:08 | <probie> | leagueoflegends: I think neovim with coc is gaining ground over regular vim, but I'm an emacs user and most of my coworkers use vscode, so take my opinion with a grain of salt |
| 13:08:32 | <merijn> | probie: I dunno, I don't use ghcup, because I'm a grumpy old man |
| 13:09:15 | <geekosaur> | <-- this grumpy old man uses ghcup. and even vscode for some things. but not nvim+coc |
| 13:10:25 | <MangoIV[m]> | <MangoIV[m]> "Does anybody here have know a..." <- bumping this. Ideally it would also have an efficient representation for the grammars. |
| 13:11:16 | <geekosaur> | might work better to ask on reddit or the discourse |
| 13:11:24 | <merijn> | or haskell-cafe, yeah |
| 13:11:29 | → | lortabac joins (~lortabac@37.166.20.4) |
| 13:14:30 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 13:16:00 | × | lortabac quits (~lortabac@37.166.20.4) (Ping timeout: 250 seconds) |
| 13:17:41 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:a2d7:73b4:5d4c:1129) |
| 13:20:54 | <leagueoflegends> | what is coc |
| 13:23:17 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 240 seconds) |
| 13:23:56 | <geekosaur> | language server protocol plugin for nvim |
| 13:24:15 | <geekosaur> | lets it speak to HLS and other LSP engines (for C, JS, etc.) |
| 13:24:24 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 13:26:09 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 13:26:13 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 13:27:56 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 13:32:57 | → | ft joins (~ft@p508dbd59.dip0.t-ipconnect.de) |
| 13:34:59 | × | littlefinger quits (~littlefin@pool-100-15-237-121.washdc.fios.verizon.net) (Quit: Client closed) |
| 13:36:06 | × | nilradical quits (~nilradica@user/naso) (Remote host closed the connection) |
| 13:37:05 | → | nilradical joins (~nilradica@user/naso) |
| 13:38:56 | <leagueoflegends> | what's the preferred way to install haskell in ubuntu? |
| 13:39:23 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.7.1) |
| 13:40:13 | → | vpan joins (~0@212.117.1.172) |
| 13:40:44 | → | jonathanx__ joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 13:43:31 | × | king_gs quits (~Thunderbi@187.201.83.115) (Ping timeout: 255 seconds) |
| 13:45:19 | × | jonathanx_ quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 272 seconds) |
| 13:45:26 | <geekosaur> | same way. most OS distros have very old versions of GHC |
| 13:45:57 | × | jonathanx__ quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 272 seconds) |
| 13:52:04 | <leagueoflegends> | ok, thanks |
| 13:55:02 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 13:55:02 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 13:55:02 | → | wroathe joins (~wroathe@user/wroathe) |
| 13:55:22 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 13:56:22 | × | nilradical quits (~nilradica@user/naso) (Remote host closed the connection) |
| 13:57:34 | → | Tuplanolla joins (~Tuplanoll@91-159-69-11.elisa-laajakaista.fi) |
| 13:58:59 | → | slack1256 joins (~slack1256@186.11.47.202) |
| 13:59:48 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Ping timeout: 252 seconds) |
| 14:00:39 | → | slac95907 joins (~slack1256@191.125.99.208) |
| 14:00:44 | → | nilradical joins (~nilradica@user/naso) |
| 14:02:17 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 240 seconds) |
| 14:02:51 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 260 seconds) |
| 14:03:28 | × | slack1256 quits (~slack1256@186.11.47.202) (Ping timeout: 252 seconds) |
| 14:04:15 | × | nilradical quits (~nilradica@user/naso) (Remote host closed the connection) |
| 14:04:31 | → | nilradical joins (~nilradica@user/naso) |
| 14:05:07 | × | gurkenglas quits (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 14:07:03 | × | mncheck quits (~mncheck@193.224.205.254) (Quit: Leaving) |
| 14:07:09 | → | mncheckm joins (~mncheck@193.224.205.254) |
| 14:07:22 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 14:13:06 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 14:13:37 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:15:37 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 14:16:44 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 14:18:15 | × | king_gs quits (~Thunderbi@187.201.83.115) (Ping timeout: 272 seconds) |
| 14:27:16 | → | jonathanx joins (~jonathan@94.234.119.48) |
| 14:28:39 | → | mastarija joins (~mastarija@188.252.199.190) |
| 14:30:21 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 14:30:39 | <mastarija> | If I have this function in a file `foo = id :: Ord a => a -> a`, and load it into ghci and say `:t x = foo []` I get `[] :: Ord a => [a]`. |
| 14:31:38 | <mastarija> | However, if I write `x = foo []` alongside the `foo` in that same file I get an error saying "ambiguous type variable a0 prevents constraint Ord a0 from being solved" |
| 14:31:44 | <mastarija> | If I don't add the type signature. |
| 14:32:32 | → | king_gs joins (~Thunderbi@187.201.83.115) |
| 14:34:07 | × | king_gs quits (~Thunderbi@187.201.83.115) (Client Quit) |
| 14:36:42 | <dolio> | That's the monomorphism restriction. |
| 14:37:14 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 14:38:46 | <mastarija> | Ah.. I thought that too, and have added the MonomorphismRestriction extension instead of NoMonomorphismRestriction |
| 14:38:49 | <mastarija> | x/ |
| 14:39:54 | <mastarija> | thanks dolio |
| 14:40:00 | <dolio> | No problem. |
| 14:42:15 | → | tomku joins (~tomku@user/tomku) |
| 14:44:01 | × | burakcank quits (burakcank@has.arrived.and.is.ready-to.party) (Killed (NickServ (GHOST command used by burakcank_!B438@free.znc.bg))) |
| 14:44:15 | → | burakcank joins (bnc4free@has.arrived.and.is.ready-to.party) |
| 14:44:44 | × | mastarija quits (~mastarija@188.252.199.190) (Quit: Leaving) |
| 14:46:24 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 15:04:02 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 15:04:35 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 15:04:37 | × | CiaoSen quits (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 15:05:38 | × | jonathanx quits (~jonathan@94.234.119.48) (Ping timeout: 250 seconds) |
| 15:06:14 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:a2d7:73b4:5d4c:1129) (Ping timeout: 276 seconds) |
| 15:09:02 | → | boxscape joins (~boxscape@81.191.27.107) |
| 15:09:16 | → | econo joins (uid147250@user/econo) |
| 15:10:02 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 15:12:22 | → | jonathanx joins (~jonathan@c-5eea7730-74736162.cust.telenor.se) |
| 15:13:10 | × | leagueoflegends quits (~leagueofl@user/leagueoflegends) (Remote host closed the connection) |
| 15:24:09 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 15:25:41 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 15:26:07 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 255 seconds) |
| 15:28:22 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 15:31:10 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 15:32:28 | × | mrvdb quits (~mrvdb@185.92.221.186) (Quit: ZNC 1.8.2 - https://znc.in) |
| 15:34:34 | × | jonathanx quits (~jonathan@c-5eea7730-74736162.cust.telenor.se) (Remote host closed the connection) |
| 15:34:55 | → | mrvdb joins (~mrvdb@185.92.221.186) |
| 15:34:56 | → | jonathanx joins (~jonathan@94.234.119.48) |
| 15:36:36 | boxscape | is now known as boxscape_ |
| 15:40:10 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 15:46:06 | × | jonathanx quits (~jonathan@94.234.119.48) (Ping timeout: 260 seconds) |
| 15:49:58 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7137a26d59898e5c9870d6b.dip0.t-ipconnect.de) |
| 15:56:18 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 15:56:37 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 15:56:53 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 15:57:25 | × | zeenk quits (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) (Quit: Konversation terminated!) |
| 16:00:04 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 16:00:22 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 16:04:22 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 16:06:19 | <monochrom> | EvanR: I now wonder if wikiepedia had a typo. If it said instead "here T |
| 16:06:21 | <monochrom> | err |
| 16:06:53 | <monochrom> | EvanR: I now wonder if wikiepedia had a typo. If it said instead "here Tµ and µT are formed by whiskering", that would be perfect. |
| 16:08:34 | × | mrvdb quits (~mrvdb@185.92.221.186) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:08:50 | → | mrvdb joins (~mrvdb@2001:19f0:5000:8582:5400:ff:fe07:3df5) |
| 16:08:56 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 16:10:20 | → | jonathanx joins (~jonathan@c-5eea738b-74736162.cust.telenor.se) |
| 16:16:49 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 16:18:25 | → | jonathanx_ joins (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
| 16:20:37 | × | jonathanx_ quits (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Remote host closed the connection) |
| 16:20:57 | → | jonathanx_ joins (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
| 16:21:07 | × | jonathanx quits (~jonathan@c-5eea738b-74736162.cust.telenor.se) (Ping timeout: 272 seconds) |
| 16:21:54 | × | Kaiepi quits (~Kaiepi@108.175.84.104) (Ping timeout: 255 seconds) |
| 16:24:07 | × | jonathanx_ quits (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Read error: Connection reset by peer) |
| 16:25:00 | → | jonathanx_ joins (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
| 16:26:34 | × | phma quits (~phma@host-67-44-208-88.hnremote.net) (Read error: Connection reset by peer) |
| 16:27:21 | → | phma joins (~phma@2001:5b0:212a:cc58:94b0:45f6:bc48:ff7d) |
| 16:27:44 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:28:43 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 272 seconds) |
| 16:31:15 | × | fserucas|eod quits (~fserucas|@2001:818:e376:a400:fb92:70c1:dd88:c7d7) (Quit: Leaving) |
| 16:31:29 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 16:31:50 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 16:33:06 | → | nate3 joins (~nate@98.45.169.16) |
| 16:33:46 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 16:35:05 | → | titibandit joins (~titibandi@xdsl-87-78-36-34.nc.de) |
| 16:37:37 | × | nate3 quits (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
| 16:40:15 | → | jonathanx joins (~jonathan@94.234.102.75) |
| 16:40:18 | × | jonathanx_ quits (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Remote host closed the connection) |
| 16:43:45 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 16:43:45 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 16:43:45 | → | wroathe joins (~wroathe@user/wroathe) |
| 16:44:58 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 16:47:48 | → | mixfix41 joins (~sdeny9ee@user/mixfix41) |
| 16:50:32 | × | nilradical quits (~nilradica@user/naso) () |
| 16:51:23 | → | redmp joins (~redmp@eduroam-169-233-187-108.ucsc.edu) |
| 16:51:55 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 16:54:06 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:55:57 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 272 seconds) |
| 16:56:10 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 16:56:48 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 264 seconds) |
| 16:57:36 | × | vpan quits (~0@212.117.1.172) (Quit: Leaving.) |
| 16:58:09 | → | jonathanx_ joins (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
| 16:58:43 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 16:58:53 | → | Guest2776 joins (~Guest27@2001:448a:7028:49a2:c005:3fe8:2bc0:33bd) |
| 16:59:25 | × | Guest2776 quits (~Guest27@2001:448a:7028:49a2:c005:3fe8:2bc0:33bd) (Client Quit) |
| 17:00:56 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:01:57 | × | jonathanx quits (~jonathan@94.234.102.75) (Ping timeout: 240 seconds) |
| 17:02:42 | × | boxscape_ quits (~boxscape@81.191.27.107) (Remote host closed the connection) |
| 17:02:59 | → | boxscape joins (~boxscape@81.191.27.107) |
| 17:03:08 | boxscape | is now known as boxscape_ |
| 17:03:24 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 17:05:09 | × | cross quits (~cross@spitfire.i.gajendra.net) (Quit: leaving) |
| 17:07:20 | → | johnw joins (~johnw@2600:1700:cf00:db0:24dd:7cba:243c:c819) |
| 17:10:09 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 17:11:14 | <EvanR> | monochrom, ah. Feel free to change it xD |
| 17:13:57 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 17:14:06 | <EvanR> | but also by a leap of logic, whiskering is horizontal composition where one of the natural transformations is identity |
| 17:15:08 | <EvanR> | Tµ =desugar=> id_T * µ |
| 17:15:14 | → | Kaiepi joins (~Kaiepi@108.175.84.104) |
| 17:15:31 | <EvanR> | µT =desugar=> µ * id_T |
| 17:21:26 | → | slack1256 joins (~slack1256@186.11.44.138) |
| 17:23:31 | × | slac95907 quits (~slack1256@191.125.99.208) (Ping timeout: 260 seconds) |
| 17:28:06 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:29:30 | × | jtomas quits (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) (Ping timeout: 250 seconds) |
| 17:30:16 | × | beteigeuze quits (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) (Ping timeout: 252 seconds) |
| 17:31:25 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 17:31:26 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 17:31:48 | → | jtomas joins (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) |
| 17:32:38 | → | sadmax2 joins (~user@cpe-76-186-137-164.tx.res.rr.com) |
| 17:33:24 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 17:34:50 | × | sadmax2 quits (~user@cpe-76-186-137-164.tx.res.rr.com) (Remote host closed the connection) |
| 17:39:44 | → | jonathanx joins (~jonathan@c-5eea74d9-74736162.cust.telenor.se) |
| 17:40:31 | → | gurkenglas joins (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
| 17:41:29 | → | sadmax joins (~user@cpe-76-186-137-164.tx.res.rr.com) |
| 17:42:11 | × | jonathanx_ quits (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Ping timeout: 260 seconds) |
| 17:44:28 | × | titibandit quits (~titibandi@xdsl-87-78-36-34.nc.de) (Quit: Leaving.) |
| 17:46:18 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 17:51:52 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 17:52:39 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 17:54:07 | <monochrom> | EvanR: Ah, thanks. |
| 17:55:07 | → | slack3102 joins (~slack1256@191.126.99.208) |
| 17:57:18 | × | slack1256 quits (~slack1256@186.11.44.138) (Ping timeout: 255 seconds) |
| 17:58:00 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 17:58:06 | × | berberman quits (~berberman@user/berberman) (Ping timeout: 250 seconds) |
| 17:58:44 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 18:03:11 | <monochrom> | EvanR: Riehl's textbook (Category Theory in Context) section 1.7 has a brief intro to 2-catgories. It may help you decode that blog. Her homepage has the book in PDF for free: https://math.jhu.edu/~eriehl/ |
| 18:04:38 | <monochrom> | Actually https://emilyriehl.github.io/ may be a more active page, heh. |
| 18:10:19 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 18:10:54 | → | jonathanx_ joins (~jonathan@c-5eea63bf-74736162.cust.telenor.se) |
| 18:12:24 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
| 18:13:36 | × | jonathanx quits (~jonathan@c-5eea74d9-74736162.cust.telenor.se) (Ping timeout: 264 seconds) |
| 18:15:34 | → | birdgoose joins (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) |
| 18:18:17 | × | sadmax quits (~user@cpe-76-186-137-164.tx.res.rr.com) (Ping timeout: 272 seconds) |
| 18:18:47 | <EvanR> | cool |
| 18:19:29 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 18:21:14 | × | jonathanx_ quits (~jonathan@c-5eea63bf-74736162.cust.telenor.se) (Ping timeout: 276 seconds) |
| 18:24:06 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
| 18:25:24 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 250 seconds) |
| 18:26:53 | <jean-paul[m]> | `CString` is just an alias for `Ptr CChar` so any function, like `newCString` or `withCString` that gives you a `CString` might be giving you null, right? |
| 18:28:16 | <monochrom> | Actually I doubt it. |
| 18:29:09 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 18:30:37 | <jean-paul[m]> | That would be great. But do I have to read GHC source or something to know for sure? |
| 18:30:58 | <jean-paul[m]> | (if so, easier to just assume they could give me NULL, I think) |
| 18:31:13 | <monochrom> | The source code rabbit hole seems to go through a "failWhenNULL" so you get an exception or you get a non-null pointer. |
| 18:34:04 | × | birdgoose quits (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) (Ping timeout: 250 seconds) |
| 18:36:28 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7137a26d59898e5c9870d6b.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 18:37:27 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7137a26d59898e5c9870d6b.dip0.t-ipconnect.de) |
| 18:37:36 | → | birdgoose joins (~jesse@151.210.175.160) |
| 18:41:11 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 18:43:03 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 18:43:35 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 18:44:15 | × | birdgoose quits (~jesse@151.210.175.160) (Ping timeout: 272 seconds) |
| 18:45:14 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 18:48:03 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
| 18:50:24 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
| 18:51:49 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 18:55:14 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 18:56:17 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 240 seconds) |
| 19:05:48 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 19:12:49 | → | danza joins (~francesco@151.68.150.173) |
| 19:13:28 | → | troydm joins (~troydm@host-176-37-124-197.b025.la.net.ua) |
| 19:18:01 | <gurkenglas> | Let Phi be some set of functions Reals->Reals. Their pointwise infimum is at each point their greatest lower bound. This acts like an optic that can turn "all f in Phi satisfy foo(f) <= bar(f)" into "their pointwise infimum g satisfies foo(g) <= bar(f)" whenever foo and bar are monotonic. Thus it can turn "all Phi are monotonic/1-lipschitz/concave" into "their pointwise infimum is |
| 19:18:07 | <gurkenglas> | monotonic/1-lipschitz/concave". I thought I would mention that here since I was surprised to be reminded of optics. |
| 19:19:16 | <gurkenglas> | s/foo(g) <= bar(f)/foo(g) <= bar(g)/ :( |
| 19:23:18 | → | thyriaen joins (~thyriaen@2a01:aea0:dd4:470d:6245:cbff:fe9f:48b1) |
| 19:24:48 | → | gqplox joins (~textual@2a02:c7c:941d:fd00:40a0:1c9d:7a12:f334) |
| 19:25:33 | → | slack1256 joins (~slack1256@181.42.52.169) |
| 19:26:25 | → | jinsun__ joins (~jinsun@user/jinsun) |
| 19:26:25 | jinsun | is now known as Guest7738 |
| 19:26:25 | × | Guest7738 quits (~jinsun@user/jinsun) (Killed (iridium.libera.chat (Nickname regained by services))) |
| 19:26:25 | jinsun__ | is now known as jinsun |
| 19:26:37 | × | slack3102 quits (~slack1256@191.126.99.208) (Ping timeout: 240 seconds) |
| 19:28:17 | <gqplox> | Hello guys |
| 19:28:37 | <gqplox> | I have made a project in pytohn I want to convert it to haskell to learn haskell |
| 19:28:58 | <gqplox> | However, for it i need to read toml and csv files |
| 19:29:05 | <gqplox> | what is the easiest way to do it |
| 19:29:29 | <energizer> | <EvanR: so a transpose of a 0 x inf matrix> but why is the empty arglist in zip() a 0 x inf matrix instead of, say, a 0 x 0 matrix? |
| 19:29:44 | <gqplox> | Basically i want to focus on actually transforming the data for now and later on i can learn the io and monad stuff |
| 19:29:59 | <gqplox> | but for now i just want a simple way to get the data in so i can do haskell stuff on it |
| 19:30:12 | <jean-paul[m]> | gqplox: Maybe set aside the idea of "easiest" and just learn some stuff. |
| 19:30:29 | <EvanR> | jean-paul[m], withCString uses allocaArray, which uses ... ... allocaBytesAlignedAndUnchecked which newAlignedPinnedByteArray# which can't fail |
| 19:30:47 | <geekosaur> | we generally use cassava to read csv. dunno about toml |
| 19:30:48 | <EvanR> | except that it is IO so anything can fail if you try hard enough |
| 19:31:04 | <monochrom> | Perhaps choose a project that doesn't read toml. |
| 19:31:05 | <jean-paul[m]> | gqplox: You can type things like "toml" and "yaml" into the search box on https://hoogle.haskell.org/ if you want to use libraries for this. |
| 19:31:12 | <EvanR> | energizer, it isn't |
| 19:31:29 | <EvanR> | there's no way to know using only list rep |
| 19:31:56 | <energizer> | EvanR: so why would zip() be an inf x 0 matrix? |
| 19:32:02 | <EvanR> | my observations just highlight all the important missing information in a ill typed variadic zip |
| 19:32:16 | <EvanR> | energizer, repeat () would represent inf x 0 matrix |
| 19:32:53 | <EvanR> | someone else suggested that is what zip() should return |
| 19:33:12 | <EvanR> | more like, zip( a 0 x inf matrix ) should return repeat () |
| 19:33:12 | <energizer> | EvanR: but you think it's ambiguous? |
| 19:33:29 | <energizer> | EvanR: *but you think zip() is ambiguous? |
| 19:33:31 | <EvanR> | and zip ( 0 x 17 matrix ) should return 17 ()s |
| 19:33:57 | <gqplox> | yeah okay fair enough |
| 19:34:07 | <gqplox> | thx for the website btw, looks helpful |
| 19:34:33 | <EvanR> | zip() with no other information is ambiguous, such as what size you want |
| 19:34:50 | <jean-paul[m]> | monochrom, EvanR : thanks |
| 19:35:11 | <monochrom> | I did nothing :) |
| 19:35:22 | <jean-paul[m]> | gqplox: Personally I found https://www.cis.upenn.edu/~cis1940/fall16/ to be a good resource to work though. |
| 19:35:32 | <EvanR> | if your name is on the paper you're good |
| 19:35:35 | <jean-paul[m]> | Hmmm nope, that's not the right link at all (maybe it is good but I haven't done it yet) |
| 19:35:43 | <gqplox> | oh haha |
| 19:35:53 | <gqplox> | right now i am doing programming in haskell by Graham Hutton |
| 19:35:56 | <geekosaur> | @where cis194 |
| 19:35:57 | <lambdabot> | https://www.seas.upenn.edu/~cis194/spring13/lectures.html |
| 19:36:06 | <geekosaur> | is the usually recommended one hereabouts |
| 19:36:07 | <energizer> | EvanR: i am sorta persuaded that zip is fairly tho not exactly monoidal, in which case repeat () is right |
| 19:36:11 | <geekosaur> | but hutton's good too |
| 19:36:16 | <gqplox> | im not far through but im eager to build stuff now that's why i was asking |
| 19:36:19 | <jean-paul[m]> | Yes, thanks, that's the one. |
| 19:36:40 | → | mvk joins (~mvk@2607:fea8:5ce3:8500::f30b) |
| 19:36:48 | <gqplox> | i understand your point, best to just learn properly |
| 19:37:02 | <monochrom> | Dive-in projects are more haste less speed. |
| 19:37:33 | <monochrom> | (Oh it "worked" when you switched from python to javascript because the difference was too small.) |
| 19:38:23 | <gqplox> | haha :) i understand your point |
| 19:38:29 | <gqplox> | oh this website looks cool |
| 19:38:40 | <gqplox> | the seas.upenn |
| 19:38:52 | <monochrom> | "I already speak American English. I want to learn Australian English by the dive-in project of writing a review for an Australian-accent movie." This works. |
| 19:39:17 | <monochrom> | "I already speak American English. I want to learn Japanese by the dive-in project of writing a review for a Japanese movie." This breaks. |
| 19:39:28 | <c_wraith> | I learned Haskell starting with making changes to a production system. It's not impossible, but you do need to be motivated by things like "This is hard and I want to learn it all" |
| 19:39:52 | <c_wraith> | That was 14 years ago and I have not yet learned it all |
| 19:40:14 | <gqplox> | yep i understand |
| 19:40:23 | <c_wraith> | But I have learned a whole lot! |
| 19:40:47 | <gqplox> | in this case it was a very minor thing, if i can get the toml and csv files into variables i can do it |
| 19:40:55 | <gqplox> | anyway ill look at the upenn |
| 19:42:13 | <monochrom> | There is also the prospect of not porting a python code base to haskell, instead write in haskell from scratch and implement the same features. |
| 19:42:39 | <monochrom> | Indeed you wouldn't even try to translate C++ to C. |
| 19:43:49 | <gqplox> | Yep that's what I meant sorry |
| 19:43:58 | <gqplox> | and its like a 200 lines script haha |
| 19:44:03 | <gqplox> | woah the .lhs is so cool |
| 19:44:24 | <monochrom> | OK that works better. |
| 19:46:38 | <monochrom> | Alternatively, dive-in projects can work (even for arbitrarily large gaps) if you manage your expectations. (Tautology: All frustrations can be solved by managing expectations.) |
| 19:48:06 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 19:48:19 | <monochrom> | The first dive-in project alerts you to a million things you need to learn first. Learning them can take a long time. If you don't have a conflicting expectation, you will persevere. |
| 19:48:46 | <monochrom> | This initial investment amortizes. The 2nd, 3rd, ... projects will be much faster. |
| 19:50:10 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:50:34 | × | eggplantade quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 19:52:04 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:52:44 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 19:58:44 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Quit: leaving) |
| 19:59:56 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 20:02:11 | × | redmp quits (~redmp@eduroam-169-233-187-108.ucsc.edu) (Ping timeout: 260 seconds) |
| 20:02:28 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 20:07:01 | <gurkenglas> | yeah i gave up on my 2nd and 3rd project much faster than on my 1st |
| 20:07:21 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 20:10:23 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
| 20:11:10 | → | birdgoose joins (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) |
| 20:11:12 | × | hpc quits (~juzz@ip98-169-32-242.dc.dc.cox.net) (Ping timeout: 264 seconds) |
| 20:11:49 | <c_wraith> | see how much faster you reached the natural conclusion? |
| 20:12:36 | → | hpc joins (~juzz@ip98-169-32-242.dc.dc.cox.net) |
| 20:13:46 | <darkling> | If only I'd learned to give up programming 40 years ago. :) |
| 20:15:09 | <gurkenglas> | noticing that training giving up allocates my skill ranks to Giving Up put such a pin into trying :D |
| 20:16:46 | × | hpc quits (~juzz@ip98-169-32-242.dc.dc.cox.net) (Ping timeout: 250 seconds) |
| 20:23:28 | → | hpc joins (~juzz@ip98-169-32-242.dc.dc.cox.net) |
| 20:23:55 | × | kjak quits (~kjak@pool-108-31-114-135.washdc.fios.verizon.net) (Quit: leaving) |
| 20:24:19 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 20:26:57 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 20:28:25 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 246 seconds) |
| 20:30:57 | → | irrgit__ joins (~irrgit@176.113.74.74) |
| 20:31:31 | → | iteratee joins (~kyle@162.218.222.107) |
| 20:33:49 | × | irrgit_ quits (~irrgit@176.113.74.130) (Ping timeout: 244 seconds) |
| 20:34:21 | × | slack1256 quits (~slack1256@181.42.52.169) (Ping timeout: 255 seconds) |
| 20:34:35 | → | nate3 joins (~nate@98.45.169.16) |
| 20:35:36 | → | irrgit_ joins (~irrgit@176.113.74.74) |
| 20:38:02 | × | gqplox quits (~textual@2a02:c7c:941d:fd00:40a0:1c9d:7a12:f334) (Quit: Textual IRC Client: www.textualapp.com) |
| 20:38:56 | × | irrgit__ quits (~irrgit@176.113.74.74) (Ping timeout: 260 seconds) |
| 20:39:17 | × | nate3 quits (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
| 20:45:51 | × | jtomas quits (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) (Ping timeout: 272 seconds) |
| 20:46:15 | → | titibandit joins (~titibandi@xdsl-87-78-36-34.nc.de) |
| 20:47:24 | × | irrgit_ quits (~irrgit@176.113.74.74) (Read error: Connection reset by peer) |
| 20:48:29 | × | titibandit quits (~titibandi@xdsl-87-78-36-34.nc.de) (Remote host closed the connection) |
| 20:51:39 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 20:52:10 | → | polo joins (~polo@user/polo) |
| 20:52:25 | × | polo quits (~polo@user/polo) (Client Quit) |
| 20:52:31 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 20:52:44 | → | polo joins (~polo@user/polo) |
| 20:53:36 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 20:54:37 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 20:56:27 | × | nek0 quits (~nek0@2a01:4f8:222:2b41::12) (Quit: The Lounge - https://thelounge.chat) |
| 21:01:47 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 21:03:13 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 21:03:14 | → | bilegeek joins (~bilegeek@2600:1008:b027:7f32:a99b:c297:feda:8531) |
| 21:03:16 | <cpli> | are there async `Chan`s? |
| 21:03:26 | <cpli> | i.e. where one may await `readChan`? |
| 21:03:35 | <monochrom> | You can just use TChan. |
| 21:04:16 | <monochrom> | Or Chan, too. |
| 21:04:49 | <EvanR> | isn't await readChan already what readChan does |
| 21:06:07 | × | mncheckm quits (~mncheck@193.224.205.254) (Ping timeout: 272 seconds) |
| 21:10:01 | <cpli> | so if i race between readChan and anything else, it's cancel safe? |
| 21:13:43 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:15:03 | <dsal> | cpli: Not super clear what you mean. If you're waiting for a channel value in a transaction and get killed, it should be safe, but if you completed the transaction and were killed, it's not going to magically fix stuff. |
| 21:19:05 | → | beteigeuze joins (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
| 21:26:46 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 21:30:03 | ← | raek parts (raek@2a01:7e01::f03c:93ff:fedf:bffe) (WeeChat 3.0) |
| 21:35:12 | × | mvk quits (~mvk@2607:fea8:5ce3:8500::f30b) (Ping timeout: 250 seconds) |
| 21:38:53 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 21:38:58 | <EvanR> | if you're thinking of cancelling something doing a readChan then it does sound like you're at least going to need TChan |
| 21:39:29 | <EvanR> | either the entire atomically containing readTChan happens or it doesn't |
| 21:39:50 | <EvanR> | (STM) |
| 21:46:55 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 21:51:07 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
| 21:51:12 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 21:52:35 | <cpli> | perfect thank |
| 21:54:25 | → | redmp joins (~redmp@eduroam-169-233-187-108.ucsc.edu) |
| 21:56:59 | → | mvk joins (~mvk@2607:fea8:5ce3:8500::f30b) |
| 21:57:03 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 21:59:21 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 21:59:33 | × | talismanick quits (~talismani@76.133.152.122) (Remote host closed the connection) |
| 22:00:13 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 22:00:13 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 22:00:13 | → | wroathe joins (~wroathe@user/wroathe) |
| 22:03:44 | × | michalz quits (~michalz@185.246.207.200) (Remote host closed the connection) |
| 22:03:48 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
| 22:04:24 | × | fjmorazan quits (~quassel@user/fjmorazan) () |
| 22:05:08 | → | fjmorazan joins (~quassel@user/fjmorazan) |
| 22:06:25 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 246 seconds) |
| 22:06:26 | → | talismanick joins (~talismani@76.133.152.122) |
| 22:07:30 | → | axeman joins (~quassel@ip-037-201-153-145.um10.pools.vodafone-ip.de) |
| 22:08:24 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7137a26d59898e5c9870d6b.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 22:09:44 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:11:20 | → | pavonia joins (~user@user/siracusa) |
| 22:11:39 | × | polo quits (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 22:12:07 | → | polo joins (~polo@user/polo) |
| 22:13:15 | <cpli> | is there some `TChan A -> TChan A -> TChan A` which fuses two channels? |
| 22:13:28 | <cpli> | i.e. for writing purposes only |
| 22:14:16 | <cpli> | dup and clone exist, would fusing require doing so on a seperate thread? |
| 22:14:33 | → | caryhartline joins (~caryhartl@2600:1700:2d0:8d30:41f8:4e00:54f7:b844) |
| 22:15:41 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 22:15:42 | <EvanR> | what does fusing for writing purpose mean |
| 22:15:53 | <dminuoso> | Or for reading purposes. |
| 22:16:06 | <EvanR> | or append purpose |
| 22:16:10 | <dminuoso> | That is, if both channels have multiple things, in what order should they read? |
| 22:16:40 | <dminuoso> | Looking at the internals, I think you can construct an interleaving TChan without a thread |
| 22:16:54 | <DigitalKiwi> | no append only prepend |
| 22:17:08 | <EvanR> | this is haskell we can only prepend |
| 22:17:17 | <DigitalKiwi> | :D |
| 22:17:58 | <EvanR> | haskellOS |
| 22:18:09 | <EvanR> | all the files are stored backwards |
| 22:18:35 | <dminuoso> | Well anyway, an interleaving TChan could be constructed if the internals were exposed in Control.Concurrent.STM.TChan |
| 22:18:44 | <dminuoso> | But they are not, so I guess you're out of luck either way |
| 22:18:53 | <dminuoso> | I dont see a way without a separate thread doing what you want |
| 22:19:08 | <DigitalKiwi> | https://mostlyabsurd.com/files/2022-10-28-171849_964x357_scrot.png |
| 22:19:08 | × | polo quits (~polo@user/polo) (Ping timeout: 276 seconds) |
| 22:20:16 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
| 22:20:53 | <cpli> | re:dminuoso "..., in what order should they read?"; in order they were written |
| 22:21:07 | <dminuoso> | cpli: What does that even mean in STM? |
| 22:22:27 | <cpli> | i have a `[Backend]` where `data Backend = B1 B1State | B2 B2State | B3...` |
| 22:22:50 | <cpli> | each `Backend` broadcasts its event to all other backends |
| 22:23:16 | <dsal> | "order" over distinct things (e.g., two threads with two channels) is a coincidence when you observe it. |
| 22:23:22 | <cpli> | in some wrapper `data Event = E1 FromB1 | E2 FromB2` |
| 22:23:48 | <cpli> | all backends are concurrently executed |
| 22:23:59 | <dminuoso> | cpli: STM works differently |
| 22:24:07 | <dminuoso> | It's not just barriers. |
| 22:25:01 | <cpli> | is there any <10min read on how to impl async broadcasting? |
| 22:25:51 | <dsal> | The stm docs are pretty clear. You just dup a chan and write to it. |
| 22:26:05 | <monochrom> | There is no need to "merge" two TChans. Instead, to read from both TChans with "whichever one has a message first, read it", use atomically (fmap Left readTChan c1 <|> fmap Right readTChan c2) or equivalent. |
| 22:26:08 | <int-e> | DigitalKiwi: 4 centuries earlier: REPENT! REPENT! |
| 22:26:11 | <cpli> | if i write to a chan and immediately read, do i read my own message? |
| 22:26:26 | <dsal> | https://hackage.haskell.org/package/stm-2.5.1.0/docs/Control-Concurrent-STM-TChan.html#v:dupTChan |
| 22:26:45 | <dminuoso> | monochrom: Im not sure "first" really applies. |
| 22:26:49 | <DigitalKiwi> | https://twitter.com/ArchKiwi/status/1586120762544398336 |
| 22:27:05 | <monochrom> | Sure, s/first/"first" |
| 22:27:14 | <dminuoso> | monochrom: Consider the case where first `c2` has a message, the stm transaction proceeds, but gets retried. |
| 22:27:43 | <dminuoso> | Is there any guarantee c2 will be picked again, even if after retrying c1 has a message? |
| 22:28:00 | <dsal> | cpli: maybe? You've not shown enough code to say for sure. |
| 22:28:56 | × | TonyStone quits (~TonyStone@cpe-74-76-51-197.nycap.res.rr.com) (Remote host closed the connection) |
| 22:29:29 | <dsal> | dminuoso: I'm pretty sure that code won't read from c2 until c1 is empty. To make that fairer, you could put the channels in a queue of some sort and make sure each time a channel is read from it goes to the end of the list. |
| 22:29:41 | <dsal> | Doing the go thing of "randomly pick a ready channel" might be a little harder. |
| 22:29:52 | <dminuoso> | dsal: well, if c1 is empty at the time the transaction is started |
| 22:30:00 | <dminuoso> | but has data when its retried. |
| 22:30:23 | <dminuoso> | The only way I can see fairness is if you put them into a single list with a tag |
| 22:30:28 | <dminuoso> | Then you can preserve the original order. |
| 22:30:50 | <monochrom> | Oh the beauty is that every observation can be explained away by a fictional sequence, and you have no way to refute it, right? |
| 22:31:00 | <monochrom> | or fictional history. |
| 22:32:48 | → | thyriaen_ joins (~thyriaen@2a01:aea0:dd4:470d:6245:cbff:fe9f:48b1) |
| 22:32:49 | → | buffet joins (~buffet@buffet.sh) |
| 22:32:52 | <dminuoso> | cpli: So yeah I guess thats the real answer. Keep a single TChan and have all write into that, and then each backend would have a dupTChan'ed or newBroadcastTChan'ed reader. |
| 22:33:00 | <dsal> | I've never had to care about a particular ordering of channel ops, so I've not thought too much about avoiding having one get behind. One approach might be to atomically read from multiple and make a decision as to which one you want based on data inside. |
| 22:33:23 | <dminuoso> | cpli: (so the merging happens by fact of just writing into a single TChan) |
| 22:33:37 | <dsal> | Yeah, that's a lot easier. :) |
| 22:33:41 | <monochrom> | Right? "Is c2 really ready earlier?" is just philosophy. The computer science question is "if empirically you get Right, can we restrospectively make up a story that says c2 is ready earlier?" and the answer is yes. |
| 22:33:57 | → | polo joins (~polo@user/polo) |
| 22:34:42 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 22:34:52 | <dsal> | I've got into a lot of arguments with people who just want to overwrite the state with "whatever happened last" and it's really hard to explain to people how that doesn't work. |
| 22:34:59 | <dminuoso> | cpli: more to the point, set up that `TChan Event` with newBroadcastTChan (instead of newTChan) and then dupChan it for every backend. :) |
| 22:35:25 | <dminuoso> | dsal: You can just fling an IORef around! |
| 22:35:53 | <dminuoso> | And to silence any arguments, unsafeIOtoSTM all evil operations and do this in STM for maximum confusion. |
| 22:36:01 | <dsal> | A guy on my team once made a model of our system that let someone single step through every decision with business folks nodding that it was doing what they want and then get to the last bit and it all falls apart and they just assume it's a bug that needs to be fixed. |
| 22:37:01 | <dsal> | You could always have a PNRG in your STM state and change the ordering along the way. |
| 22:37:24 | → | pyrex joins (~pyrex@user/pyrex) |
| 22:39:17 | <dminuoso> | Why settle for a PRNG? |
| 22:39:31 | <dminuoso> | unsafeIOtoSTM that quantum RNG :) |
| 22:39:38 | <monochrom> | Haha |
| 22:39:48 | <cpli> | dsal: not enough code |
| 22:39:49 | <cpli> | run :: [Backend] → IO () |
| 22:39:50 | <cpli> | run bs = let |
| 22:39:50 | <cpli> | withChannel :: [(Chan Event, Backend)] |
| 22:39:50 | <cpli> | withChannel = (newChan,) <$> bs |
| 22:39:50 | <cpli> | -- what would i do here, such that |
| 22:39:50 | <cpli> | -- bn <- bm where N /= M |
| 22:39:50 | <cpli> | in mapConcurrently_ (uncurry runBackend) withChannel |
| 22:39:51 | <cpli> | runBackend :: Chan Event → Backend → IO () |
| 22:39:51 | <cpli> | runBackend ch (B1 b) = runB1 ch b |
| 22:39:52 | <cpli> | runBackend ch (B2 b) = runB2 ch b |
| 22:39:52 | <cpli> | -- ... |
| 22:40:48 | <cpli> | dminuoso: if i simply `dupChan` then every backend needs to take `N-1` reading channels from all the other backends |
| 22:41:00 | <dminuoso> | cpli: No, you seem to misunderstand. |
| 22:41:01 | <monochrom> | That may break the Copenhagen interpretation >:) |
| 22:41:04 | → | TonyStone joins (~TonyStone@cpe-74-76-51-197.nycap.res.rr.com) |
| 22:41:33 | <dminuoso> | cpli: First you start with one writer TChan, set it up with newBroadcastTChan (this is important!), this will get passed along to every backend. |
| 22:41:47 | <cpli> | understood. |
| 22:41:54 | <dminuoso> | cpli: Then, for every backend, you provide a dupTChan of that original chan, which will - for each backend - be a reader. |
| 22:42:23 | <dminuoso> | s/for each backend/for each respective backend/ |
| 22:43:04 | <dminuoso> | So if you want to broadcast, you write to that first writer tchan, and to listen to events you just read from that local reader tchan |
| 22:43:52 | <dminuoso> | so each backend has exactly one writer and one reader channel |
| 22:48:35 | <cpli> | and if i `runBackend1 :: Chan Event → Backend1 → IO () |
| 22:48:35 | <cpli> | runBackend1 ch b = race (async (readChan ch)) awaitBackendEvent |
| 22:48:49 | <cpli> | sorry for formatting |
| 22:49:07 | <cpli> | that code isn't really done |
| 22:49:23 | <cpli> | the idea is that events from the backend are then written into the channel again |
| 22:50:27 | <cpli> | more akin to: |
| 22:50:27 | <cpli> | runBackend1 :: Chan Event → Backend1 → IO () |
| 22:50:27 | <cpli> | runBackend1 ch b = forever $ race (readChan ch) |
| 22:50:27 | <cpli> | (writeChan ch =<< awaitBackendEvent) |
| 22:51:31 | <cpli> | or in your case dminuoso: |
| 22:51:33 | <cpli> | runBackend1 :: Chan Event → Chan Event → Backend1 → IO () |
| 22:51:33 | <cpli> | runBackend1 wch rch b = forever $ race (readChan rch) |
| 22:51:33 | <cpli> | (writeChan wch =<< awaitBackendEvent) |
| 22:52:04 | <dminuoso> | That looks a bit strange |
| 22:52:17 | <dminuoso> | Is the `rch` another channel? |
| 22:52:21 | <cpli> | don't `Event`s from `wch` don't simply end up back in `rch`? |
| 22:52:35 | <dminuoso> | Sure, you need to filter them out. |
| 22:52:42 | <cpli> | and `unGet` them? |
| 22:53:19 | <dminuoso> | No, you just read them again. |
| 22:53:36 | <cpli> | oh true |
| 22:53:41 | <cpli> | sure |
| 22:53:55 | <cpli> | kind of a hassle to have to |
| 22:54:17 | <cpli> | but the events are sure to arrive at the other threads nonetheless |
| 22:54:31 | <dminuoso> | Of course, that's what dupTChan is for |
| 22:54:43 | <dminuoso> | It lets you set up broadcast semantics exactly like that |
| 22:54:53 | × | polo quits (~polo@user/polo) (Ping timeout: 276 seconds) |
| 22:56:32 | <cpli> | the entire idea with "fuse" would've been to do what you meant, i.e. to `newBroadcastTChan` then `dupTChan` until you'd have a list of "RChan"s from all *other backends* and fuse those together to create a `Chan` for `bn` which would only recieve all events from `bm` where `n /= m` |
| 22:56:54 | <cpli> | but i guess just filtering out your own events is simpler |
| 22:57:12 | <dminuoso> | Yup, it doesnt need a n helper threads to set up |
| 22:57:36 | <dminuoso> | or I guess just a singular dispatcher thread |
| 22:57:38 | <cpli> | probably possible to solve in data, no? |
| 22:58:15 | <dminuoso> | I would only pursue the dispatcher model if you had more unicast semantics |
| 22:58:20 | <dminuoso> | but if everything is broadcast, this is the simpler way |
| 22:58:37 | <dminuoso> | cpli: Also, this model preserves event order properly |
| 22:58:47 | <dminuoso> | your other approach does not |
| 22:59:03 | <cpli> | *would* not, since it doesn't seem to exist |
| 22:59:14 | <dminuoso> | of course it does. |
| 22:59:24 | → | nek0 joins (~nek0@2a01:4f8:222:2b41::12) |
| 22:59:25 | <dminuoso> | its preserved in the order of which elements are read out |
| 23:00:05 | <dminuoso> | I mean yeah, ultimately you could still have write problems if there's any coordination/communication between the backends with retries going on |
| 23:00:11 | <cpli> | would an optimization be to include the read in the write case? i.e. immediately read after writing to the `Chan- i don't have guarantees about my event being next ever.. |
| 23:00:30 | <dminuoso> | What do you mean "to include the read in the write case"? |
| 23:00:46 | <dsal> | No, if you want to ignore particular messages, you have to ignore the particular messages. You can't rely on timing. |
| 23:01:34 | <dminuoso> | Oh you mean as a means to consume the element you have just written? |
| 23:02:37 | <cpli> | `bn` writes to `wch` and read from `rch`, `bm` will recieve the event, but `bn` also *will* recieve its own message, `bn` wouldn't need to read its message in its "read thread" if it could immediately could remove the message from `rch` |
| 23:02:42 | <cpli> | but there's no guarantee |
| 23:03:00 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
| 23:03:33 | <cpli> | also `rch` could be clogged up anyway, with 15 events "in queue" in which case the event pushed to `wch` wouldn't be the next in line anyways |
| 23:03:41 | <dminuoso> | cpli: https://gist.github.com/dminuoso/f42f92a27457088ce0d927175d7a21fc |
| 23:03:43 | <dminuoso> | Something along these lines |
| 23:03:55 | × | danza quits (~francesco@151.68.150.173) (Ping timeout: 272 seconds) |
| 23:04:34 | <dminuoso> | cpli: oh hold on by the way, we dont even need two separate TChans! |
| 23:04:43 | <dminuoso> | Just the dupTChan'ed channel will serve both! |
| 23:04:48 | <dminuoso> | simplifying things even further. |
| 23:05:50 | <cpli> | `atomically` such that no events may be written to the channels whilst initializing them? |
| 23:06:58 | <dminuoso> | cpli: No, its just that newBroadcastTChan must occur inside STM. |
| 23:07:00 | <dminuoso> | And dupTChan |
| 23:07:38 | <cpli> | what stops this from being non-STM, multithreading? |
| 23:08:02 | <dminuoso> | cpli: Ive updated the gist, feel free to reload |
| 23:08:35 | <dminuoso> | cpli: TChan is an STM data structure. |
| 23:08:56 | <dminuoso> | You dont have to use STM everywhere, just in the few parts where you interact with it. |
| 23:08:59 | × | redmp quits (~redmp@eduroam-169-233-187-108.ucsc.edu) (Ping timeout: 272 seconds) |
| 23:10:33 | → | j4cc3b joins (~j4cc3b@pool-74-105-2-138.nwrknj.fios.verizon.net) |
| 23:10:49 | <cpli> | "TChan", "STM.TChan". yes, and multithreading requires STM, I assume |
| 23:11:00 | <dminuoso> | No, we have threads without STM just fine. |
| 23:11:11 | <dminuoso> | STM is just the basis for most our synchronization tools. |
| 23:11:23 | <dminuoso> | Think of STM as setting up transactions around critical sections. |
| 23:11:55 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 23:12:00 | <dminuoso> | or well, avoiding the need for critical sections, even. |
| 23:12:32 | <dminuoso> | cpli: Basically we have two things at our disposal: We have MVar and STM |
| 23:12:34 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 23:13:46 | <dminuoso> | Both can help with synchronizing multiple threads. MVar is a really low level primitive that you can build higher primitives around (say like a semaphore), whereas STM is a potent high level framework (its not based on MVar, though) |
| 23:13:54 | <cpli> | oh this is actually way cooler than i expected |
| 23:14:18 | <cpli> | i require awaitEvent :: _ -> IO Event |
| 23:14:29 | <cpli> | actually no |
| 23:14:49 | <dminuoso> | Sure, just wrap the body in `atomically` then you can make it `IO Event` |
| 23:14:57 | <cpli> | this may await an event from `b1` indefinitely |
| 23:15:12 | <dminuoso> | Either would |
| 23:15:12 | <cpli> | whilst `b2` is broadcasting |
| 23:15:33 | <dminuoso> | Why would it?> |
| 23:16:10 | <cpli> | if `b1` recieves an event `FromB1` it creates another `B1Event` |
| 23:16:36 | <cpli> | otherwise `awaitEvent` return the event from `bn` |
| 23:16:41 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 23:16:41 | <dminuoso> | Well, each backend will likely have to run two separate threads, yes. |
| 23:16:42 | → | danza joins (~francesco@151.35.98.197) |
| 23:16:58 | <cpli> | and `race` with Control.Concurrent |
| 23:17:03 | <dminuoso> | Or you have some kind of event loop and use tryReadTChan instead |
| 23:17:49 | <cpli> | i think for each backend to either be: |
| 23:17:55 | <cpli> | 1. broadcasting its own event |
| 23:18:07 | <cpli> | 2. processing an event it recieved |
| 23:18:11 | <cpli> | is relatively elgant |
| 23:18:39 | cpli | thinks their typos probably aren't exactly elegant |
| 23:19:27 | → | jmorris joins (uid537181@id-537181.uxbridge.irccloud.com) |
| 23:19:53 | <dminuoso> | cpli: Updated gist |
| 23:20:04 | × | Sgeo quits (~Sgeo@user/sgeo) (Ping timeout: 250 seconds) |
| 23:20:34 | <dminuoso> | Whether a simple `runBackend b = forever $ do r <- tryAwaitEvent ...` or STM variant instead makes more sense, depends on what you want to do exactly |
| 23:20:49 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5147:575b:dd93:ff03) |
| 23:21:09 | <dminuoso> | Also think ahead about things like termination |
| 23:21:19 | <dminuoso> | Might want to include some kind of signaling layer in the event stream |
| 23:21:38 | <dminuoso> | Such that the worker can just stop gracefully, perhaps release resources |
| 23:21:59 | <cpli> | doesn't `TMChan` solve such a scenario? |
| 23:22:35 | <dminuoso> | Sure, if you fancy that. |
| 23:22:39 | <dminuoso> | I would probably just roll my own |
| 23:23:01 | <cpli> | i have to admit i don't know why you're checking if eventTag e == backendTag (bwcBackend b) |
| 23:23:11 | <dminuoso> | Writing such thing on the spot takes little effort and it helps keep dependency footprints small. And it lets you model your combinators the way you need to. |
| 23:23:24 | <cpli> | if it recieves a message from itself it tries agai- |
| 23:23:27 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 23:23:28 | <cpli> | makes sense. |
| 23:24:29 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 258 seconds) |
| 23:24:43 | <dminuoso> | cpli: For elaborate things, you may have to spawn two thread for each backend, potentially with TQueues or things between them for coordinations. |
| 23:25:00 | <dminuoso> | This is all just different options, without knowing what these backends really do its hard to tell |
| 23:25:01 | <cpli> | dminuoso the backends both come from relatively large dependencies, i've come this far only by scouting stackage for package versions that don't clash on their version of `ByteString` and downgrading from ghc 9.4.2 to 9.0.2 |
| 23:25:15 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 258 seconds) |
| 23:25:42 | <cpli> | they're xmpp and irc |
| 23:25:47 | <cpli> | i'm writing a bridge. |
| 23:25:53 | <cpli> | cat's out the bag |
| 23:26:04 | <dminuoso> | So there's just two backends then? |
| 23:26:11 | <cpli> | well, extensibility |
| 23:26:21 | <dminuoso> | As a kind of star bridge? |
| 23:26:36 | <cpli> | currently my dhall config only lets you specify bots for either backend, but yes, a star bridge |
| 23:26:44 | <cpli> | plans for discord etc |
| 23:27:11 | <cpli> | the thing i want to implement really is proper puppeteering for irc |
| 23:27:13 | <dminuoso> | cpli: I think I would just spawn two threads for each backend. |
| 23:27:20 | <cpli> | exaclty |
| 23:27:27 | <cpli> | s/cl/lc/ |
| 23:27:28 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 23:27:38 | <dminuoso> | Haskell threads are really cheap, so go wild with them. |
| 23:27:45 | <cpli> | they are? |
| 23:27:53 | <dminuoso> | Yes, they are green threads. |
| 23:28:32 | <cpli> | haskell knew of that color before go's implementation? |
| 23:28:37 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 272 seconds) |
| 23:29:01 | <dminuoso> | Honestly I dont know of the ethymology. :) |
| 23:29:18 | <dminuoso> | Sorry I should refine. *GHC threads cheap |
| 23:29:46 | <cpli> | it has something to do with async, where threads are coloured red or blue, and state needs to stay in one color |
| 23:29:55 | <cpli> | but green sits on top ignoring all of that |
| 23:30:07 | <dminuoso> | Im almost confident that the name is older than go. |
| 23:30:46 | <cpli> | yup 1997: "Green threads refers to the name of the original thread library for the programming language Java (that was released in version 1.1 and then Green threads were abandoned in version 1.3 to native threads). It was designed by The Green Team at Sun Microsystems." |
| 23:30:56 | <cpli> | from wikipedia the *free* encyclopedia |
| 23:31:00 | <dminuoso> | https://web.archive.org/web/20080530073139/http://java.sun.com/features/1998/05/birthday.html |
| 23:31:06 | <dminuoso> | Well I prefer citing the primary source. :) |
| 23:31:20 | × | mvk quits (~mvk@2607:fea8:5ce3:8500::f30b) (Ping timeout: 250 seconds) |
| 23:31:48 | <cpli> | find on page: "green threads" 0/0 results |
| 23:31:52 | <dminuoso> | Heh its funny, isnt it. |
| 23:32:01 | <dminuoso> | Quality control at its finest |
| 23:32:37 | <dminuoso> | cpli: the cool thing about the way things are implemented in haskell, is that you get the best of all worlds combined. |
| 23:32:59 | × | thyriaen quits (~thyriaen@2a01:aea0:dd4:470d:6245:cbff:fe9f:48b1) (Remote host closed the connection) |
| 23:32:59 | × | thyriaen_ quits (~thyriaen@2a01:aea0:dd4:470d:6245:cbff:fe9f:48b1) (Remote host closed the connection) |
| 23:33:29 | <dminuoso> | You can just use blocking IO in threads, and the RTS will be aware of that, use non-blockin IO behind the scenes, schedule threads when data is available again |
| 23:33:44 | <dminuoso> | And you still get parallelism since GHC can use multiple capabilities |
| 23:33:53 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 276 seconds) |
| 23:33:55 | <jbggs[m]> | I thought red/blue functions was a different thing from green threads |
| 23:34:16 | <dminuoso> | And when I say Haskell, I really mean GHC Haskell. |
| 23:34:34 | <cpli> | systemFω here to save the day |
| 23:35:03 | <jbggs[m]> | i.e. red functions are async functions, which in many languages are run on green threads |
| 23:35:21 | <cpli> | jbggs[m]: i apologise, i relay uncited information. |
| 23:35:35 | <jbggs[m]> | or at least can be |
| 23:35:59 | <monochrom> | amd functions, intel functions, and nvidia threads? >:) |
| 23:36:04 | <cpli> | dminuoso: this is the haskell irc, before i denounce things without thought |
| 23:36:13 | <cpli> | do people here use compilers other than ghc? |
| 23:36:21 | <dminuoso> | monochrom: If you want crazy terminology, look at ARINC 653. |
| 23:36:55 | <jbggs[m]> | I think it's interesting that people are prone to thinking of these things with colors |
| 23:36:56 | <jbggs[m]> | cpli: no harm no foul :D |
| 23:37:11 | <dminuoso> | They contort established terminology to the point where they will sell you a "list" as an "OS process" (slightly exaggerating, but not by much) |
| 23:37:25 | <monochrom> | Oh there are people who listen to music and see colours, too. |
| 23:37:26 | × | mixfix41 quits (~sdeny9ee@user/mixfix41) (Ping timeout: 260 seconds) |
| 23:37:40 | <jbggs[m]> | I mean they're both functors right :V |
| 23:37:50 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
| 23:38:08 | <jbggs[m]> | lists and OS processes i mean |
| 23:38:12 | × | gurkenglas quits (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 23:38:18 | <cpli> | jbggs[m]: smells like 2-cats |
| 23:38:45 | <cpli> | sorry, i meant 2d operads |
| 23:38:49 | <jbggs[m]> | 2-cats? |
| 23:39:11 | <EvanR> | cpli, within the atomically, it's like there are no other threads or they don't do anything that matters. So you read what you just wrote. If anything would have happened to change that, the atomically doesn't happen (retry) |
| 23:39:54 | <dminuoso> | *semantically |
| 23:39:56 | <jbggs[m]> | That's a new word for me, operad |
| 23:39:58 | <cpli> | EvanR, if i remember anything correctly STM basically locks for any other thread trying to access the same memory region |
| 23:40:05 | <dminuoso> | cpli: No. |
| 23:40:08 | <cpli> | q-q |
| 23:40:08 | <dminuoso> | cpli: its lock-free. |
| 23:40:11 | <cpli> | q-q |
| 23:40:16 | cpli | in awe |
| 23:40:26 | <EvanR> | locking sounds like an implementation thing, which it doesn't use but really shouldn't matter to this story |
| 23:40:29 | <cpli> | wait-free too? |
| 23:40:38 | <monochrom> | Well, I'm fine with a suitable definition of "basically". |
| 23:41:21 | <EvanR> | one slow implementation strategy is to run all STM actions sequentially, perhaps using a shared global lock |
| 23:42:03 | <monochrom> | Basically, if you only notice final answers and don't notice speed, STM gives the same answer as locking. |
| 23:42:18 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 23:42:28 | → | perrierjouet joins (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) |
| 23:42:39 | <monochrom> | If you pay attention to speed, STM is sometimes faster than locking, sometimes slower. |
| 23:42:42 | <cpli> | jbggs[m]: "cats" or categories, 2-cats are cats with 0-cells (your normal objects) 1-cells (arrows between your objects) and arrows between your objects etc. operads are a way to represent cells, which is another matter |
| 23:43:22 | <EvanR> | do operads have anything to do with monads |
| 23:43:38 | <monochrom> | Although, the sad thing is that the very word "transactional" in the very name has already told you how it does it, but people have never learned transactions, they have only learned locking. |
| 23:43:53 | <cpli> | not necessarily, but also yes, unless they don't EvanR |
| 23:44:18 | <EvanR> | that's the worst bit of category theory ever |
| 23:45:16 | <cpli> | operads are just shapes that give you some way of "glueing" them together to get new shapes |
| 23:45:31 | <cpli> | i.e. composition if you think of the edges of your shapes as arrows |
| 23:45:52 | <cpli> | i.e. glueing from topology if you get really weird |
| 23:46:00 | → | polo joins (~polo@user/polo) |
| 23:46:06 | <cpli> | i.e. homotopies if you haven't slept for 2 weeks |
| 23:46:45 | <talismanick> | monochrom: "If you want to write CS research today, look at what the database people were doing 2 decades ago" |
| 23:46:56 | <cpli> | monochrom, what does transactional entail? |
| 23:47:00 | <talismanick> | I forget who said that, but the more I read, the more it rings true... |
| 23:47:12 | <EvanR> | what database people other than mysql was doing 2 decades ago |
| 23:47:13 | <cpli> | i.e. "ownership" in rust terms is always handed along? |
| 23:47:22 | <talismanick> | cpli: ACIDity |
| 23:47:41 | <EvanR> | the I in ACID corresponds to transactional |
| 23:47:50 | <cpli> | of course it does |
| 23:47:56 | <monochrom> | Learn "database transactions". If you don't see "roll back" you aren't learning transactions. |
| 23:48:01 | × | polo quits (~polo@user/polo) (Client Quit) |
| 23:48:02 | × | Tuplanolla quits (~Tuplanoll@91-159-69-11.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:48:16 | <dminuoso> | Gosh, did Microsoft really remove SPJs papers website? :( |
| 23:48:18 | <talismanick> | Or, at least, the A and I parts - C is up to the programmer, and D is outside the scope of STM |
| 23:48:28 | <dminuoso> | I wish hyperlinks would just stay alive... |
| 23:48:38 | <EvanR> | i was downloading spj papers from microsoft a couple weeks ago |
| 23:48:56 | <cpli> | oh |
| 23:49:22 | <monochrom> | I think https://simon.peytonjones.org/publications/ helps. |
| 23:49:41 | <cpli> | start doing x, do x in y, if x fails, restore y |
| 23:50:02 | <EvanR> | begin transaction; do whatever, do whatever, do whatever, commit |
| 23:50:31 | <cpli> | or record y, do f, if f fails, restore y and override g's operation on y |
| 23:50:32 | <EvanR> | let the database figure out how to interleave it all |
| 23:50:55 | <EvanR> | while maintaining the invariants |
| 23:51:24 | <cpli> | i guess `I` ruins my joke |
| 23:51:44 | <dminuoso> | cpli: Anyway, the way GHC implements STM, is by just running the transactional code without any lock, along the way it records a transaction log of what it has does, and if at the end the log is consistent it will commit that to memory. |
| 23:51:49 | <cpli> | how do you guarantee `I` on non-hardware-atomics? |
| 23:51:55 | <cpli> | i.e. entire memory regions? |
| 23:52:30 | <dminuoso> | And if it doesnt, it can retry that block. Given that it has a transactional log, it can then block until it *knows* that a dependent variable has changed (no need to retry if none of the read variables havent changed) |
| 23:53:03 | <cpli> | dminuoso, oh, it's the weird "transform any algorithm into a wait-free algorithm vm" |
| 23:53:21 | <dminuoso> | I do not know that transformation |
| 23:53:30 | <cpli> | no? |
| 23:53:34 | <cpli> | one-moment |
| 23:53:48 | <EvanR> | what would wait free mean in this context |
| 23:54:06 | <monochrom> | I know lock-free, I don't know wait-free. |
| 23:54:08 | <cpli> | http://cs.technion.ac.il/~erez/Papers/wf-simulation-full.pdf |
| 23:54:16 | <cpli> | wait, this turns lock-free into wait-free |
| 23:54:22 | <cpli> | dammit |
| 23:54:25 | <monochrom> | Wouldn't it be nice if vaccination clinics were wait-free >:) |
| 23:54:41 | × | chomwitt quits (~chomwitt@2a02:587:dc10:8200:1ac0:4dff:fedb:a3f1) (Ping timeout: 276 seconds) |
| 23:55:14 | <dminuoso> | monochrom: They can be, just start coughing enough and ask loudly-but-not-too-loudly for the vaccination against your hot COVID infection. |
| 23:55:22 | <talismanick> | cpli: so, wait-free means no live locks... ? |
| 23:56:15 | <cpli> | wait-free is pseudo termination-guarantees |
| 23:56:32 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 23:56:32 | <monochrom> | I think they would immediately send you home instead. But hey, "abort early, abort often" is more wait-free than "wait then abort anyway". |
| 23:56:32 | <dminuoso> | cpli: Im not sure this really compares. One of the crucial things is that if the view of memory is not consistent (which it might be), it will retry. |
| 23:57:09 | <cpli> | talismanick: `push` **will succeed** in n cpu-cycles |
| 23:57:50 | <cpli> | dminuoso: how do you ensure termination? i.e. stop the vm from retrying indefinitely? |
| 23:58:05 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 23:58:29 | <dminuoso> | cpli: two things: a) since a transaction log is kept, you can only retry when there's a possibility of obtaining a different result |
| 23:58:42 | <monochrom> | In usage of STM we just ask for fairness, I think. |
| 23:58:50 | <cpli> | dminuoso: interesting. |
| 23:58:52 | <dminuoso> | b) just some optimism that concurrency is not crazy wild I suppose? |
| 23:59:00 | → | euandreh joins (~euandreh@179.214.113.107) |
| 23:59:05 | <cpli> | B) |
| 23:59:13 | <talismanick> | aaaaah, so it's the opposite of what I said - no deadlocks , but can have livelocks (each part succeeds in allotted time without being starved externally, but end up ping-pong'ing each other and cause the system to make no progress) |
| 23:59:13 | <dminuoso> | I mean yeah, if you keep extremely large transactions, retrying will get more expensive |
| 23:59:22 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
| 23:59:46 | <talismanick> | interesting |
All times are in UTC on 2022-10-28.