Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 447 448 449 450 451 452 453 454 455 456 457 .. 5022
— 502,152 events total
2020-10-05 22:52:00 <Andre4> is the St Monad ( Data.STRef, DataArrayST) impure, is this monoad magic, like IO ?
2020-10-05 22:52:06 <ski> carter : ah, cool :) .. you're emulating a record as a function taking a tag (in this case a `GADT' tag)
2020-10-05 22:52:44 <dolio> carter: Like, they just grab the stack, and run back through it verbatim every time. They don't optimize it on the first time through.
2020-10-05 22:52:51 × danvet_ quits (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) (Ping timeout: 272 seconds)
2020-10-05 22:53:12 <carter> dolio: ohhh, it makes more sense when explained that way
2020-10-05 22:53:18 <carter> call CC is terrible for exposition
2020-10-05 22:53:21 <carter> CPS makes more sense to me
2020-10-05 22:53:22 <carter> :)
2020-10-05 22:53:37 <carter> dolio: would this allow a faster logicT mmonad? :)
2020-10-05 22:53:55 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:71a4:5e3f:3433:7ae1) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-05 22:54:27 hackage ivar-simple 0.3.3 - Write once concurrency primitives. https://hackage.haskell.org/package/ivar-simple-0.3.3 (BertramFelgenhauer)
2020-10-05 22:55:02 <dolio> Hah. I don't know. I barely understand this paper.
2020-10-05 22:55:20 <ski> carter : reminds me of a trick to represent `data Expr where Let :: [Decl] -> Expr -> Expr; data Decl where Def :: Ident -> [Ident] -> Expr -> Decl' as `data Tag = E | D; data AST :: Tag -> * where Let :: [AST D] -> ADT E -> AST E; Def :: Ident -> [Ident] -> AST E -> AST D'
2020-10-05 22:55:23 <int-e> ski: ^^new release
2020-10-05 22:55:23 <carter> Yeah. It found it a bit hard to read
2020-10-05 22:55:59 <int-e> (it's even simpler now; writeIVar is just a putMVar, the way it was originally intended)
2020-10-05 22:56:02 → dminuoso joins (~dminuoso@unaffiliated/dminuoso)
2020-10-05 22:56:02 <carter> int-e: I cooked up a fun idea for an Mvar variant when helping viktor debug some fun perf issues
2020-10-05 22:56:10 <ski> carter : the point is that if one wants to do explicit fixpoints, we can encode a type-level tuple/record as a type function from `Tag'
2020-10-05 22:56:35 <carter> https://gitlab.haskell.org/ghc/ghc/-/issues/18798
2020-10-05 22:57:01 <carter> ski: I’m middle of eating. So not 100% atm
2020-10-05 22:57:02 → mav1 joins (~mav@p5dee344b.dip0.t-ipconnect.de)
2020-10-05 22:58:11 <ski> dolio : hm, not seeing how it relates to `par'
2020-10-05 22:58:28 <dolio> function calls are par.
2020-10-05 22:59:15 <ski> Andre4 : neither `ST' nor `IO' are impure. but both are "magic", in the sense that they have direct support by the implementation. (they aren't defined totally in Haskell source code)
2020-10-05 22:59:27 <dolio> I'd have to think a while how to actually write that 'let' thing. :)
2020-10-05 22:59:35 <ski> (similarly to how `Integer',`Int',`Double',`(->)' are also "magic", or "primitive", in the same sense)
2020-10-05 22:59:51 → tv- joins (~tv@unaffiliated/tv-)
2020-10-05 23:01:02 × alx741 quits (~alx741@186.178.110.22) (Quit: alx741)
2020-10-05 23:02:07 × albert_91 quits (~Albert@p200300e5ff0b5b4248a33bded2872db1.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-10-05 23:02:11 <carter> dolio: more you can encode functions in par
2020-10-05 23:02:11 <Andre4> aki: in the source code from Stref some foreign statements are included
2020-10-05 23:02:57 × falafel quits (~falafel@2605:e000:1527:d491:99fe:5613:f0a7:56f0) (Remote host closed the connection)
2020-10-05 23:03:23 → falafel joins (~falafel@2605:e000:1527:d491:99fe:5613:f0a7:56f0)
2020-10-05 23:04:30 <Andre4> ski: does stref, or arrayst work together with laty evaluation ?
2020-10-05 23:04:42 × Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 260 seconds)
2020-10-05 23:04:45 <Andre4> lazy evaluation
2020-10-05 23:05:12 → Axman6 joins (~Axman6@pdpc/supporter/student/Axman6)
2020-10-05 23:05:20 × mav1 quits (~mav@p5dee344b.dip0.t-ipconnect.de) (Quit: WeeChat 2.9)
2020-10-05 23:06:11 <dolio> ski: Something like this, maybe: <shift k. <f|¬x:k> | let y. ...>
2020-10-05 23:06:26 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2020-10-05 23:06:27 <ski> int-e : nice :D
2020-10-05 23:07:30 × oisdk quits (~oisdk@2001:bb6:3329:d100:e56d:4357:c75:2f61) (Quit: oisdk)
2020-10-05 23:08:04 <dolio> How to reduce that is ambiguous, though, and I left out all the polarity shifting that makes it deterministic. :)
2020-10-05 23:08:13 × m0rphism quits (~m0rphism@HSI-KBW-046-005-177-122.hsi8.kabel-badenwuerttemberg.de) (Ping timeout: 260 seconds)
2020-10-05 23:08:16 × entkme^ quits (entkme@ip98-184-89-2.mc.at.cox.net) ()
2020-10-05 23:08:16 <ski> dolio : hm, yes. but for some reason, i thought you were thinking about constructing a `par', behind the scenes, in some way there
2020-10-05 23:08:52 → alx741 joins (~alx741@186.178.110.22)
2020-10-05 23:09:31 → tsrt^ joins (tsrt@ip98-184-89-2.mc.at.cox.net)
2020-10-05 23:09:37 × Andre4 quits (~Andrea@p5de77723.dip0.t-ipconnect.de) (Quit: Leaving)
2020-10-05 23:09:38 <dolio> I guess you should imagine that f is actually a lambda term.
2020-10-05 23:09:44 <dolio> To be analogous to a case statement.
2020-10-05 23:10:16 <ski> Andre4 : yes, they don't force the values stored inside the mutable cells. however, `Control.Monad.ST' is strict in the state (the collection of `STRef's and `STArray's) that it carries around. if you want laziness there, try `Control.Monad.ST.Lazy' (i'd link you to some fun examples by monochrom here, but alas, the paste service they were on is no more ..)
2020-10-05 23:10:30 <dolio> Then it's a β redex.
2020-10-05 23:10:54 × polyrain quits (~polyrain@2001:8003:e501:6901:a41a:145a:3fce:c107) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-05 23:11:16 <ski> dolio : how should i parse `<.. | ..>' ? creating a `par' ?
2020-10-05 23:11:25 × thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 240 seconds)
2020-10-05 23:11:54 <dolio> No, <...|...> is cut.
2020-10-05 23:12:15 <dolio> cut a term with a coterm.
2020-10-05 23:12:23 <ski> ah, i was just thinking it could be that
2020-10-05 23:12:54 <dolio> Anyhow, `shift` can capture a β redex for a sum in a continuation, dually to this.
2020-10-05 23:13:11 × dminuoso quits (~dminuoso@unaffiliated/dminuoso) (Quit: ZNC 1.7.5 - https://znc.in)
2020-10-05 23:13:19 <ski> (still pondering how to parse it, though)
2020-10-05 23:13:36 → massma joins (~user@dyn-160-39-62-152.dyn.columbia.edu)
2020-10-05 23:14:14 <dolio> Haha. <(shift k. <f|¬x:k>) | (let y. ...)>
2020-10-05 23:14:28 <ski> what's the type of either side of the jump `<shift k. <f|¬x:k> | let y. ...>' ?
2020-10-05 23:14:41 <ski> (yes, i took that bracketting for granted)
2020-10-05 23:14:48 <dolio> 'let' is supposed to capture the term it's cut with in the variable (y). 'shift' captures the continuation it's cut with in `k`.
2020-10-05 23:14:57 <ski> how does it correspond to `let y = f x in ...' ?
2020-10-05 23:15:06 <ski> (is it the same `...' in both ?)
2020-10-05 23:16:35 <ski> hm, ok, so `let y. ...' is a continuation, then
2020-10-05 23:16:42 <dolio> Yeah.
2020-10-05 23:16:48 → dminuoso joins (~dminuoso@unaffiliated/dminuoso)
2020-10-05 23:17:01 <ski> (and that `...' is another jump)
2020-10-05 23:17:09 <dolio> It's a continuation that captures the term it's cut with and runs a computation in an extended environment.
2020-10-05 23:17:18 <ski> yes
2020-10-05 23:17:25 × raehik quits (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
2020-10-05 23:17:47 <dolio> To make a value version of the let might require another shift or something.
2020-10-05 23:18:12 × GyroW_ quits (~GyroW@unaffiliated/gyrow) (Quit: Someone ate my pie)
2020-10-05 23:18:22 → GyroW joins (~GyroW@d54c03e98.access.telenet.be)
2020-10-05 23:18:23 × GyroW quits (~GyroW@d54c03e98.access.telenet.be) (Changing host)
2020-10-05 23:18:23 → GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-05 23:18:28 → polyrain joins (~polyrain@2001:8003:e501:6901:a41a:145a:3fce:c107)
2020-10-05 23:21:32 <int-e> carter: looks risky... I'd think that marking the MVar as dirty is as much about the list of waiters (which, if you block on an MVar, contains an item in the youngest generation) as it is about the value.
2020-10-05 23:21:52 <ski> Γ , y : B ⊢{ ⋯y⋯ } Δ
2020-10-05 23:21:55 <ski> ──────────────────────
2020-10-05 23:21:58 <ski> Γ | let y. ⋯y⋯ : B ⊢ Δ
2020-10-05 23:22:03 <ski> something like that
2020-10-05 23:22:16 × tv- quits (~tv@unaffiliated/tv-) (Quit: WeeChat 2.8)
2020-10-05 23:22:17 <dolio> Yeah, I think so.
2020-10-05 23:22:37 → tv- joins (~tv@unaffiliated/tv-)
2020-10-05 23:22:59 <carter> ohh
2020-10-05 23:23:03 <carter> int-e: comment on that plz :)
2020-10-05 23:23:13 <ski> and ⌜¬x:k⌝ is a "calling context" of a called function, yes ?
2020-10-05 23:23:27 × notzmv quits (~user@unaffiliated/zmv) (Read error: Connection reset by peer)
2020-10-05 23:23:50 <dolio> Yeah. A function continuation is an argument pushed on the return continuation.
2020-10-05 23:23:57 <ski> right
2020-10-05 23:24:20 <ski> (oh, that's why you used ⌜:⌝, since you're thinking of the continuation as a stack you're pushing things on)
2020-10-05 23:24:53 × pacak quits (~pacak@bb116-14-220-91.singnet.com.sg) (Remote host closed the connection)
2020-10-05 23:24:56 <int-e> carter: you sure know how to put the "labor" into elaborate :P
←Prev  Next→
Page 1 .. 447 448 449 450 451 452 453 454 455 456 457 .. 5022

All times are in UTC.