Logs: freenode/#haskell
| 2020-10-05 22:02:37 | <carter> | yeah, evaluation order + dualitiies is nice |
| 2020-10-05 22:02:44 | <ski> | monochrom : one way to understand this constructivistic kerfuffle about "subfinite" and so on, is to think of it as being about "stages of knowledge" |
| 2020-10-05 22:03:25 | <dolio> | That's definitely the Brouwerian angle, I think. |
| 2020-10-05 22:03:52 | <ski> | (but in an epistemic modal logic, one has an explicit connective for "known" (often "by some particular agent"). but in a constructive setting, it's so to speak "built in") |
| 2020-10-05 22:03:54 | <carter> | dolio: which semantics for par are you drawing from? |
| 2020-10-05 22:04:03 | <carter> | i think choice/& is also cbn |
| 2020-10-05 22:04:10 | <dolio> | carter: I was thinking of Compiling with Classical Connectives. |
| 2020-10-05 22:04:26 | <dolio> | Yeah, & is also call-by-name. |
| 2020-10-05 22:04:31 | <dolio> | And × is by-value. |
| 2020-10-05 22:04:33 | <ski> | monochrom : but yes, the Kripke semantics for intuitionistic logic is, iiuc, related to the one for epistemic modal logic |
| 2020-10-05 22:04:40 | × | pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 2020-10-05 22:05:04 | <carter> | do whats their semantics for par? (i'd actually wanted to read that paper when i found it a few months ago, but it fell off my queue) |
| 2020-10-05 22:05:06 | <int-e> | ("new-ish"... refers to ghc 7.10 here, I think.) |
| 2020-10-05 22:05:10 | <ski> | (there's a "modal translation" from the former logic to the latter. at least in the propositional case, dunno about how it works with the quantifiers) |
| 2020-10-05 22:06:05 | <dolio> | ski: You should definitely look at that paper, by the way. It's got arbitrary (co)data types with constructors whose types are sequents, and can have arbitrarily many value and continuation fields. |
| 2020-10-05 22:06:13 | <ski> | dolio : oh .. that's a bit strange (the "i can't distinguish between two and infinity" one) |
| 2020-10-05 22:06:17 | <dolio> | I think I've pointed you to it, but I don't know if you've seen it. |
| 2020-10-05 22:06:26 | × | oisdk quits (~oisdk@2001:bb6:3329:d100:189f:9172:61d6:2b9e) (Quit: oisdk) |
| 2020-10-05 22:07:01 | <ski> | carter : hm, did you look into the paper by Wadler about relating session types to linear logic ? |
| 2020-10-05 22:07:12 | <carter> | session types are trash :) |
| 2020-10-05 22:07:30 | → | oisdk joins (~oisdk@2001:bb6:3329:d100:e56d:4357:c75:2f61) |
| 2020-10-05 22:07:35 | <dolio> | carter: A par continuation is two continuations, and a par value is a lambda term that binds two continuations, I think. |
| 2020-10-05 22:07:49 | <carter> | ok, that sounds correct |
| 2020-10-05 22:07:54 | <carter> | its forkIO by another name ! |
| 2020-10-05 22:08:08 | <ski> | i think the "cbn" vs. "cbv" distinction you mentioned above is more or less the same as the "negative" vs. "positive" one, that's cropping up in some cases (focusing, uniform proof) |
| 2020-10-05 22:08:08 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2020-10-05 22:08:31 | <carter> | or "cbpv" |
| 2020-10-05 22:08:33 | <dolio> | Yes, but another cool thing this paper does is incorporate call-by-need and call-by-coneed. |
| 2020-10-05 22:08:40 | <carter> | ... whats that even mean |
| 2020-10-05 22:08:48 | <carter> | *coneed |
| 2020-10-05 22:08:57 | <ski> | dolio : hm, i haven't seen this one before. ty for the suggestion |
| 2020-10-05 22:09:26 | → | machinedgod joins (~machinedg@142.169.78.240) |
| 2020-10-05 22:09:53 | <dolio> | -by-need saves work when you do a let that gets used multiple times. -by-coneed saves work when you do a shift where the continuation gets used multiple times, or something. |
| 2020-10-05 22:10:19 | ski | . o O ( "Compiling with Classical Connectives" by Paul Downen,Zena M. Ariola in 2020-08-28 at <https://arxiv.org/abs/1907.13227> ) |
| 2020-10-05 22:10:37 | <fraktor> | Hey, I've been trying to find definitive sources on this (admittedly controversial) topic: what's the plan for the new record syntax? |
| 2020-10-05 22:11:41 | <ski> | carter : well, that session types paper does evoke such analogies as `forkIO' |
| 2020-10-05 22:12:18 | <ski> | dolio, hm, interesting |
| 2020-10-05 22:12:19 | × | albethere quits (sid457088@gateway/web/irccloud.com/x-fnvfojoflynertwf) (Ping timeout: 272 seconds) |
| 2020-10-05 22:12:25 | <carter> | ski: explicitly? |
| 2020-10-05 22:12:25 | <carter> | i gave a talk where i dervied it |
| 2020-10-05 22:12:57 | × | alanz quits (sid110616@gateway/web/irccloud.com/x-rotyfkerxdfrgsjt) (Ping timeout: 272 seconds) |
| 2020-10-05 22:13:45 | <ski> | carter : i don't recall if it's mentioned explicitly. but i did a presentation of the paper (first part was a refreshed of linear logic), which ended by a translation table having terms like "spawn" and "join" for the `par' case |
| 2020-10-05 22:13:53 | <dolio> | ski: It's probably not all novel, but it was the first time I've seen almost everything in the paper (because I slacked on learning CBPV), so it just seemed like one cool idea after another when I read it. :) |
| 2020-10-05 22:14:03 | <ski> | (s/refreshed/refresher/) |
| 2020-10-05 22:14:31 | → | alanz joins (sid110616@gateway/web/irccloud.com/x-hhuchzrtvkxyanvu) |
| 2020-10-05 22:14:51 | × | dmj` quits (sid72307@gateway/web/irccloud.com/x-adxoyhgdabwnfahc) (Ping timeout: 272 seconds) |
| 2020-10-05 22:15:19 | <koz_> | :t maybe empty pure |
| 2020-10-05 22:15:21 | <lambdabot> | Alternative f => Maybe a -> f a |
| 2020-10-05 22:15:29 | × | liszt_ quits (sid336875@gateway/web/irccloud.com/x-yllqqkokdlggifua) (Ping timeout: 272 seconds) |
| 2020-10-05 22:15:47 | → | albethere joins (sid457088@gateway/web/irccloud.com/x-uubpnvrpjsbjfkmg) |
| 2020-10-05 22:15:50 | <ski> | koz_ : i sometimes wish that was in a "standard library" |
| 2020-10-05 22:15:52 | → | liszt_ joins (sid336875@gateway/web/irccloud.com/x-uuxepiucxpvvjuow) |
| 2020-10-05 22:15:59 | <koz_> | ski: Yeah, you and me both. |
| 2020-10-05 22:16:04 | <koz_> | It's probbo in extra or something. |
| 2020-10-05 22:16:07 | × | conjunctive quits (sid433686@gateway/web/irccloud.com/x-ddwejxzgxrdkpmwd) (Ping timeout: 272 seconds) |
| 2020-10-05 22:16:07 | × | elvishjerricco quits (sid237756@NixOS/user/ElvishJerricco) (Ping timeout: 272 seconds) |
| 2020-10-05 22:16:07 | × | tchar quits (sid301738@gateway/web/irccloud.com/x-squtmljpvmzfdfsk) (Ping timeout: 272 seconds) |
| 2020-10-05 22:16:07 | × | adius quits (sid321344@gateway/web/irccloud.com/x-hdzjqmobobrptkzk) (Ping timeout: 272 seconds) |
| 2020-10-05 22:16:28 | hackage | tini 0.1.0.1 - Tiny INI file and configuration library with a minimal dependency footprint. https://hackage.haskell.org/package/tini-0.1.0.1 (AntonEkblad) |
| 2020-10-05 22:16:29 | → | tchar joins (sid301738@gateway/web/irccloud.com/x-rgpmjtqqbhrmcohe) |
| 2020-10-05 22:16:45 | × | SrPx quits (sid108780@gateway/web/irccloud.com/x-czvvabmhqaigtsgp) (Ping timeout: 272 seconds) |
| 2020-10-05 22:16:57 | <carter> | ski: oh, it def does that, the issue i have with session types is that a lotta expositions kinda treat par as not being symmetric in the two args |
| 2020-10-05 22:16:59 | → | dmj` joins (sid72307@gateway/web/irccloud.com/x-khxpyzsgwpyndoap) |
| 2020-10-05 22:17:19 | → | SrPx joins (sid108780@gateway/web/irccloud.com/x-lqrnqgbzvbfaqfbf) |
| 2020-10-05 22:17:35 | × | albethere quits (sid457088@gateway/web/irccloud.com/x-uubpnvrpjsbjfkmg) (Max SendQ exceeded) |
| 2020-10-05 22:17:52 | → | albethere joins (sid457088@gateway/web/irccloud.com/x-lwglmvolkygoqkcg) |
| 2020-10-05 22:18:10 | → | adius joins (sid321344@gateway/web/irccloud.com/x-fevubjfnjnczxgiy) |
| 2020-10-05 22:18:18 | → | conjunctive joins (sid433686@gateway/web/irccloud.com/x-svszloomofjzwqrv) |
| 2020-10-05 22:18:23 | → | falafel joins (~falafel@2605:e000:1527:d491:99fe:5613:f0a7:56f0) |
| 2020-10-05 22:18:33 | <dolio> | carter: I guess in more detail, the idea with by-need is that there can be non-trivial work to reduce a term to an actionable value when you 'let' something, and you want to delay doing that work until you need it, but only do it once. Similarly, when you capture a continuation, there might be non-trivial work to reduce it to an actionable co-value, and you similarly only want to do it once, but only if you actually jump to it. |
| 2020-10-05 22:19:17 | × | buggymcbugfix quits (sid432603@gateway/web/irccloud.com/x-fjvfxmicxyzmpfmg) (Ping timeout: 272 seconds) |
| 2020-10-05 22:19:27 | → | elvishjerricco joins (sid237756@NixOS/user/ElvishJerricco) |
| 2020-10-05 22:19:55 | × | m-renaud quits (sid333785@gateway/web/irccloud.com/x-wdhdpnuntagzspud) (Ping timeout: 272 seconds) |
| 2020-10-05 22:19:55 | × | ^[_ quits (sid43445@gateway/web/irccloud.com/x-eiyktghegavpjkto) (Ping timeout: 272 seconds) |
| 2020-10-05 22:20:01 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 2020-10-05 22:20:06 | ski | . o O ( `(getAlt .) . foldMap . (Alt .) :: (Foldable t,Alternative f) => (a -> f b) -> (t a -> f b)' ) |
| 2020-10-05 22:20:11 | × | Tops21 quits (~Tobias@dyndsl-095-033-017-021.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 2020-10-05 22:20:26 | → | buggymcbugfix joins (sid432603@gateway/web/irccloud.com/x-hmfcqscsbxxfrwjh) |
| 2020-10-05 22:20:56 | <ski> | carter : yea, it's a bit annoying, perhaps, but it seems it's what you get, for the intended application domain of session types ? (at least to a first approximation ?) |
| 2020-10-05 22:21:49 | <ski> | (note that i haven't really looked much at session types, apart from that paper relating them to linear logic .. so i might be missing some relevant stuff) |
| 2020-10-05 22:22:03 | → | ^[_ joins (sid43445@gateway/web/irccloud.com/x-jnodviuydqdnbssz) |
| 2020-10-05 22:22:20 | × | nbloomf quits (~nbloomf@2600:1700:83e0:1f40:507:9614:9e50:551c) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2020-10-05 22:22:30 | → | m-renaud joins (sid333785@gateway/web/irccloud.com/x-hxgmjbgqyiqvuvvr) |
| 2020-10-05 22:23:14 | → | moet joins (~moet@mobile-166-170-41-37.mycingular.net) |
| 2020-10-05 22:23:43 | × | noan quits (~noan@2604:a880:400:d0::12fc:5001) (Ping timeout: 272 seconds) |
| 2020-10-05 22:24:06 | × | DavidEichmann quits (~david@43.240.198.146.dyn.plus.net) (Ping timeout: 258 seconds) |
| 2020-10-05 22:24:07 | <moet> | is it better to have a "search & extract" function like `(a -> Bool) -> [a] -> Maybe ([a], a)` or like `(a -> Bool) -> [a] -> ([a], Maybe a)` ? |
| 2020-10-05 22:24:20 | → | Sgeo_ joins (~Sgeo@ool-18b982ad.dyn.optonline.net) |
| 2020-10-05 22:24:43 | <koz_> | moet: I guess this finds (possibly) the first satisfying item, and the rest? |
| 2020-10-05 22:24:43 | <moet> | i tend to prefer the former `Maybe ([a], a)` because it communicates that there's no need to update the list in it's containing data structure because no result was found |
| 2020-10-05 22:24:49 | → | noan joins (~noan@2604:a880:400:d0::12fc:5001) |
| 2020-10-05 22:24:50 | <koz_> | What happens if there's more than one? |
| 2020-10-05 22:24:59 | × | no-n quits (sid257727@gateway/web/irccloud.com/x-rjqspinjxdvineod) (Ping timeout: 272 seconds) |
| 2020-10-05 22:24:59 | × | AndreasK quits (sid320732@gateway/web/irccloud.com/x-degmzwhevcbnxqim) (Ping timeout: 272 seconds) |
| 2020-10-05 22:25:24 | <ski> | moet : assuming i understand the context correctly, i'd go for the former, probably |
| 2020-10-05 22:25:34 | → | snakemasterflex joins (~snakemast@213.100.206.23) |
| 2020-10-05 22:25:37 | × | carter quits (sid14827@gateway/web/irccloud.com/x-qxwtkltudlralpiz) (Ping timeout: 272 seconds) |
| 2020-10-05 22:25:58 | <ski> | it seems less common to want to remove an element, if present, and separately get a notification whether an element was removed |
| 2020-10-05 22:25:58 | <moet> | koz_: yes, it finds the first and returns the list with that item removed .. eg `searchExtract (=='l') "hello" == Just ("helo", 'l')` |
| 2020-10-05 22:26:05 | <koz_> | Ah. |
All times are in UTC.