Logs: freenode/#haskell
| 2020-10-05 22:26:06 | <moet> | koz_: if there's more than one, they're left in the list |
| 2020-10-05 22:26:07 | <dolio> | carter: I'm not sure what a great example is. The one that comes to mind is: when you capture a continuation that does some lets to build (by-need) closures after it's called, those closures should not be built for each invocation of the continuation. |
| 2020-10-05 22:26:28 | → | carter joins (sid14827@gateway/web/irccloud.com/x-sizpssbboxwjlzfn) |
| 2020-10-05 22:26:30 | × | xff0x quits (~fox@2001:1a81:5300:fe00:1175:d8f5:8ada:f855) (Quit: xff0x) |
| 2020-10-05 22:26:30 | <ski> | usually, i think, one'd want to explicitly tell how to continue with the list, if the item was not present |
| 2020-10-05 22:26:30 | <dolio> | Only once, if possible, and shared. |
| 2020-10-05 22:26:59 | → | no-n joins (sid257727@gateway/web/irccloud.com/x-njvyzrpfdtdezqbh) |
| 2020-10-05 22:27:01 | → | AndreasK joins (sid320732@gateway/web/irccloud.com/x-hkkwdrhutkwmrhne) |
| 2020-10-05 22:27:11 | <ski> | dolio : maybe some `shift'&`reset' example ? |
| 2020-10-05 22:27:33 | × | Sgeo quits (~Sgeo@ool-18b982ad.dyn.optonline.net) (Ping timeout: 258 seconds) |
| 2020-10-05 22:27:55 | <moet> | ski: so if i'm understanding you correctly, you agree with what i said above about preferring `Maybe ([a], a)` because it's less ambiguous in meaning than `([a], Maybe a)`? |
| 2020-10-05 22:27:56 | × | machinedgod quits (~machinedg@142.169.78.240) (Ping timeout: 258 seconds) |
| 2020-10-05 22:28:17 | <dolio> | Maybe. I have trouble of thinking of good 'doing computation to determine the continuation' examples because that's basically something you can't do in most type theory. |
| 2020-10-05 22:28:22 | <ski> | (there's some paper on normalization-by-evaluation, which has a `reflect' operation that uses `shift' on sum types, to evaluate both branches, iirc .. hmm) |
| 2020-10-05 22:29:25 | × | ghuntley quits (sid16877@gateway/web/irccloud.com/x-jwzkcgtobgufetir) (Ping timeout: 272 seconds) |
| 2020-10-05 22:29:25 | × | pent quits (sid313808@gateway/web/irccloud.com/x-mbwahawoqthelmme) (Ping timeout: 272 seconds) |
| 2020-10-05 22:29:33 | <carter> | ski: i specfically think that the session types approach to linar logica was the biggest barrier to people understanding linear logic and relating it to functional programming |
| 2020-10-05 22:29:35 | → | ghuntley joins (sid16877@gateway/web/irccloud.com/x-hazckpioupzucowz) |
| 2020-10-05 22:29:40 | <ski> | moet : yes, the latter would allow/encourage continuing using the list (whether an element was removed or not), and perhaps later checking the removal status of the other part. if that was a common pattern one'd want to support, i'd probably go with the latter alternative (or maybe support both) |
| 2020-10-05 22:29:52 | × | snakemasterflex quits (~snakemast@213.100.206.23) (Ping timeout: 246 seconds) |
| 2020-10-05 22:30:03 | × | JSharp quits (sid4580@wikia/JSharp) (Ping timeout: 272 seconds) |
| 2020-10-05 22:30:24 | <ski> | moet : but if it's not a likely situation (to reasonably be in), i'd go with the former, to reduce risk of bugs due to not being forced to upfront check the status |
| 2020-10-05 22:30:25 | × | cosimone quits (~user@2001:b07:ae5:db26:f68c:50ff:fe0b:b774) (Ping timeout: 240 seconds) |
| 2020-10-05 22:30:31 | → | pent joins (sid313808@gateway/web/irccloud.com/x-lsufgbovmcuefoiy) |
| 2020-10-05 22:30:53 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-05 22:31:57 | × | cemerick quits (sid54985@gateway/web/irccloud.com/x-ongnogrqassjmkgm) (Ping timeout: 272 seconds) |
| 2020-10-05 22:32:22 | → | JSharp joins (sid4580@wikia/JSharp) |
| 2020-10-05 22:32:29 | → | cemerick joins (sid54985@gateway/web/irccloud.com/x-ticsgvtoxvknnlzm) |
| 2020-10-05 22:32:30 | <ski> | carter : oh, that might be so. i haven't heard of many people trying to understand linear logic (or even functional programming), coming from a session types perspective. i learned linear logic long before i heard of session types |
| 2020-10-05 22:32:57 | <carter> | How’d you manage that? |
| 2020-10-05 22:33:13 | <ski> | dolio : hm, elaborate on "doing computation to determine the continuation" ? |
| 2020-10-05 22:33:22 | × | polyrain quits (~polyrain@2001:8003:e501:6901:a41a:145a:3fce:c107) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2020-10-05 22:33:54 | <carter> | dolio: this is the co-need bit? the paper kinda talks about it |
| 2020-10-05 22:34:08 | <carter> | "control effectful cbv but more efficient for weird programs" |
| 2020-10-05 22:34:12 | → | polyrain joins (~polyrain@2001:8003:e501:6901:a41a:145a:3fce:c107) |
| 2020-10-05 22:34:12 | <ski> | carter : i dunno. i'm not sure how long session types have been a thing (i heard of them, less than ten years ago, i think). but i was reading lots of papers on various logics and type systems, and encountered linear logic that way |
| 2020-10-05 22:34:21 | <carter> | cool |
| 2020-10-05 22:34:48 | <carter> | by volume, most linear lgoic stuff in the last 20 years seems to either be in small boring fragments, or session types |
| 2020-10-05 22:34:51 | <carter> | until the past 2-5 years |
| 2020-10-05 22:34:59 | <ski> | carter : let's enable more weird programs, heh ;) |
| 2020-10-05 22:36:15 | × | moet quits (~moet@mobile-166-170-41-37.mycingular.net) (Quit: leaving) |
| 2020-10-05 22:37:13 | <dolio> | carter: Yeah. |
| 2020-10-05 22:37:31 | <carter> | dolio: wrt co-need or wrt linear logic? |
| 2020-10-05 22:37:41 | <carter> | https://ix.cs.uoregon.edu/~pdownen/presentations/beyond-polarity.pdf maybe this presentation by the author has stuff |
| 2020-10-05 22:37:43 | <carter> | skimming atm |
| 2020-10-05 22:38:02 | <ski> | a tail-recursive function (definition) is one that passes the same continuation (for output) to the recursive calls. how would a "head-recursive function (definition)", being one that passes the same value (for input) to the recursive calls, work ? |
| 2020-10-05 22:38:18 | <carter> | ski: ??? |
| 2020-10-05 22:38:22 | × | chaosmasttter quits (~chaosmast@p200300c4a73b2e0100f3c5a701cd6e56.dip0.t-ipconnect.de) (Quit: WeeChat 2.9) |
| 2020-10-05 22:38:22 | <dolio> | ski, carter: I think another example is: if the continuation starts by doing case analysis on a sum type that is closed over by the continuation, you should just reduce that out of the continuation the first time you go through it, and memoize the result. |
| 2020-10-05 22:38:25 | <carter> | co deta? |
| 2020-10-05 22:38:35 | <ski> | ah, i suppose this is related to "message-dispatching syntax" (aka "copattern syntax") (i was thinking that before, but didn't mention) |
| 2020-10-05 22:38:46 | <dolio> | carter: co-need. |
| 2020-10-05 22:39:10 | atk | is now known as nil |
| 2020-10-05 22:39:18 | <ski> | dolio : what's the dual situation to that ? |
| 2020-10-05 22:39:21 | <carter> | i dont like the up/down shift notations in this |
| 2020-10-05 22:39:23 | × | nil quits (~Arch-TK@ircpuzzles/staff/Arch-TK) (Disconnected by services) |
| 2020-10-05 22:39:26 | <carter> | in these papers |
| 2020-10-05 22:39:27 | <carter> | hard to read |
| 2020-10-05 22:40:03 | <dolio> | ski: The first time you evaluate a lazy let function call, you should remember the value it produces. |
| 2020-10-05 22:40:06 | → | atk joins (~Arch-TK@ircpuzzles/staff/Arch-TK) |
| 2020-10-05 22:40:38 | → | argent0 joins (~argent0@168.227.97.5) |
| 2020-10-05 22:40:44 | × | jwynn6 quits (~jwynn6@050-088-122-078.res.spectrum.com) (Ping timeout: 256 seconds) |
| 2020-10-05 22:41:12 | <ski> | carter : if you consider `shunt [] ys = ys; shunt (x:xs) ys = shunt xs (x:ys)' (for `reverse xs = shunt xs []'), then it inspects information in its input value (putting stuff into the accumulator), and continues looping with the same continuation (only actually used in the base casr) |
| 2020-10-05 22:41:28 | <carter> | whats this about? |
| 2020-10-05 22:42:00 | <ski> | carter : for a "head-recursive" definition, you'd pass the same input parameter `v' to the recursive call as you got in the current call. but instead, you'd extract information, by inspecting your continuation (which would change across recursive calls) |
| 2020-10-05 22:42:11 | <argent0> | Hi, what does `do ...; let foo bar = cat <$> dog <*> aniamal` means? |
| 2020-10-05 22:42:11 | <carter> | are you just talking about coinductive |
| 2020-10-05 22:42:27 | <argent0> | I ask about the `foo bar` part? |
| 2020-10-05 22:42:50 | <ski> | i was wondering if one could relate this to what dolio mentioned about "doing computation to determine the continuation" |
| 2020-10-05 22:43:00 | <monochrom> | <$> is fmap, from the Functor class. <*> is from the Applicative class. |
| 2020-10-05 22:43:04 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:71a4:5e3f:3433:7ae1) |
| 2020-10-05 22:43:18 | <ski> | dolio : "a lazy let function call" ? |
| 2020-10-05 22:43:33 | <monochrom> | This is obviously very abstract and unnecessarily general. But this is how much information is possible from the question. |
| 2020-10-05 22:43:45 | <argent0> | monochrom: yes but how does the `foo bar` part matches |
| 2020-10-05 22:43:55 | × | mav1 quits (~mav@p5dee344b.dip0.t-ipconnect.de) (Quit: WeeChat 2.9) |
| 2020-10-05 22:44:02 | <monochrom> | foo is a function name, bar is an argument name. |
| 2020-10-05 22:44:23 | <monochrom> | This is defining the function "foo". |
| 2020-10-05 22:44:24 | × | dminuoso quits (~dminuoso@unaffiliated/dminuoso) (Quit: ZNC 1.6.6+deb1ubuntu0.1 - http://znc.in) |
| 2020-10-05 22:44:33 | <argent0> | monochrom: ok, thanks |
| 2020-10-05 22:44:48 | <ski> | argent0 : if `cat :: I (Dog -> Animal -> Farm)', and `dog :: I Dog',`animal :: I Animal', then `cat <$> dog <*> animal :: I Farm', where `I' is some idiom (an instance of `Applicative') |
| 2020-10-05 22:44:49 | argent0 | :-P |
| 2020-10-05 22:45:04 | × | LKoen quits (~LKoen@81.255.219.130) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 2020-10-05 22:45:21 | <argent0> | ski: thanks I get it now |
| 2020-10-05 22:45:58 | <ski> | (er, sorry. that should be just `cat :: Dog -> Animal -> Farm'. if you had used `cat <*> dog <*> aniamal', then it would have been as i said above) |
| 2020-10-05 22:45:59 | → | Andre4 joins (~Andrea@p5de77723.dip0.t-ipconnect.de) |
| 2020-10-05 22:47:19 | <ski> | carter : "are you just talking about coinductive" -- more or less. thinking about how to relate it to the other topic here. have you seen "message-dispatching syntax" (perhaps read the "copatterns" paper) ? |
| 2020-10-05 22:47:35 | <carter> | copatterns are fun |
| 2020-10-05 22:47:51 | <ski> | indeed |
| 2020-10-05 22:47:54 | <carter> | ski: did you see my thing about how to fake copatterns in haskell on reddit a few years ago |
| 2020-10-05 22:48:04 | <ski> | hm, i don't recall so ? |
| 2020-10-05 22:48:15 | <ski> | @where ErikPoll |
| 2020-10-05 22:48:15 | <lambdabot> | "Subtyping and Inheritance for Inductive Types" in 1997 at <http://www.cs.ru.nl/E.Poll/papers/durham97.pdf>,"Subtyping and Inheritance for Categorical Datatypes" in 1997 at <http://www.cs.ru.nl/E. |
| 2020-10-05 22:48:15 | <lambdabot> | Poll/papers/kyoto97.pdf>,"A Coalgebraic Semantics of Subtyping" in 2000 at <http://www.cs.ru.nl/E.Poll/papers/cmcs00.pdf>,later version of that in 2001 at <http://www.cs.ru.nl/E.Poll/papers/ita01. |
| 2020-10-05 22:48:15 | <lambdabot> | pdf> |
| 2020-10-05 22:48:55 | <dolio> | ski: `let y = f x` is naming (y) a computation that matches up closed-over variables in a par redex that might do non-trivial amounts of work before reducing to a value. So call-by-need says that when you want its value, you should do the work and remember the value. |
| 2020-10-05 22:49:00 | <carter> | https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/ ski |
| 2020-10-05 22:49:27 | <ski> | the first two of these papers, are where i first saw the idea (which i called "message-dispatching syntax", since it seemed to obviously correspond to definitions of how objects respond to messages (by giving method implementations), in OO) |
| 2020-10-05 22:49:49 | <dolio> | Instead of re-doing the redex every time (call-by-name). |
| 2020-10-05 22:50:15 | <carter> | dolio: aka its saying "continuations are cbn normally in cbv languages" |
| 2020-10-05 22:51:54 | <dolio> | Something like that. |
All times are in UTC.