Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 10 11 12 13 14 15 16 17 18 19 20 .. 5022
— 502,152 events total
2020-09-17 05:06:18 <davean> Usually if you're writing your own monad though not composing MTL you're doing something "interesting" that would get reused elsewhere.
2020-09-17 05:06:27 <davean> Not always but its a good predictor
2020-09-17 05:07:02 <davean> siraben: I'd say usually you write your own when you care about semantics, not capabilities, but thats not well defined.
2020-09-17 05:07:35 × exodrifter quits (adacad5d@cpe-173-172-173-93.tx.res.rr.com) (Remote host closed the connection)
2020-09-17 05:08:26 × isovector1 quits (~isovector@172.103.216.166.cable.tpia.cipherkey.com) (Quit: Leaving)
2020-09-17 05:09:09 → asan joins (~yan4138@124.78.5.33)
2020-09-17 05:09:46 <davean> siraben: did that make sense?
2020-09-17 05:10:05 <siraben> davean: what do you mean by capabilities?
2020-09-17 05:10:28 <davean> "Get access to Disk" "Ask about a value"
2020-09-17 05:10:30 × nan` quits (~nan`@unaffiliated/nan/x-5405850) (Ping timeout: 260 seconds)
2020-09-17 05:10:54 <siraben> Ah, I see.
2020-09-17 05:11:01 → jedws joins (~jedws@101.184.189.58)
2020-09-17 05:11:05 <siraben> And semantics here as in PL semantics?
2020-09-17 05:11:10 → Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362)
2020-09-17 05:11:21 <davean> semantics: "Do monadic things sequentually, but applicative things on a thread pool of a given size"
2020-09-17 05:11:37 × Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 264 seconds)
2020-09-17 05:12:12 <davean> yah, semantics are about how you do the computation
2020-09-17 05:12:29 <davean> hence PlanT as an example
2020-09-17 05:12:32 Lord_of_Life_ is now known as Lord_of_Life
2020-09-17 05:12:42 <davean> topos: slap me around and say something a little tighter?
2020-09-17 05:13:20 topos slaps davean
2020-09-17 05:13:23 <topos> something a little tighter
2020-09-17 05:13:42 <davean> Cont is the exception
2020-09-17 05:13:46 <davean> that does anything, badly.
2020-09-17 05:14:12 × mmohammadi9812 quits (~mmohammad@5.116.223.123) (Ping timeout: 256 seconds)
2020-09-17 05:14:25 → rapskalian joins (~user@2601:804:8400:5750:6d07:cb01:64a9:36bb)
2020-09-17 05:14:40 <siraben> One issue I've had with effects was trying to convert my Scheme interpreter to a monadic version
2020-09-17 05:14:41 <siraben> https://github.com/siraben/r5rs-denot/blob/fba3b49d88c6d7c4e7a2cff302589a669a4fdb88/src/SchemeEval.hs#L10
2020-09-17 05:15:01 × Foritus quits (~buggery@cpc91334-watf11-2-0-cust153.15-2.cable.virginm.net) (Read error: Connection reset by peer)
2020-09-17 05:15:22 × Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-55-157-9.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
2020-09-17 05:15:39 → Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-55-157-9.dhcp-dynamic.fibreop.nb.bellaliant.net)
2020-09-17 05:15:44 <siraben> I tried something like, Except over Reader over Cont over State, but the Except <> Cont interaction didn't work out
2020-09-17 05:16:06 <siraben> In a sense I don't want Haskell's full range of continuations, just the Scheme continuations, if that makes sense
2020-09-17 05:16:06 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds)
2020-09-17 05:16:07 → dansho joins (~dansho@ip68-108-167-185.lv.lv.cox.net)
2020-09-17 05:16:20 <davean> siraben: That sure is a scheme interpriter that reads like scheme!
2020-09-17 05:16:47 <siraben> davean: Heh, it was converted directly from the denotational semantics of R5RS
2020-09-17 05:16:59 <davean> I ... could have guessed
2020-09-17 05:17:20 → Foritus joins (~buggery@cpc91334-watf11-2-0-cust153.15-2.cable.virginm.net)
2020-09-17 05:18:12 <siraben> Maybe it was someone here who mentioned that they were working a similar project and was planning to encapsulate primitive operations in a typeclass
2020-09-17 05:18:35 <siraben> Like a CSEK machine.
2020-09-17 05:18:37 <siraben> CESK*
2020-09-17 05:19:11 × __Joker quits (~Joker@180.151.106.108) (Ping timeout: 272 seconds)
2020-09-17 05:19:49 × rapskalian quits (~user@2601:804:8400:5750:6d07:cb01:64a9:36bb) (Ping timeout: 272 seconds)
2020-09-17 05:20:11 <siraben> Hm, http://matt.might.net/articles/cesk-machines/
2020-09-17 05:20:48 <topos> i mean, edwardk's been doing some of that with his livestreaming. I'm working on a machine based on matt might's abstract abstract interpreters work as well
2020-09-17 05:20:51 → justanotheruser joins (~justanoth@unaffiliated/justanotheruser)
2020-09-17 05:21:00 <edwardk> i need to stream again
2020-09-17 05:21:12 <siraben> edwardk: streaming on twitch?
2020-09-17 05:21:39 × elliott_ quits (~elliott@pool-71-114-77-65.washdc.fios.verizon.net) (Quit: WeeChat 2.9)
2020-09-17 05:21:58 <edwardk> yeah, i moved and never bothered to get set back up
2020-09-17 05:22:17 <siraben> topos: are you referring to http://matt.might.net/papers/might2010free.pdf ?
2020-09-17 05:22:19 → elliott_ joins (~elliott@pool-71-114-77-65.washdc.fios.verizon.net)
2020-09-17 05:22:47 <siraben> Wow, that circular dependence in figure 1 is exactly the issue I came across
2020-09-17 05:22:48 <topos> yeah
2020-09-17 05:23:28 <topos> but this one http://matt.might.net/papers/vanhorn2010abstract.pdf
2020-09-17 05:23:39 <topos> it's all gravy tho
2020-09-17 05:24:03 <edwardk> siraben: that interpreter is nice and direct
2020-09-17 05:24:40 <siraben> edwardk: the r5rs-denot one?
2020-09-17 05:24:53 <edwardk> capturing scheme continuations in a CESK machine is super simple. Capture K, restore K,.
2020-09-17 05:24:58 <edwardk> yeah
2020-09-17 05:25:07 <siraben> Thanks.
2020-09-17 05:26:43 × elliott_ quits (~elliott@pool-71-114-77-65.washdc.fios.verizon.net) (Client Quit)
2020-09-17 05:26:54 → eric joins (~eric@2804:431:c7d4:b75:19f7:ea85:5be8:4c8e)
2020-09-17 05:26:57 <siraben> topos: interesting paper
2020-09-17 05:27:23 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-17 05:27:41 → elliott_ joins (~elliott@pool-71-114-77-65.washdc.fios.verizon.net)
2020-09-17 05:28:01 × Guest74761 quits (sid13060@gateway/web/irccloud.com/x-rcuirdcnfpfdubdp) ()
2020-09-17 05:28:27 → dsal joins (sid13060@gateway/web/irccloud.com/x-pvmusdavojjxflwa)
2020-09-17 05:28:38 <siraben> These techniques, do they carry over to compilation as well? I haven't looked much into abstract interpretation.
2020-09-17 05:28:52 dsal is now known as Guest85365
2020-09-17 05:30:25 → __Joker joins (~Joker@180.151.106.108)
2020-09-17 05:32:06 × eric quits (~eric@2804:431:c7d4:b75:19f7:ea85:5be8:4c8e) (Ping timeout: 244 seconds)
2020-09-17 05:33:23 Guest85365 is now known as dsal
2020-09-17 05:34:10 <edwardk> abstract interpretation can be a good first step towards compilation, as you get a sense of what cases are and aren't possible in each use site
2020-09-17 05:34:19 × ransom quits (~c4264035@c-73-243-2-10.hsd1.co.comcast.net) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-17 05:34:47 <edwardk> there's another paper by van horn and might on abstract abstract machines, that i'm particularly fond of
2020-09-17 05:34:48 <edwardk> https://arxiv.org/pdf/1007.4446.pdf
2020-09-17 05:34:59 <edwardk> that paper is the one that made abstract interpretation finally gel for me
2020-09-17 05:35:01 → falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a)
2020-09-17 05:35:16 × __Joker quits (~Joker@180.151.106.108) (Ping timeout: 260 seconds)
2020-09-17 05:36:45 <siraben> edwardk: Heh, the notation looks somewhat intimidating
2020-09-17 05:37:19 <edwardk> all the greek letters and hats?
2020-09-17 05:39:26 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
2020-09-17 05:39:34 <edwardk> the paper starts with a CEK machine, which you can squint at a krivine machine and see, adds a store, moves continuations into the store, then starts to play with what happens if you make the store, etc. less accurate approximations.
2020-09-17 05:40:09 <siraben> Ok, so on closer inspection it may be tractable for me.
2020-09-17 05:40:12 × lc_ quits (~lc@94.198.42.164) (Ping timeout: 272 seconds)
2020-09-17 05:41:29 <Axman6> topos: for the encode loop, have you tried the version which just does the maths to compute the hex character for the nibble?
2020-09-17 05:41:39 × mitchellsalad_ quits (uid40617@gateway/web/irccloud.com/x-wopqfurhxhollxgh) (Quit: Connection closed for inactivity)
2020-09-17 05:43:06 → ransom joins (~c4264035@c-73-243-2-10.hsd1.co.comcast.net)
2020-09-17 05:43:30 × ransom quits (~c4264035@c-73-243-2-10.hsd1.co.comcast.net) (Client Quit)
2020-09-17 05:43:39 <edwardk> one thing all these papers on quantitative type theory seem to sweep under the rug is how much harder it makes inference for things like what to instantiate meta variables to.
2020-09-17 05:44:06 <edwardk> (just to mention a frustraton that is on y mind)
2020-09-17 05:44:25 <siraben> edwardk: what paper are you reading?
2020-09-17 05:44:52 <edwardk> well. i've been trying to build a little "ELF" style logical framework with quantitative type theory bolted in.
2020-09-17 05:45:40 <siraben> Quantitative type theory differs from linear type theories in what way?
2020-09-17 05:46:58 <edwardk> the papers in question are https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf which came first https://bentnib.org/quantitative-type-theory.pdf which fixed it up. then abel and bernardy which gave us the formulation for linear haskell, https://wg28.mpi-sws.org/technical-presentations/files/cfdb7_uploads/1584070624-w28-qtt-zion.pdf and finally the choudhury et al paper
2020-09-17 05:46:58 <edwardk> https://richarde.dev/papers/2020/quantitative/quantitative.pdf
2020-09-17 05:47:06 <edwardk> but the gist is this
2020-09-17 05:47:08 <edwardk> take your type theory
←Prev  Next→
Page 1 .. 10 11 12 13 14 15 16 17 18 19 20 .. 5022

All times are in UTC.