Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 448 449 450 451 452 453 454 455 456 457 458 .. 5022
— 502,152 events total
2020-10-05 23:25:09 <ski> (at first i was wondering why ⌜¬x⌝ had type ⌜k⌝ ..)
2020-10-05 23:25:09 → notzmv joins (~user@177.45.26.174)
2020-10-05 23:25:13 → pacak joins (~pacak@bb116-14-220-91.singnet.com.sg)
2020-10-05 23:25:23 <dolio> Oh, sorry.
2020-10-05 23:25:25 notzmv is now known as Guest43030
2020-10-05 23:26:05 × dminuoso quits (~dminuoso@unaffiliated/dminuoso) (Quit: ZNC 1.7.5 - https://znc.in)
2020-10-05 23:26:13 <dolio> I should say, that's what a function continuation value is. Or a co-value.
2020-10-05 23:26:21 → dminuoso joins (~dminuoso@unaffiliated/dminuoso)
2020-10-05 23:26:47 Guest43030 is now known as zmv
2020-10-05 23:26:51 × zmv quits (~user@177.45.26.174) (Changing host)
2020-10-05 23:26:51 → zmv joins (~user@unaffiliated/zmv)
2020-10-05 23:26:58 <dolio> You could also put a 'let' in there to do more stuff.
2020-10-05 23:26:58 zmv is now known as notzmv
2020-10-05 23:30:30 <argent0> :q
2020-10-05 23:30:46 <ski> Γ ⊢ x : A | Δ
2020-10-05 23:30:51 <ski> ────────────────
2020-10-05 23:30:55 <ski> Γ , ¬x : ¬ A ⊢ Δ Γ | k : B ⊢ Δ
2020-10-05 23:30:59 <ski> ────────────────────────────────
2020-10-05 23:31:02 <ski> Γ | ¬x::k : A → B ⊢ Δ
2020-10-05 23:31:25 × Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Ping timeout: 240 seconds)
2020-10-05 23:31:54 × pacak quits (~pacak@bb116-14-220-91.singnet.com.sg) (Remote host closed the connection)
2020-10-05 23:32:04 <dolio> Yeah.
2020-10-05 23:32:17 → pacak joins (~pacak@bb116-14-220-91.singnet.com.sg)
2020-10-05 23:32:36 <ski> Γ ⊢ f : A → B ⊢ Δ Γ | ¬x::k : A → B ⊢ Δ
2020-10-05 23:32:41 <ski> ─────────────────────────────────────────
2020-10-05 23:32:44 <ski> Γ ⊢{ ⟨f|¬x:k⟩ } Δ
2020-10-05 23:34:15 <dolio> Yeah, with one of the ⊢ replaced with a |.
2020-10-05 23:34:36 <ski> er, yes
2020-10-05 23:34:48 → conal joins (~conal@64.71.133.70)
2020-10-05 23:34:55 <ski> should have been ⌜Γ ⊢ f : A → B | Δ⌝
2020-10-05 23:35:01 <dolio> Right.
2020-10-05 23:35:45 <dolio> And for a genuine β redex we'ere imagining f = λ[¬x::k] <...>
2020-10-05 23:37:13 <dolio> So it's a value cut with a covalue.
2020-10-05 23:37:18 <ski> Γ ⊢{ ⟨f|¬x:k⟩ } Δ
2020-10-05 23:37:22 <ski> ───────────────────────────────────
2020-10-05 23:37:26 <ski> Γ ⊢ ξ k. ⟨f|¬x:k⟩ : B | Δ ∸ (k : B)
2020-10-05 23:37:31 <ski> and then cut with the other one
2020-10-05 23:38:07 <ski> (i should have included ⌜k : B⌝ in ⌜Δ⌝, for the ⌜¬x::k⌝ derivation, above)
2020-10-05 23:38:15 <dolio> Oh, you never put k in the context.
2020-10-05 23:38:18 <dolio> Yeah.
2020-10-05 23:38:25 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-05 23:39:28 <ski> hm, so we have a "critical pair"
2020-10-05 23:39:44 <ski> each one side wanting to override the other one
2020-10-05 23:40:23 <dolio> Yeah, so you need an evaluation strategy to decide what happens.
2020-10-05 23:40:35 <ski> mm
2020-10-05 23:40:47 <ski> i'm not seeing where by-need ties into this, atm, though
2020-10-05 23:44:18 <ski> <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 23:44:22 <ski> <dolio> ski: The first time you evaluate a lazy let function call, you should remember the value it produces.
2020-10-05 23:44:31 <ski> <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 23:44:42 <ski> (backtracking back to these now)
2020-10-05 23:45:14 <dolio> Suppose `let` wins, B is by-name, and y occurs multiple times. Then the beta reduction happens twice, because we duplicate the whole term (I think).
2020-10-05 23:45:37 <ski> "a sum type that is closed over by the continuation", would that be ⌜y⌝, above ?
2020-10-05 23:46:45 <dolio> No, that would be the dual case.
2020-10-05 23:47:09 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-05 23:47:25 × inkbottle quits (~inkbottle@aaubervilliers-654-1-101-245.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!)
2020-10-05 23:47:25 × falafel quits (~falafel@2605:e000:1527:d491:99fe:5613:f0a7:56f0) (Ping timeout: 240 seconds)
2020-10-05 23:47:32 <ski> Γ ⊢ ξ k. ⟨f|¬x::k⟩ : B | Δ ∸ (k : B) Γ | let y. ⋯y⋯ : B ⊢ Δ
2020-10-05 23:47:35 <ski> ─────────────────────────────────────────────────────────────
2020-10-05 23:47:39 <ski> Γ ⊢{ ⟨ξ k. ⟨f|¬x::k⟩|let y. ⋯y⋯⟩ } Δ
2020-10-05 23:47:44 <ski> (spelling the final cut out, for easy reference)
2020-10-05 23:47:45 → inkbottle joins (~inkbottle@aaubervilliers-654-1-101-245.w86-212.abo.wanadoo.fr)
2020-10-05 23:48:38 × vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving)
2020-10-05 23:48:44 <dolio> <λ[¬x::k] ... | ¬x::k> is a par redex, <inl x | case{inl x -> ... | inr y -> ...}> is a + redex.
2020-10-05 23:48:48 → albert_91 joins (~Albert@p200300e5ff0b5b4248a33bded2872db1.dip0.t-ipconnect.de)
2020-10-05 23:48:51 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-05 23:49:23 <int-e> carter: Fine there you go
2020-10-05 23:50:20 <ski> hm, yes. in the latter, the continuation is a pair of two continuations
2020-10-05 23:50:38 <ski> (thinking about the former)
2020-10-05 23:50:59 × justache quits (~justache@unaffiliated/justache) (Ping timeout: 260 seconds)
2020-10-05 23:50:59 <dolio> Yeah, but it's a pair of continuataions that does arbitrary computation in each case.
2020-10-05 23:51:12 <ski> as opposed to ?
2020-10-05 23:51:21 <dolio> Whereas par has continuations that are well-founded trees.
2020-10-05 23:51:44 <dolio> At least, those are teh values.
2020-10-05 23:51:48 <ski> how do you mean ?
2020-10-05 23:51:55 <dolio> That 'case' is a continuation value for +.
2020-10-05 23:52:01 <ski> yes
2020-10-05 23:53:39 × albert_91 quits (~Albert@p200300e5ff0b5b4248a33bded2872db1.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
2020-10-05 23:53:46 <dolio> Well, it's not quite true once you get into all the polarity shifting. But if you work in the system without any shifts, then par is only applicable to hereditarily by-name codata types, and those have continuation values that are well-founded trees, just like data types have term values that are well-founded trees.
2020-10-05 23:53:59 → thir joins (~thir@p200300f27f0fc60038c1b16891cbfa03.dip0.t-ipconnect.de)
2020-10-05 23:54:21 <ski> hm, ok
2020-10-05 23:54:56 <dolio> Codata covalues are the tree of all the projections, data values are the tree of all the constructors.
2020-10-05 23:55:27 → machinedgod joins (~machinedg@24.105.81.50)
2020-10-05 23:55:58 <dolio> And you're only allowed to substitute (co)values for variables.
2020-10-05 23:56:07 → conal joins (~conal@64.71.133.70)
2020-10-05 23:58:25 × thir quits (~thir@p200300f27f0fc60038c1b16891cbfa03.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-10-05 23:59:36 <ski> (loking at the typing rules in the paper now .. i think i was thinking of another right rule for `par')
2020-10-06 00:00:01 × jesusabdullah quits (~jesusabdu@178.162.204.214) ()
2020-10-06 00:00:13 → justache joins (~justache@unaffiliated/justache)
2020-10-06 00:00:26 <ski> in the reductions in the first figure in the paper, are they only substituting (co)values for variables ?
2020-10-06 00:00:48 <ski> or maybe that's the initial system they start with, and want to improve on
2020-10-06 00:00:59 <dolio> I think the first figure is showing you the problem with classical logic.
2020-10-06 00:01:05 <dolio> First section, even.
2020-10-06 00:01:25 × hiroaki quits (~hiroaki@ip4d176049.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds)
2020-10-06 00:01:43 <dolio> So they can over-fix it, and then relax into something that can actually be used (kind of).
2020-10-06 00:02:13 <ski> mhm (over-fix ?)
2020-10-06 00:03:32 <dolio> Well, when everything is hereditarily by-name or by-value, you can't write some things, I think.
2020-10-06 00:04:30 <dolio> You can't put a function value in an either.
2020-10-06 00:05:28 <ski> hm, so some escaping from / explicit switching of polarity, i suppose
2020-10-06 00:05:44 <dolio> Yeah.
2020-10-06 00:08:09 × xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 256 seconds)
←Prev  Next→
Page 1 .. 448 449 450 451 452 453 454 455 456 457 458 .. 5022

All times are in UTC.