Logs: freenode/#haskell
| 2021-03-08 13:28:30 | <chisui> | merijn: I actually expect conflicting updates, since I write from many threads. |
| 2021-03-08 13:28:42 | <merijn> | chisui: Yeah, but how frequently? :p |
| 2021-03-08 13:28:57 | <merijn> | Like, 100% of your updates, 50% of your updates, or 10% of them ;) |
| 2021-03-08 13:31:02 | <merijn> | chisui: Basically, STM assumes it will succeed, run a computation and at the end it will check nothing has happened "in between". So if 2 threads are trying to update the same TVar, one will win, the other will rollback and "redo" the computation. The cost of that depends on how frequently your concurrent updates happen to conflict. |
| 2021-03-08 13:31:05 | <chisui> | The values of the cells are semilattices (like Set) and they collect facts. These facts are propagated through the entire network all the time, since it's the main form of communication in the system |
| 2021-03-08 13:32:13 | <chisui> | I'll have to measure what the actual frequency is. |
| 2021-03-08 13:33:00 | <merijn> | chisui: Gut feeling is ok. Suppose you have thousands of cells and ten threads, if those threads are somewhat randomly updating cells, conflicts should be fairly rare, for example |
| 2021-03-08 13:33:30 | <merijn> | chisui: The optimistic locking is *considerably* faster then MVars in the non-conflicting case, so you can win quite a bit |
| 2021-03-08 13:35:46 | → | bitmapper joins (uid464869@gateway/web/irccloud.com/x-zlhchyvsgfxybgra) |
| 2021-03-08 13:37:17 | <chisui> | merijn: That sounds reasonable. I may have many `forkIO` threads writing, but the actual number of threads woll be low |
| 2021-03-08 13:37:19 | <chisui> | *will |
| 2021-03-08 13:37:42 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-08 13:37:50 | × | hiroaki quits (~hiroaki@2a02:8108:8c40:2bb8:2846:3c47:a8c:db47) (Ping timeout: 264 seconds) |
| 2021-03-08 13:37:50 | → | hiroaki1 joins (~hiroaki@2a02:8108:8c40:2bb8:1b99:a7f4:2a9d:6474) |
| 2021-03-08 13:38:28 | <merijn> | chisui: So unless you expect to have like 10s of threads repeatedly racing on one cell it'll probably be better to go straight to STM and skip MVar |
| 2021-03-08 13:39:13 | → | bitmagie joins (~Thunderbi@200116b806c05f001879c69ab5903a67.dip.versatel-1u1.de) |
| 2021-03-08 13:40:54 | × | gnumonic quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 2021-03-08 13:41:27 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 2021-03-08 13:41:45 | <chisui> | Thank you merijn |
| 2021-03-08 13:45:02 | × | bitmagie quits (~Thunderbi@200116b806c05f001879c69ab5903a67.dip.versatel-1u1.de) (Quit: bitmagie) |
| 2021-03-08 13:45:26 | → | ddellacosta joins (~ddellacos@86.106.143.115) |
| 2021-03-08 13:49:00 | × | drbean quits (~drbean@TC210-63-209-202.static.apol.com.tw) (Quit: ZNC 1.8.2+cygwin2 - https://znc.in) |
| 2021-03-08 13:49:03 | × | Feuermagier quits (~Feuermagi@2a02:2488:4211:3400:246e:bf09:8453:9d6) (Remote host closed the connection) |
| 2021-03-08 13:49:36 | → | Feuermagier joins (~Feuermagi@2a02:2488:4211:3400:246e:bf09:8453:9d6) |
| 2021-03-08 13:49:47 | × | Chai-T-Rex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Ping timeout: 268 seconds) |
| 2021-03-08 13:51:16 | × | ADG1089__ quits (~aditya@223.226.235.12) (Remote host closed the connection) |
| 2021-03-08 13:51:21 | → | Chai-T-Rex joins (~ChaiTRex@gateway/tor-sasl/chaitrex) |
| 2021-03-08 13:52:57 | × | ddellacosta quits (~ddellacos@86.106.143.115) (Remote host closed the connection) |
| 2021-03-08 13:57:36 | → | ep1ctetus joins (~epictetus@ip72-194-215-136.sb.sd.cox.net) |
| 2021-03-08 13:58:38 | × | frozenErebus quits (~frozenEre@94.128.82.20) (Ping timeout: 260 seconds) |
| 2021-03-08 14:01:03 | × | acidjnk_new quits (~acidjnk@p200300d0c72b9523190c92979cea572a.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2021-03-08 14:08:08 | × | gzj quits (~gzj@unaffiliated/gzj) (Remote host closed the connection) |
| 2021-03-08 14:08:31 | → | gzj joins (~gzj@unaffiliated/gzj) |
| 2021-03-08 14:09:06 | × | gzj quits (~gzj@unaffiliated/gzj) (Remote host closed the connection) |
| 2021-03-08 14:09:30 | → | gzj joins (~gzj@unaffiliated/gzj) |
| 2021-03-08 14:09:42 | × | edo-codes quits (916b64e1@145.107.100.225) (Ping timeout: 240 seconds) |
| 2021-03-08 14:13:06 | × | gzj quits (~gzj@unaffiliated/gzj) (Remote host closed the connection) |
| 2021-03-08 14:13:26 | → | gzj joins (~gzj@unaffiliated/gzj) |
| 2021-03-08 14:14:08 | × | gzj quits (~gzj@unaffiliated/gzj) (Remote host closed the connection) |
| 2021-03-08 14:14:29 | → | gzj joins (~gzj@unaffiliated/gzj) |
| 2021-03-08 14:15:07 | × | gzj quits (~gzj@unaffiliated/gzj) (Remote host closed the connection) |
| 2021-03-08 14:15:32 | × | AWizzArd quits (~code@gehrels.uberspace.de) (Changing host) |
| 2021-03-08 14:15:32 | → | AWizzArd joins (~code@unaffiliated/awizzard) |
| 2021-03-08 14:17:02 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-03-08 14:17:30 | → | Mrbuck joins (~Mrbuck@gateway/tor-sasl/mrbuck) |
| 2021-03-08 14:17:36 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:9814:d93f:56c2:c87) |
| 2021-03-08 14:20:15 | dexter | is now known as dexterfoo |
| 2021-03-08 14:22:14 | × | Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 264 seconds) |
| 2021-03-08 14:22:50 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:9814:d93f:56c2:c87) (Ping timeout: 264 seconds) |
| 2021-03-08 14:28:06 | <Gurkenglas> | A total function is one that maps total inputs to total outputs (nonfunctions are total if there are no undefineds). newtype Bot = Bot { unBot :: Bot -> Bool }. What Bots are total? There may be multiple fixed points, and no obvious reason for there to be a least or greatest one. But nice = Bot $ const True is total. So is paladin = Bot $ \x -> unBot x nice. So is ditto = Bot (\x -> unBot x x): If x is total, applying it to itself will be |
| 2021-03-08 14:28:06 | <Gurkenglas> | total. But wait: unBot ditto ditto diverges, so it can't be total! Therefore there is no fixed point. But I was still able to meaningfully call paladin total. Is there a theory that lets me talk about these meaningful statements? |
| 2021-03-08 14:28:49 | <heck-to-the-gnom> | How do I type a function to deal with both `Maybe a` and `a`? |
| 2021-03-08 14:29:01 | → | forgottenone joins (~forgotten@176.42.24.161) |
| 2021-03-08 14:29:18 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-112-176.w86-198.abo.wanadoo.fr) |
| 2021-03-08 14:29:21 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-03-08 14:29:51 | <jacks2> | accept a, use fmap to use it with Maybe a |
| 2021-03-08 14:29:57 | <geekosaur> | heck-to-the-gnom, they're different types, you can't treat them as the same (aside from the same way `id` does) |
| 2021-03-08 14:30:02 | <merijn> | heck-to-the-gnom: You don't |
| 2021-03-08 14:30:06 | × | LKoen_ quits (~LKoen@194.250.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 2021-03-08 14:30:12 | <Gurkenglas> | heck-to-the-gnom, do you want a way to add a default result to a function that takes a, so it can handle Maybe a? |
| 2021-03-08 14:30:49 | × | elliott__ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
| 2021-03-08 14:31:08 | <pjb> | heck-to-the-gnom: data Both a = Maybe a | Only a ; foo :: Both a -> a |
| 2021-03-08 14:31:48 | <pjb> | Of course, there's not much difference between Just a and Only a… |
| 2021-03-08 14:31:58 | <Gurkenglas> | > maybe 3 (+1) (Just 10) |
| 2021-03-08 14:32:00 | <lambdabot> | 11 |
| 2021-03-08 14:32:02 | <Gurkenglas> | > maybe 3 (+1) Nothing |
| 2021-03-08 14:32:03 | <lambdabot> | 3 |
| 2021-03-08 14:32:04 | <Gurkenglas> | Is this what you want? |
| 2021-03-08 14:34:06 | × | SquidDev quits (~SquidDev@autoclave.squiddev.cc) (Quit: Ping timeout (120 seconds)) |
| 2021-03-08 14:34:28 | → | SquidDev joins (~SquidDev@autoclave.squiddev.cc) |
| 2021-03-08 14:34:30 | → | carlomagno joins (~cararell@148.87.23.4) |
| 2021-03-08 14:35:16 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 2021-03-08 14:35:58 | × | coot quits (~coot@37.30.55.141.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2021-03-08 14:36:49 | → | frozenErebus joins (~frozenEre@94.128.82.20) |
| 2021-03-08 14:37:22 | × | Pickchea quits (~private@unaffiliated/pickchea) (Ping timeout: 260 seconds) |
| 2021-03-08 14:38:19 | × | MidAutumnHotaru quits (~MidAutumn@unaffiliated/midautumnhotaru) (Quit: Quit 啾) |
| 2021-03-08 14:38:58 | → | MidAutumnHotaru joins (~MidAutumn@unaffiliated/midautumnhotaru) |
| 2021-03-08 14:40:12 | <heck-to-the-gnom> | Upon looking at my errors closer, I think what I actually want is how to convert to Maybe. Gurkenglas, I think that's what I want. Why's there a +1 in there? |
| 2021-03-08 14:40:40 | <geekosaur> | it's an example |
| 2021-03-08 14:41:11 | <geekosaur> | it's showing how to perform some operation (here, (+1)) "through" a Maybe to the value contained within, if any |
| 2021-03-08 14:41:16 | <jacks2> | heck-to-the-gnom, what's the big picture |
| 2021-03-08 14:42:03 | heck-to-the-gnom | uploaded an image: image.png (31KiB) < https://matrix.org/_matrix/media/r0/download/matrix.org/vJiaIdLaVNmAhNjnloqEapIL/image.png > |
| 2021-03-08 14:42:07 | <heck-to-the-gnom> | jacks2 ^ |
| 2021-03-08 14:43:30 | <dolio> | Gurkenglas: The place that 'total' and 'partial' vocabulary come from don't allow you to define a type like that, so I'm not sure it makes sense to expect it to hold up in that situation. |
| 2021-03-08 14:44:13 | <Gurkenglas> | dolio, then imagine i said "cool" instead of "total" |
| 2021-03-08 14:44:35 | → | CodeAlways joins (uid272474@gateway/web/irccloud.com/x-dzvbbhipleasvhkv) |
| 2021-03-08 14:44:52 | <dolio> | Okay, then your specification of 'cool' is incoherent. |
| 2021-03-08 14:46:46 | <dolio> | Or the application, I guess. |
| 2021-03-08 14:48:43 | <dolio> | I guess maybe you could pin the flaw in your reasoning on thinking that 'unbot' is total. |
| 2021-03-08 14:49:16 | × | geekosaur quits (82650c7a@130.101.12.122) (Quit: Connection closed) |
| 2021-03-08 14:49:20 | <dolio> | What happens if you classify `unBot` as non-total? |
| 2021-03-08 14:50:24 | → | Sgeo joins (~Sgeo@ool-18b98aa4.dyn.optonline.net) |
| 2021-03-08 14:50:36 | → | atraii joins (~atraii@c-174-52-203-201.hsd1.ut.comcast.net) |
| 2021-03-08 14:51:48 | × | notzmv quits (~zmv@unaffiliated/zmv) (Ping timeout: 246 seconds) |
| 2021-03-08 14:51:56 | <dolio> | Anyhow, negative types are pretty well known to allow you to write paradox type stuff. |
| 2021-03-08 14:52:19 | <dolio> | And they only have semantics in stuff like domains and general recursion. |
| 2021-03-08 14:53:24 | <dolio> | Basically because assuming that one exists lets you write some sort of general recursion. In this case it would give you general recursion on Bool. |
| 2021-03-08 14:53:47 | → | toorevitimirp joins (~tooreviti@117.182.183.154) |
| 2021-03-08 14:54:14 | × | elliott_ quits (~elliott_@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 245 seconds) |
| 2021-03-08 14:54:51 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:11c5:786:f774:d85e) |
All times are in UTC.