Logs on 2020-11-19 (freenode/#haskell)
| 00:00:38 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 00:00:49 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 00:02:44 | <boxscape> | % :kind! Fam MkR (MkR :: Relation Int Int) -- so this is fine |
| 00:02:45 | <yahb> | boxscape: forall {k} {a :: k}. Relation a Int; = 'MkR |
| 00:02:46 | <boxscape> | % :kind! Fam MkR (MkR :: Int Int) -- But I do find it a bit confusing that this has no output |
| 00:02:46 | <yahb> | boxscape: |
| 00:03:24 | <boxscape> | I guess I'll try installing HEAD and see if it's fixed there |
| 00:03:31 | → | erisco joins (~erisco@d24-57-249-233.home.cgocable.net) |
| 00:05:27 | × | sfvm quits (~sfvm@37.228.215.148) (Remote host closed the connection) |
| 00:05:37 | × | alp quits (~alp@2a01:e0a:58b:4920:7462:8d66:154:f167) (Ping timeout: 272 seconds) |
| 00:06:19 | ski | . o O ( <https://lambdacats.github.io/fixed-in-head/> ) |
| 00:07:01 | → | sfvm joins (~sfvm@37.228.215.148) |
| 00:07:34 | <boxscape> | :) |
| 00:08:23 | <hpc> | whenever someone says "it's fixed in head", i read it as "it's fixed in my imagination" |
| 00:08:26 | × | borne quits (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) (Ping timeout: 264 seconds) |
| 00:09:30 | hackage | witch 0.0.0.3 - Convert values from one type into another. https://hackage.haskell.org/package/witch-0.0.0.3 (fozworth) |
| 00:10:52 | × | jedws quits (~jedws@101.184.175.183) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 00:15:57 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 00:16:36 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 00:19:03 | × | mastarija quits (~mastarija@93-136-63-196.adsl.net.t-com.hr) (Remote host closed the connection) |
| 00:19:07 | × | Entertainment quits (~entertain@104.246.132.210) () |
| 00:19:25 | → | mastarija joins (~mastarija@93-136-63-196.adsl.net.t-com.hr) |
| 00:20:19 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:d091:432d:3cee:b0b2) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 00:24:41 | × | jonatanb quits (jonatanb@gateway/vpn/protonvpn/jonatanb) (Remote host closed the connection) |
| 00:27:44 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 00:27:44 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 00:28:01 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 00:28:19 | × | conal quits (~conal@64.71.133.70) (Ping timeout: 246 seconds) |
| 00:29:48 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) |
| 00:29:49 | <monochrom> | That's half true because clearly there is no release plan other than imagination. |
| 00:30:00 | → | conal joins (~conal@66.115.157.132) |
| 00:32:10 | × | solonarv quits (~solonarv@astrasbourg-653-1-156-4.w90-6.abo.wanadoo.fr) (Ping timeout: 265 seconds) |
| 00:32:13 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 00:32:42 | × | haasn quits (~nand@mpv/developer/haasn) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 00:33:04 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 00:33:39 | DTZUZU | is now known as toxix |
| 00:35:55 | → | hekkaidekapus_ joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 00:37:29 | → | fendor_ joins (~fendor@178.165.128.131.wireless.dyn.drei.com) |
| 00:37:38 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 00:37:43 | × | hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds) |
| 00:37:45 | × | jespada quits (~jespada@90.254.245.49) (Ping timeout: 256 seconds) |
| 00:37:50 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 00:38:04 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 00:38:25 | <boxscape> | ski: FWIW this fails in agda, but I'm not sure if the same caveat applies here that you mentioned about Nats https://pastebin.com/jKsJpPVd |
| 00:39:05 | → | jespada joins (~jespada@90.254.245.49) |
| 00:39:22 | <boxscape> | guess I should look up non-linear pattern |
| 00:39:32 | <dolio> | You need to prove it by cases. |
| 00:40:03 | × | fendor quits (~fendor@77.119.128.218.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 00:40:31 | × | mastarija quits (~mastarija@93-136-63-196.adsl.net.t-com.hr) (Quit: Leaving) |
| 00:40:34 | <boxscape> | dolio right, that would have been my intuition but from my conversation with ski it initially sounded like this would work (and it would in Haskell type families, I think) |
| 00:41:28 | × | fr33domlover quits (~fr33domlo@fsf/member/fr33domlover) (Ping timeout: 260 seconds) |
| 00:42:00 | → | haasn joins (~nand@mpv/developer/haasn) |
| 00:44:55 | → | fr33domlover joins (~fr33domlo@fsf/member/fr33domlover) |
| 00:46:23 | <dolio> | Yeah, an analogous type family would work. That it does work is a massive difference in expectation of what they mean, more or less. |
| 00:46:25 | × | Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 240 seconds) |
| 00:46:39 | <dolio> | Like, type families are assuming that all the things they operate over have decidable equality. |
| 00:47:05 | <boxscape> | Oh, that's interesting |
| 00:47:39 | <dolio> | I guess in some ways it's not even that, though. |
| 00:47:52 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) |
| 00:48:27 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Client Quit) |
| 00:48:48 | <dolio> | Because the actual behavior is like, 'if you ever figure out that m = n, then `foo m n` reduces to one thing, and if you figure out that m /= n, it reduces to another.' |
| 00:49:16 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 00:49:55 | <boxscape> | oh, yeah.. I thought it would work in agda if you wrote {a} {.a}, but with your it doesn't sound like it, and indeed, it says "Failed to infer the value of dotted pattern". |
| 00:50:09 | <boxscape> | s/with your/with your explanation |
| 00:50:17 | × | bergey quits (~user@pool-74-108-99-127.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 00:50:19 | <dolio> | No, .a is for when you match on a proof that two things are equal. |
| 00:50:51 | <boxscape> | RIght, okay |
| 00:51:03 | <boxscape> | So it's very different from saying @a @a in a type family |
| 00:51:26 | <dolio> | Yeah. |
| 00:51:49 | × | DataComp_ quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Remote host closed the connection) |
| 00:54:30 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 00:54:46 | → | rogue_cheddar joins (~manjaro-u@2806:1000:8003:2a54:da9a:e457:f660:288a) |
| 00:55:37 | <dolio> | Anyhow, if you don't want things to get stuck, which is important in Agda, then decidable equality is kind of important for justifying that sort of matching. |
| 00:56:07 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) |
| 00:56:19 | <dolio> | Whereas type families are kind of based on the idea of adding things that get stuck, and specifying certain scenarios where they become unstuck, with no guarantee that all scenarios are covered. |
| 00:56:37 | × | wpcarro quits (sid397589@gateway/web/irccloud.com/x-jyvrhcovkjnuufaq) (Ping timeout: 260 seconds) |
| 00:57:36 | <boxscape> | hmm I wonder how this pretend-dec-eq-ness will work when you try to match on unsaturated type families once those are merged |
| 00:57:44 | <boxscape> | I guess maybe it'll just get stuck |
| 00:58:21 | × | Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:59:24 | → | wpcarro joins (sid397589@gateway/web/irccloud.com/x-mptadpaqtazralft) |
| 00:59:33 | × | xsperry quits (~as@unaffiliated/xsperry) (Ping timeout: 260 seconds) |
| 01:01:14 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 01:02:13 | → | Tesseraction joins (~Tesseract@unaffiliated/tesseraction) |
| 01:02:54 | × | thc202 quits (~thc202@unaffiliated/thc202) (Quit: thc202) |
| 01:03:00 | <ski> | boxscape : yes, you'd need `sameNat {false} {false} = just refl; sameNat {true} {true} = just refl; sameNat = nothing', pretty sure |
| 01:03:47 | <boxscape> | yeah, that does work |
| 01:05:37 | × | jneira quits (02896ac0@gateway/web/cgi-irc/kiwiirc.com/ip.2.137.106.192) (Ping timeout: 264 seconds) |
| 01:05:38 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 01:06:01 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 01:06:30 | <p0a> | /quit bye |
| 01:06:32 | × | p0a quits (~user@unaffiliated/p0a) (Quit: bye) |
| 01:06:39 | × | SupaYoshi quits (~supayoshi@213-10-140-13.fixed.kpn.net) (Ping timeout: 260 seconds) |
| 01:08:14 | → | cosimone joins (~cosimone@5.171.24.92) |
| 01:08:19 | ← | iqubic parts (~user@2601:602:9500:4870:18b7:5f73:2db2:1881) ("ERC (IRC client for Emacs 28.0.50)") |
| 01:09:18 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 01:13:25 | × | m0rphism quits (~m0rphism@HSI-KBW-095-208-098-207.hsi5.kabel-badenwuerttemberg.de) (Ping timeout: 264 seconds) |
| 01:13:49 | → | SupaYoshi joins (~supayoshi@213-10-140-13.fixed.kpn.net) |
| 01:17:10 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Quit: Leaving) |
| 01:17:45 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 01:19:14 | → | DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) |
| 01:20:37 | → | Tourist joins (~tourist@da.tourist.sh) |
| 01:20:37 | × | Tourist quits (~tourist@da.tourist.sh) (Changing host) |
| 01:20:37 | → | Tourist joins (~tourist@unaffiliated/tourist) |
| 01:20:41 | → | christo joins (~chris@81.96.113.213) |
| 01:21:14 | → | nuncanada joins (~dude@179.235.160.168) |
| 01:21:27 | → | guest1119 joins (~user@49.5.6.87) |
| 01:25:32 | × | nek0 quits (~nek0@mail.nek0.eu) (Ping timeout: 260 seconds) |
| 01:25:45 | × | cgfuh quits (~cgfuh@181.167.191.58) (Ping timeout: 240 seconds) |
| 01:27:03 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 01:30:34 | → | i8ucl joins (~manjaro-u@201.130.137.230.dsl.dyn.telnor.net) |
| 01:31:07 | × | rogue_cheddar quits (~manjaro-u@2806:1000:8003:2a54:da9a:e457:f660:288a) (Ping timeout: 272 seconds) |
| 01:32:06 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 01:32:45 | × | Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 240 seconds) |
| 01:33:16 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Quit: leaving) |
| 01:33:24 | → | magnuscake joins (~magnuscak@103.44.33.121) |
| 01:33:36 | → | Lord_of_Life_ joins (~Lord@46.217.218.252) |
| 01:33:36 | × | Lord_of_Life quits (~Lord@46.217.217.18) (Ping timeout: 240 seconds) |
| 01:34:31 | hackage | citeproc 0.2 - Generates citations and bibliography from CSL styles. https://hackage.haskell.org/package/citeproc-0.2 (JohnMacFarlane) |
| 01:35:47 | × | magnuscake quits (~magnuscak@103.44.33.121) (Client Quit) |
| 01:37:03 | → | wh0 joins (~wh0000@cpc152777-shef18-2-0-cust223.17-1.cable.virginm.net) |
| 01:37:05 | → | elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) |
| 01:42:42 | → | nek0 joins (~nek0@mail.nek0.eu) |
| 01:44:51 | × | Deide quits (~Deide@217.155.19.23) (Quit: Seeee yaaaa) |
| 01:47:29 | × | nek0 quits (~nek0@mail.nek0.eu) (Client Quit) |
| 01:49:07 | → | nek0 joins (~nek0@mail.nek0.eu) |
| 01:52:07 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 01:52:51 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 02:06:19 | <guest1119> | case parse (spaces >> symbol) "lisp" input of ... |
| 02:06:27 | <guest1119> | what "lisp" and input here mean? |
| 02:06:40 | <guest1119> | parse :: Stream s Identity t => Parsec s () a -> SourceName -> s -> Either ParseError a |
| 02:06:52 | <guest1119> | from https://hackage.haskell.org/package/parsec-3.1.14.0/docs/Text-Parsec.html |
| 02:07:25 | × | wh0 quits (~wh0000@cpc152777-shef18-2-0-cust223.17-1.cable.virginm.net) (Ping timeout: 264 seconds) |
| 02:07:46 | <guest1119> | also, what do Stream s Identity t constraint? constraint for s? not t? |
| 02:08:37 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 02:10:47 | <glguy> | "lisp" is the name of the input |
| 02:11:01 | <glguy> | Often that's a filename or some other description |
| 02:13:19 | → | christo joins (~chris@81.96.113.213) |
| 02:15:44 | <Axman6> | s appears to be the type of impot that's being parsed, to probably usually a String or Text |
| 02:15:51 | <Axman6> | input* |
| 02:17:49 | → | xsperry joins (~as@unaffiliated/xsperry) |
| 02:18:44 | → | toorevitimirp joins (~tooreviti@117.182.180.118) |
| 02:23:00 | × | jakob_ quits (~textual@p200300f49f162200756a589588d5c172.dip0.t-ipconnect.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 02:23:44 | × | conal quits (~conal@66.115.157.132) (Quit: Computer has gone to sleep.) |
| 02:24:46 | <Axman6> | guest1119: does that help at all? |
| 02:30:34 | <guest1119> | Axman6: yes |
| 02:30:50 | <guest1119> | but why we would give input a name? |
| 02:31:03 | <guest1119> | case (parse numbers "" "11, 2, 43") of |
| 02:31:15 | <guest1119> | numbers = commaSep integer |
| 02:31:43 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 260 seconds) |
| 02:31:44 | <guest1119> | this give "11, 2, 43" a "" name? |
| 02:33:25 | × | st8less quits (~st8less@2603:a060:11fd:0:9539:fd10:c1ca:1d78) (Quit: WeeChat 2.9) |
| 02:37:40 | × | guest1119 quits (~user@49.5.6.87) (Remote host closed the connection) |
| 02:38:10 | × | nuncanada quits (~dude@179.235.160.168) (Quit: Leaving) |
| 02:39:51 | → | isacl___ joins (uid13263@gateway/web/irccloud.com/x-zatkgdiubqivrbyl) |
| 02:40:09 | × | xff0x quits (~fox@2001:1a81:5310:3c00:eddd:290e:8cac:b048) (Ping timeout: 272 seconds) |
| 02:41:33 | → | xff0x joins (~fox@2001:1a81:534b:a000:20f1:4040:a0e2:f16) |
| 02:48:08 | → | jakob_ joins (~textual@p200300f49f16220080fac7d5cef5a2db.dip0.t-ipconnect.de) |
| 02:48:17 | × | jakob_ quits (~textual@p200300f49f16220080fac7d5cef5a2db.dip0.t-ipconnect.de) (Client Quit) |
| 02:48:54 | → | drbean joins (~drbean@TC210-63-209-68.static.apol.com.tw) |
| 02:50:45 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 02:54:34 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 02:55:37 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 02:56:35 | → | SupaYoshii joins (~supayoshi@213-10-140-13.fixed.kpn.net) |
| 02:57:23 | × | SupaYoshi quits (~supayoshi@213-10-140-13.fixed.kpn.net) (Ping timeout: 260 seconds) |
| 02:58:59 | → | guest1119 joins (~user@49.5.6.87) |
| 03:02:50 | × | guest1119 quits (~user@49.5.6.87) (Client Quit) |
| 03:04:00 | → | guest1119 joins (~user@49.5.6.87) |
| 03:04:02 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 03:04:31 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 03:05:45 | → | wei2912 joins (~wei2912@unaffiliated/wei2912) |
| 03:07:37 | → | rab24ack[m] joins (rab24ackma@gateway/shell/matrix.org/x-psmufgypmrylcnyv) |
| 03:12:27 | × | inkbottle quits (~inkbottle@aaubervilliers-654-1-104-55.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 03:12:27 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 03:13:05 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 03:13:07 | × | howdoi quits (uid224@gateway/web/irccloud.com/x-xcriusnvhpaknzlz) (Quit: Connection closed for inactivity) |
| 03:13:16 | × | erisco quits (~erisco@d24-57-249-233.home.cgocable.net) (Ping timeout: 240 seconds) |
| 03:14:18 | → | falafel joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) |
| 03:15:08 | × | Benzi-Junior quits (~BenziJuni@dsl-149-67-198.hive.is) (Ping timeout: 244 seconds) |
| 03:15:32 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-104-55.w86-212.abo.wanadoo.fr) |
| 03:18:27 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 03:18:27 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 03:19:01 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 03:19:41 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 03:19:41 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 03:20:26 | × | urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna) |
| 03:21:43 | × | i8ucl quits (~manjaro-u@201.130.137.230.dsl.dyn.telnor.net) (Quit: Konversation terminated!) |
| 03:24:00 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 03:25:08 | → | Saukk joins (~Saukk@2001:998:f9:2914:1c59:9bb5:b94c:4) |
| 03:25:18 | × | toorevitimirp quits (~tooreviti@117.182.180.118) (Remote host closed the connection) |
| 03:26:38 | → | toorevitimirp joins (~tooreviti@117.182.180.118) |
| 03:28:21 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 03:29:26 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Max SendQ exceeded) |
| 03:29:30 | hackage | aeson-gadt-th 0.2.5.0 - Derivation of Aeson instances for GADTs https://hackage.haskell.org/package/aeson-gadt-th-0.2.5.0 (abrar) |
| 03:29:53 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 03:33:39 | × | ph88 quits (~ph88@ip5f5af6cd.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 03:37:47 | × | Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds) |
| 03:39:06 | × | crdrost quits (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) (Quit: This computer has gone to sleep) |
| 03:42:39 | → | Benzi-Junior joins (~BenziJuni@88-149-67-198.du.xdsl.is) |
| 03:43:39 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 03:43:58 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 246 seconds) |
| 03:45:19 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Killed (moon.freenode.net (Nickname regained by services))) |
| 03:45:27 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 03:45:48 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 260 seconds) |
| 03:46:59 | × | andi- quits (~andi-@NixOS/user/andi-) (Remote host closed the connection) |
| 03:50:17 | <hololeap> | i have a function: tryE :: MonadUnliftIO m => m a -> ExceptT IOException m a |
| 03:51:06 | × | toorevitimirp quits (~tooreviti@117.182.180.118) (Remote host closed the connection) |
| 03:51:07 | → | jedws joins (~jedws@101.184.150.93) |
| 03:51:23 | <hololeap> | how reasonable is it to use this wherever possible (and deal with the ExceptT monad) vs. keeping IOExceptions from the IO monad implicit and dealing with them closer to the `main` function |
| 03:51:45 | × | theDon quits (~td@94.134.91.119) (Ping timeout: 240 seconds) |
| 03:52:14 | <hololeap> | converting to `ExceptT ...` makes the possibility of an exception more explicit |
| 03:52:38 | → | toorevitimirp joins (~tooreviti@117.182.180.118) |
| 03:53:57 | → | theDon joins (~td@muedsl-82-207-238-104.citykom.de) |
| 03:54:04 | → | andi- joins (~andi-@NixOS/user/andi-) |
| 03:54:08 | <hololeap> | but then again, i could just try to remember that any IO operation has the possibility of throwing an IOException |
| 03:58:41 | <glguy> | Doing this will mean you have two places to catch IOExceptions, still in IO and also in ExceptT, and your code will be slower |
| 04:00:01 | × | alexelcu quits (~alexelcu@142.93.180.198) (Quit: ZNC 1.8.2 - https://znc.in) |
| 04:00:15 | <hololeap> | yeah, it's also more typing |
| 04:00:23 | → | Rudd0 joins (~Rudd0@185.189.115.108) |
| 04:00:55 | <hololeap> | i did it in one place and then realized it's kind of an all-or-nothing approach. you can't really mix it with the default. |
| 04:01:00 | → | alexelcu joins (~alexelcu@142.93.180.198) |
| 04:01:22 | <hololeap> | well, you can... |
| 04:02:19 | × | ddellacosta quits (dd@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 256 seconds) |
| 04:04:27 | × | acidjnk_new quits (~acidjnk@p200300d0c719ff57608036dc958592ad.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 04:05:12 | → | macrover joins (~macrover@ip70-189-231-35.lv.lv.cox.net) |
| 04:05:26 | × | renzhi quits (~renzhi@2607:fa49:655f:e600::28da) (Ping timeout: 264 seconds) |
| 04:12:13 | × | thunderrd quits (~thunderrd@183.182.111.169) (Ping timeout: 264 seconds) |
| 04:14:11 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 04:16:31 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Ping timeout: 246 seconds) |
| 04:17:35 | × | moth quits (~moth@s91904426.blix.com) (Remote host closed the connection) |
| 04:19:29 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Remote host closed the connection) |
| 04:20:12 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 04:20:35 | ← | mwehner parts (~martin@li910-8.members.linode.com) () |
| 04:22:31 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 04:24:21 | → | thunderrd joins (~thunderrd@183.182.114.130) |
| 04:24:56 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Ping timeout: 240 seconds) |
| 04:26:19 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 04:29:35 | → | ph88 joins (~ph88@2a02:8109:9e00:7e5c:a963:461:83fa:2c4) |
| 04:30:58 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 04:37:36 | × | drbean quits (~drbean@TC210-63-209-68.static.apol.com.tw) (Ping timeout: 240 seconds) |
| 04:46:28 | × | tumdedum quits (~tumdedum@unaffiliated/espiral) (Ping timeout: 260 seconds) |
| 04:46:31 | hackage | yesod-core 1.6.18.7 - Creation of type-safe, RESTful web applications. https://hackage.haskell.org/package/yesod-core-1.6.18.7 (MichaelSnoyman) |
| 04:53:12 | × | falafel quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Ping timeout: 260 seconds) |
| 04:53:14 | → | spatchkaa joins (~spatchkaa@S010600fc8da47b63.gv.shawcable.net) |
| 04:53:35 | → | tumdedum joins (~tumdedum@unaffiliated/espiral) |
| 04:54:30 | × | thunderrd quits (~thunderrd@183.182.114.130) (Ping timeout: 246 seconds) |
| 04:55:23 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Ping timeout: 240 seconds) |
| 04:56:55 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 05:00:17 | × | texasmynsted quits (~texasmyns@212.102.45.121) (Remote host closed the connection) |
| 05:00:57 | → | conal joins (~conal@64.71.133.70) |
| 05:00:57 | × | Saukk quits (~Saukk@2001:998:f9:2914:1c59:9bb5:b94c:4) (Remote host closed the connection) |
| 05:02:29 | → | texasmynsted joins (~texasmyns@212.102.45.121) |
| 05:04:13 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 05:05:15 | × | tumdedum quits (~tumdedum@unaffiliated/espiral) (Ping timeout: 265 seconds) |
| 05:07:12 | × | texasmynsted quits (~texasmyns@212.102.45.121) (Ping timeout: 260 seconds) |
| 05:07:42 | → | thunderrd joins (~thunderrd@183.182.110.8) |
| 05:08:54 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 05:09:49 | × | spatchkaa quits (~spatchkaa@S010600fc8da47b63.gv.shawcable.net) (Ping timeout: 264 seconds) |
| 05:10:56 | × | mbomba quits (~mbomba@bras-base-toroon2719w-grc-49-142-114-9-241.dsl.bell.ca) (Quit: WeeChat 3.0) |
| 05:12:53 | → | christo joins (~chris@81.96.113.213) |
| 05:13:03 | → | tumdedum joins (~tumdedum@unaffiliated/espiral) |
| 05:13:16 | × | cosimone quits (~cosimone@5.171.24.92) (Ping timeout: 240 seconds) |
| 05:14:21 | → | aioe joins (aoei@2a01:7e01::f03c:92ff:fe4f:e85a) |
| 05:14:23 | × | monochrom quits (trebla@216.138.220.146) (Quit: NO CARRIER) |
| 05:15:20 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Remote host closed the connection) |
| 05:15:25 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 240 seconds) |
| 05:17:16 | → | cosimone joins (~cosimone@5.170.241.44) |
| 05:17:23 | × | christo quits (~chris@81.96.113.213) (Ping timeout: 260 seconds) |
| 05:17:29 | × | aoei quits (~aoei@240.223.246.35.bc.googleusercontent.com) (Remote host closed the connection) |
| 05:18:44 | aioe | is now known as aoei |
| 05:19:07 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:8c9:42ac:c0f6:8508) (Ping timeout: 272 seconds) |
| 05:21:32 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Remote host closed the connection) |
| 05:21:38 | × | ft quits (~ft@shell.chaostreff-dortmund.de) (Ping timeout: 264 seconds) |
| 05:21:52 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 05:22:23 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Quit: leaving) |
| 05:22:38 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 05:24:43 | → | day_ joins (~Unknown@unaffiliated/day) |
| 05:27:05 | → | SanchayanMaity joins (~Sanchayan@106.201.35.233) |
| 05:27:45 | × | day quits (~Unknown@unaffiliated/day) (Ping timeout: 240 seconds) |
| 05:27:45 | day_ | is now known as day |
| 05:27:58 | → | monochrom joins (trebla@216.138.220.146) |
| 05:28:31 | → | xerox_ joins (~xerox@unaffiliated/xerox) |
| 05:31:06 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:b274:8c51:102c:8ca9) |
| 05:32:10 | → | n00b joins (d055ed89@208.85.237.137) |
| 05:32:55 | n00b | is now known as n0042 |
| 05:33:34 | <n0042> | Hello folks. May I ask what is probably a pretty common newbie question? I have done a lot of research on it and am starting to feel a little stumped at having not found the proper answer |
| 05:33:48 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 272 seconds) |
| 05:34:52 | → | zyklotomic joins (~ethan@unaffiliated/chocopuff) |
| 05:35:29 | <n0042> | I have a situation where I need to take an unknown # of lines from stdin (no more, no less, finite but unknown until runtime). I have tried a hundred different ways of trying to use getLine programmatically so that it collects exactly n-amount of lines, after n is known. Is there a good article I can read on this? |
| 05:36:11 | <zyklotomic> | what have you tried so far |
| 05:37:33 | <n0042> | So far my most promising approach has been to get the initial number of lines with getLine (because that input is known) parse it and extract the number, and then try to run getLine that amount of times. |
| 05:37:59 | <glguy> | that sounds right |
| 05:37:59 | <zyklotomic> | i'm just a beginner, but maybe replicateM might help |
| 05:38:04 | <dsal> | It'd be easier to show code and describe the confusion than to describe the problem. |
| 05:38:06 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 05:38:18 | <glguy> | ?paste |
| 05:38:18 | <lambdabot> | A pastebin: https://paste.debian.net/ |
| 05:38:20 | <zyklotomic> | replicateM n getLine |
| 05:38:39 | <n0042> | I have not tried replicateM. I'll try that. |
| 05:38:41 | <glguy> | zyklotomic, maybe, but n0042 ought to be able to do this without any library functions first |
| 05:39:13 | <glguy> | n0042, Do you have any attempts yet? What have you tried? |
| 05:39:32 | <n0042> | I did try: "take n (repeat getLine)" and wound up with a list of getLine functions that I then wasn't sure how to turn into values |
| 05:39:54 | <n0042> | I also tried recursive-do as described in the ghc docs, but that didn't want to compile the way I was trying to do it. |
| 05:40:29 | <glguy> | recursive-do is something you don't need |
| 05:40:29 | <dsal> | Showing code (and errors/confusion) is more informative than describing code. |
| 05:40:42 | × | cosimone quits (~cosimone@5.170.241.44) (Quit: cosimone) |
| 05:40:45 | <glguy> | You can paste your code on a pastebin so that people can see what you've got |
| 05:40:56 | <n0042> | I'll use pastebin real quick to show you what I've got so far. uno momento |
| 05:41:04 | <glguy> | showing code will help us see what you do know how to do |
| 05:41:52 | → | agrajag` joins (~agrajag`@84.39.117.57) |
| 05:43:24 | <dsal> | Some confusion seems to be between functions and actions. replicating `getLine` will make a bunch of `getLine` actions, but it won't get lines. There's a path from there, but it's probably not what you want. |
| 05:43:57 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) |
| 05:44:49 | <zyklotomic> | on a seperate thread, i have a question about folds vs monads |
| 05:44:59 | <zyklotomic> | hope you guys don't mind juggling the convo a bit |
| 05:45:11 | <glguy> | go for it |
| 05:45:29 | <zyklotomic> | is there any deeper relationship b/w them? I was reading https://mail.haskell.org/pipermail/beginners/2014-August/013993.html |
| 05:45:43 | <zyklotomic> | as a result of a google search, after noticing that foldl was kinda like State |
| 05:46:20 | <zyklotomic> | then I was writing another function that folded with a monoid (list appending) |
| 05:46:30 | <glguy> | There's not much relating folds to monads |
| 05:46:31 | <zyklotomic> | and it basically was Writer (i think) |
| 05:46:38 | <zyklotomic> | are these just coincidences? |
| 05:46:56 | <zyklotomic> | I should generally prefer using folds right |
| 05:47:11 | <zyklotomic> | I can show an example |
| 05:47:29 | × | aoei quits (aoei@2a01:7e01::f03c:92ff:fe4f:e85a) (Quit: ZNC 1.7.5 - https://znc.in) |
| 05:47:37 | <n0042> | https://pastebin.com/zwuqHsSY |
| 05:47:37 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 05:48:00 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 05:48:02 | <glguy> | zyklotomic, foldl is similar to traverse used with State |
| 05:48:04 | <n0042> | Here's sort of what I got so far. It's for an assignment but there's no need to get into the assignment itself. I already have that part figured out. It's just the I/O that's confusing me |
| 05:48:08 | <glguy> | but that's not much about being a monad |
| 05:48:17 | <zyklotomic> | https://paste.debian.net/1173146/ |
| 05:48:32 | <zyklotomic> | wait yeah, you're right, I probably shouldn't have jumped to monad |
| 05:48:35 | <glguy> | that's more about foldl being related to State specifically in the context of foldable types |
| 05:49:44 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 05:49:56 | <glguy> | :t \f t -> runState(traverse (state . f) t) |
| 05:49:57 | <lambdabot> | Traversable t => (a -> s -> (b, s)) -> t a -> s -> (t b, s) |
| 05:50:08 | → | aoei joins (~aoei@li2174-104.members.linode.com) |
| 05:50:12 | <glguy> | :t foldl |
| 05:50:13 | <lambdabot> | Foldable t => (b -> a -> b) -> b -> t a -> b |
| 05:50:36 | <glguy> | :t scanl |
| 05:50:38 | <lambdabot> | (b -> a -> b) -> b -> [a] -> [b] |
| 05:50:46 | <glguy> | :t mapAccumL |
| 05:50:47 | <lambdabot> | Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c) |
| 05:51:01 | <zyklotomic> | or actually, I mean, what about Writer and State |
| 05:51:17 | <zyklotomic> | would you like classify them as some kind, or am I looking into this too much |
| 05:51:27 | <zyklotomic> | and it is just a nice coincidenec |
| 05:51:51 | <zyklotomic> | where the behavior is "traversing" |
| 05:51:52 | <glguy> | there's no deep connection that I can think of |
| 05:52:21 | <zyklotomic> | ah fair enough, thanks for entertaining my q |
| 05:52:43 | <dsal> | n0042: what do you want `results` to be? |
| 05:53:14 | <dsal> | From the application, it looks like you want it to be a single string. |
| 05:54:18 | <n0042> | So, results is going to print a line for each "packet" showing the time it was processed or if it was processed. That's all going to be handled by the program logic which i've got covered, and it'll just print off a list of strings. But to get there I need to collect the strings which contain the arrival time and time-to-process for each packet, |
| 05:54:18 | <n0042> | which is the programmatic input part. |
| 05:54:54 | <dsal> | Do you understand what `repeat getLine` means? |
| 05:55:01 | <dsal> | :t repeat getLine |
| 05:55:04 | <lambdabot> | [IO String] |
| 05:55:35 | <n0042> | Yeah it's a list of getLine functions. I was trying to find some way to call getLine a certain amount of times in a row. |
| 05:55:43 | <n0042> | But I'm not sure I'm on the right track |
| 05:55:50 | <dsal> | It's a list of actions that produce strings. |
| 05:56:31 | <dsal> | What type would make more sense here? |
| 05:57:02 | <dsal> | (it's often easier to think about what you want than to struggle with the parts you have) |
| 05:57:11 | <n0042> | Strings themselves, I suppose. |
| 05:57:33 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 05:57:44 | <dsal> | What does "Strings themselves" mean? |
| 05:57:56 | <n0042> | The assignment's program flow is: Input buffer size and number of packets -> input line for each packet -> calculate the processing time for each packet or if it was dropped -> output a line for each packet. |
| 05:58:00 | <dsal> | (Haskell is an ideal language to speak here to avoid misunderstanding) |
| 05:58:08 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 05:58:22 | <n0042> | The input/output is pre-determined and I can't change how it works because it's an automated system that collectes from stdin during runtime. |
| 05:58:38 | <dsal> | None of these details are relevant to what you're trying to do. |
| 05:58:42 | <n0042> | We got to choose our language though and I figured it's be a good way to dive in head first with haskell |
| 05:59:23 | <zyklotomic> | i'm saying in case no one pointed out the distinction, `repeat getLine` is returing a list of the actions, but nothing is executing those actions |
| 05:59:48 | <dsal> | But taking a step back and identifying what you actually want might make this easy. |
| 05:59:52 | <n0042> | I know. I'm not sure how to execute those actions once I have them. |
| 06:00:00 | <zyklotomic> | yup that is the crux (i think) |
| 06:00:10 | <dsal> | Stating clearly what you want would speed things up a lot. |
| 06:00:38 | <n0042> | What I want is to get n-lines from stdin, separated by newline characters. |
| 06:00:58 | <n0042> | As [Char] types |
| 06:01:17 | <n0042> | Which I will then parse into [Int] types |
| 06:01:37 | <dsal> | OK, closer... Less English, more Haskell. How would you describe the above in Haskell? |
| 06:01:44 | <dsal> | :t getLine -- e.g. |
| 06:01:46 | <lambdabot> | IO String |
| 06:01:54 | <n0042> | Well, a single line is easy: line <- getLine |
| 06:01:58 | <dsal> | So, `getLine` is `IO String` |
| 06:02:04 | <dsal> | What type are you looking for |
| 06:02:05 | <dsal> | ? |
| 06:02:06 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 06:02:35 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 06:02:58 | <n0042> | String |
| 06:03:07 | <zyklotomic> | bigger |
| 06:03:20 | <n0042> | [String]? |
| 06:03:21 | <zyklotomic> | think a bit higher |
| 06:03:23 | <zyklotomic> | yup |
| 06:03:37 | <dsal> | Closer, but it isn't pure. |
| 06:03:40 | <dsal> | You're doing IO to get there. |
| 06:03:56 | <n0042> | I am intrigued. Tell me more. |
| 06:04:03 | <dsal> | :t getLine |
| 06:04:04 | <lambdabot> | IO String |
| 06:04:31 | <dsal> | That's not a String. |
| 06:04:37 | <n0042> | line <- getLine results in String. |
| 06:04:49 | <n0042> | according to my REPL, the type of line is String after that |
| 06:05:03 | <dsal> | Eh. That's slightly confusing. |
| 06:05:20 | <n0042> | Which is why I thought I might be able to turn [getLine] into [String] somehow |
| 06:05:34 | <zyklotomic> | the <- does some magic lol |
| 06:05:56 | <dsal> | It's also not a complete useful expression. The repl lets you do things that don't fully make sense. |
| 06:06:08 | <dsal> | @undo do { line <- getLine } |
| 06:06:08 | <lambdabot> | <unknown>.hs:1:23:Parse error: Last statement in a do-block must be an expression |
| 06:06:16 | <dsal> | @undo do { line <- getLine; putStrLn line } |
| 06:06:16 | <lambdabot> | getLine >>= \ line -> putStrLn line |
| 06:07:34 | <dsal> | How about this. Let's say you want to create a new thing called `getLines`. What does is its type? |
| 06:07:40 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 06:07:49 | <n0042> | :t getLine |
| 06:07:50 | <lambdabot> | IO String |
| 06:07:57 | <n0042> | so... [IO String] ? |
| 06:08:22 | <LKoen> | IO [String] ? |
| 06:08:26 | <dsal> | That's not super useful, though, as you found out, because now instead of having one action, you have a list of actions. What would one action look like? |
| 06:08:57 | → | xerox_ joins (~xerox@unaffiliated/xerox) |
| 06:09:48 | <dsal> | So, there's a super easy way to go from `[m a]` to `m [a]` but I don't think it's necessarily a good path. It might be more useful for you to consider writing a function that takes the `n` and returns the actual thing you need. |
| 06:10:24 | <dsal> | (which is technical `replicateM`, but you'd get pretty far along if you write this yourself) |
| 06:10:29 | <n0042> | I must admit I'm having a hard time with Haskell's I/O. That is exactly what I'd like to do. |
| 06:10:54 | <dsal> | You're having a hard time because you're trying to use it without understanding it or your goal. :) |
| 06:10:59 | <n0042> | I have really enjoyed using this language for my assignments so far. It's a real pleasure to write and work with. |
| 06:11:34 | → | borne joins (~fritjof@200116b864eda200f1dc39039d201adf.dip.versatel-1u1.de) |
| 06:11:34 | <dsal> | It continues to get better as you learn more of it. But some things that you can kind of hand wave will eventually require a bit more understanding. In particular, expressing the type of the thing you want. |
| 06:12:12 | → | SanchayanM joins (~Sanchayan@223.226.123.235) |
| 06:12:57 | <n0042> | Well my goal is to take input, calculate some results, and print outputs. The "calculating some results" part is the actual assignment, and I've already worked it out, and was the fun part. The I/O part is throwing me for a loop because it should have been trivial. It's like two different languages when it comes to program logic and I/O |
| 06:12:59 | <dsal> | Also, though it's still partial, I'd write what you have so far something like: `[bufferSize, numPackets] <- map read . words <$> getLine` -- but that's next week's episode. |
| 06:13:16 | × | SanchayanMaity quits (~Sanchayan@106.201.35.233) (Ping timeout: 260 seconds) |
| 06:13:39 | <n0042> | I am the sort of person who likes to understand this stuff from first principles where possible. Do you have any good resources for understanding how replicateM works on a more intuitive level? I'd like to learn this. |
| 06:14:06 | <dsal> | Haskell Programming From First Principles will get you there quickly. |
| 06:14:34 | <dsal> | @src replicateM |
| 06:14:34 | <lambdabot> | replicateM n x = sequence (replicate n x) |
| 06:14:49 | <zyklotomic> | the weird part about haskell is, the hard stuff becomes easy and the "easy" stuff becomes hard |
| 06:14:55 | <zyklotomic> | *when you're first learning it |
| 06:15:13 | <zyklotomic> | like IO basically |
| 06:15:22 | <dsal> | I'd by that with the addendum. After a while, most things are easy. |
| 06:15:51 | × | lukelau_ quits (~lukelau@46.101.13.214) (Quit: Bye) |
| 06:16:05 | <n0042> | I recently joined a study group for that book, but we haven't started yet. |
| 06:16:05 | <zyklotomic> | but i'm sure the fun never gets old |
| 06:16:07 | → | lukelau joins (~lukelau@46.101.13.214) |
| 06:16:25 | <n0042> | It really is a fun language. The list comprehensions are my favorite in any language I've used so far. |
| 06:16:49 | <dsal> | I generally recommend that book. It's a slow path, which I think will get you somewhere useful the fastest. |
| 06:17:19 | → | coot joins (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) |
| 06:17:46 | → | darjeeling_ joins (~darjeelin@122.245.211.11) |
| 06:17:46 | <zyklotomic> | list comprehensions are cool indeed |
| 06:18:07 | <dsal> | I somehow don't use list comprehensions that much in haskell. |
| 06:18:28 | <zyklotomic> | I use them in ghci most often tbh |
| 06:18:31 | <dsal> | I often forget they exist. heh. |
| 06:18:35 | <n0042> | So far everything I've written has been a mixture of list comprehensions and the recursive-go pattern. |
| 06:18:42 | <n0042> | But I'm still doing pretty basic stuff |
| 06:18:52 | <zyklotomic> | when I switched to Linux from a Mac, ghci replaced the Spotlight calculator if you know what spotlight is |
| 06:18:59 | <n0042> | recursive-go makes my inner LISP programmer happy |
| 06:19:07 | <zyklotomic> | basically just quickfire calculator that you can type some math into |
| 06:19:07 | <dsal> | what's recursive-go? |
| 06:19:52 | <n0042> | Where you wrap a function in a "go" function scoped in a "where" statement that requires parameters that don't make sense to call outside the function. Usually to do something in a list-processing kind of way |
| 06:20:08 | <dsal> | Oh. Just recursion. :) |
| 06:20:36 | <zyklotomic> | I've been struggling to know what to call that practice lol |
| 06:20:36 | <dsal> | Usually there's a higher level abstraction that does the thing already |
| 06:20:42 | <n0042> | Yes, but in Scheme or something you'd have to wrap it in a macro to make it look decent. |
| 06:20:57 | <zyklotomic> | some things are just kinda un-pronuncable in Haskell lol |
| 06:21:10 | <zyklotomic> | like all the weird operators and when someone decides to roll their own custom operator too |
| 06:21:42 | <dsal> | > maximumOf (folded . _Right) [Left 1, Right 2, Left 3, Right 4, Left 5, Right 3] |
| 06:21:44 | <lambdabot> | Just 4 |
| 06:22:35 | <dsal> | Operators are just functions. The really common ones have fairly common names. Or we just don't say them much. |
| 06:23:58 | <n0042> | I am still trying to wrap my head around some of them. You used two I'm unfamiliar with in that snippet you posted: (.) and <$> |
| 06:24:07 | <dsal> | > sum (digitToInt <$> "123") |
| 06:24:09 | <lambdabot> | 6 |
| 06:24:16 | → | alp joins (~alp@2a01:e0a:58b:4920:d4c7:761f:e715:72ea) |
| 06:24:17 | <dsal> | . and $ are *super* common |
| 06:24:22 | <dsal> | :t (.) |
| 06:24:24 | <lambdabot> | (b -> c) -> (a -> b) -> a -> c |
| 06:24:25 | <zyklotomic> | with time |
| 06:24:25 | <dsal> | :t ($) |
| 06:24:27 | <lambdabot> | (a -> b) -> a -> b |
| 06:24:41 | → | codeAlways joins (uid272474@gateway/web/irccloud.com/x-rnqcrwigssxuyxdw) |
| 06:24:42 | <dsal> | . is just how you compose functions. |
| 06:24:50 | <dsal> | @src (.) |
| 06:24:50 | <lambdabot> | (f . g) x = f (g x) |
| 06:24:56 | <zyklotomic> | <$> is fmap |
| 06:24:58 | <dsal> | That's it. |
| 06:25:05 | <n0042> | Oh |
| 06:25:06 | <zyklotomic> | it is like a generlaized map |
| 06:25:22 | <dsal> | IMO, map shouldn't exist, but at least a few people think it's not bad. |
| 06:25:35 | <dsal> | > fmap (+1) [1..5] |
| 06:25:37 | <lambdabot> | [2,3,4,5,6] |
| 06:25:42 | <dsal> | > (+1) <$> [1..5] |
| 06:25:44 | <lambdabot> | [2,3,4,5,6] |
| 06:25:48 | <n0042> | ($) I have used plenty to get rid of parentheses, but <$> was a new one. That's pretty sweet |
| 06:26:07 | <dsal> | $ should be used sparingly. :) |
| 06:26:13 | <dsal> | :t ($) |
| 06:26:14 | <lambdabot> | (a -> b) -> a -> b |
| 06:26:16 | <dsal> | :t (<$>) |
| 06:26:18 | <lambdabot> | Functor f => (a -> b) -> f a -> f b |
| 06:26:20 | <zyklotomic> | dsal: I find myself using fmap on lists unconsciously, cause you type that before the list and you don't register that you're getting a list mentally yet |
| 06:26:38 | <n0042> | <$> is just infix fmap... got it.. that's pretty neat |
| 06:26:43 | <zyklotomic> | yup |
| 06:26:48 | <dsal> | @src (<$>) |
| 06:26:48 | <lambdabot> | f <$> a = fmap f a |
| 06:27:16 | <zyklotomic> | but I'm guessing it's existence is legacy cruft |
| 06:27:17 | <n0042> | And you said ($) should be used sparingly? I have been using it willy-nilly on the assumption that people don't like parentheses as much as I do. What's the general guideline there? |
| 06:27:32 | <dsal> | If you're composing functions, use . |
| 06:27:53 | <zyklotomic> | when would you say it's acceptable to use $ |
| 06:28:05 | <dsal> | At the end of a bunch of .s :) |
| 06:28:27 | <n0042> | take 5 $ repeat 10 |
| 06:28:31 | <n0042> | or something like that |
| 06:28:38 | <n0042> | to avoid take 5 (repeat 10) ? |
| 06:28:43 | <dsal> | > replicate 5 10 |
| 06:28:45 | <lambdabot> | [10,10,10,10,10] |
| 06:29:02 | <dsal> | : take 5 . repeat |
| 06:29:07 | <dsal> | :t take 5 . repeat |
| 06:29:08 | <zyklotomic> | (take 5 . repeat) 10 hon oh you beat me to it |
| 06:29:09 | <lambdabot> | a -> [a] |
| 06:29:27 | <zyklotomic> | but it's not that much cleaner i'm gonna oh, wait ig you can put a $ instead of the paren |
| 06:29:40 | <dsal> | > take 5 . repeat $ 10 |
| 06:29:42 | <zyklotomic> | i'm clearly not a very good user of $ lol |
| 06:29:42 | <lambdabot> | [10,10,10,10,10] |
| 06:29:55 | <n0042> | Oh nice |
| 06:29:55 | <dsal> | Save yo # |
| 06:29:57 | <dsal> | Save yo $ |
| 06:29:58 | <dsal> | damnit |
| 06:30:12 | <n0042> | Okay I see how (.) works now |
| 06:30:21 | <zyklotomic> | i'm going to go out on a limb though and say that sometimes |
| 06:30:30 | <zyklotomic> | take 5 $ repeat 10 is just easier to read |
| 06:30:50 | <zyklotomic> | or my brain hasn't been molded enough |
| 06:31:21 | <dsal> | > let f = show . sum . take 5 . repeat in f 10 |
| 06:31:23 | <lambdabot> | "50" |
| 06:32:36 | <n0042> | For something a little different, do any of you know if it's true that last is an O(n) function? Like, if you wanted to use a list as a Queue, would it really be O(n) to call last to dequeue? |
| 06:32:46 | <dsal> | > let f = nub . sort show . sum . take 11 . repeat in f 13 |
| 06:32:48 | <lambdabot> | error: |
| 06:32:48 | <lambdabot> | • Couldn't match expected type ‘b -> [a2]’ with actual type ‘[a0]’ |
| 06:32:48 | <lambdabot> | • Possible cause: ‘sort’ is applied to too many arguments |
| 06:32:51 | <dsal> | stupid keyboard |
| 06:32:54 | <dsal> | > let f = nub . sort . show . sum . take 11 . repeat in f 13 |
| 06:32:57 | <lambdabot> | "134" |
| 06:32:58 | <n0042> | I sort of assumed that the built-in list object would have a tail pointer, but hoogle says that's O(n) |
| 06:33:17 | <dsal> | @src (:) |
| 06:33:17 | <lambdabot> | Source not found. Listen, broccoli brains, I don't have time to listen to this trash. |
| 06:33:20 | <dsal> | boooo |
| 06:33:26 | <dsal> | a list is just a head and a tail. |
| 06:33:29 | <n0042> | Whoah that bot has atittude |
| 06:34:02 | <dsal> | It's a cons list. You said you're familiar with lisp. |
| 06:34:14 | <n0042> | Right, a singly-linked list with a head pointer |
| 06:34:46 | <n0042> | So to get the last element you would have to traverse all the way down the list, hence O(n). |
| 06:34:48 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Remote host closed the connection) |
| 06:35:21 | <n0042> | But there's no reason you couldn't have the low-level logic include a tail pointer so that last is O(1). |
| 06:35:26 | <dsal> | Lists are great, but if you need other performance characteristics, there are better data structures. |
| 06:35:37 | <dsal> | There are many, many reasons you can't do that. |
| 06:35:42 | <dsal> | But if you disagree, write one. |
| 06:35:56 | <dsal> | Haskell has very little magic. You can write most of what you see. |
| 06:36:12 | <dsal> | Even many of the super fancy compiler optimizations are library-definable. |
| 06:37:04 | <n0042> | My plan was to use Data.Array but that seems kind of un-functional. What would you suggest? |
| 06:37:10 | × | mceier quits (~mceier@89-68-132-187.dynamic.chello.pl) (Ping timeout: 268 seconds) |
| 06:37:12 | <dsal> | Vector? |
| 06:37:16 | <dsal> | Seq? |
| 06:37:17 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 06:37:18 | <MarcelineVQ> | for what? |
| 06:37:28 | <n0042> | To simulate a Queue, or circular buffer |
| 06:38:03 | <dsal> | Lists are fine for many of these things, but there are specific structures. |
| 06:40:45 | <zyklotomic> | is it a bad practice to append to the front of a list instead tehn |
| 06:40:50 | <zyklotomic> | to get around the time complexity of ++ |
| 06:40:56 | <dsal> | It's the best. |
| 06:41:01 | <n0042> | Seems like the opposite. Bad practice to append to the rear |
| 06:41:04 | <dsal> | No better place to put something. |
| 06:41:13 | <dsal> | ++ is another one of those language warts. |
| 06:41:21 | <MarcelineVQ> | lists make pretty good queues in haskell https://rafal.io/posts/haskell-queues.html |
| 06:41:55 | <zyklotomic> | dsal: so lists make a pretty bad monoid? |
| 06:41:58 | <MarcelineVQ> | This doesn't explain super in depth, but the idea is to use two lists with one in reverse to create your queue |
| 06:42:15 | <dsal> | zyklotomic: ++ vs. <> |
| 06:42:19 | <n0042> | Thank you very much |
| 06:42:22 | <dsal> | lists are fine for what they do |
| 06:42:23 | → | mceier joins (~mceier@89-68-132-187.dynamic.chello.pl) |
| 06:42:47 | → | shangxiao joins (~davids@101.181.159.140) |
| 06:43:21 | <MarcelineVQ> | There's a lot of queue-like things around though so you'd probably just want to use whatever and optommize later, Seq that dsal mentioned is a fair all-around option for accessing either end of. |
| 06:44:02 | <n0042> | Oh wow, Haskell has built-ins for everything |
| 06:44:12 | <dsal> | built-in? |
| 06:44:52 | <n0042> | Stuff you don't have to roll on your own. |
| 06:45:02 | <MarcelineVQ> | dsal: people who don't already know don't know what you mean when you say you don't like map and ++. They won't realize you mean you don't like that there's both fmap and map and just want one, or relatedly that ++ and <> are the same for lists so just <> is fine |
| 06:45:12 | <dsal> | Oh. Not built-in, just already implemented.. |
| 06:45:22 | <n0042> | Yes, thank you |
| 06:45:35 | → | Stanley|00 joins (~stanley00@unaffiliated/stanley00) |
| 06:45:46 | <dsal> | MarcelineVQ: that's true. People should understand me better. heh |
| 06:46:02 | <n0042> | You've both been very helpful, thank you. |
| 06:46:24 | × | jlamothe quits (~jlamothe@198.251.55.207) (Ping timeout: 260 seconds) |
| 06:46:48 | <dsal> | The functional data structure stuff is amazing. That queue thing was amazing to see. |
| 06:47:34 | <zyklotomic> | MarcelineVQ: wait, I don't think ++ and <> are the same |
| 06:47:41 | <dsal> | :t (++) |
| 06:47:42 | <lambdabot> | [a] -> [a] -> [a] |
| 06:47:44 | <dsal> | :t (<>) |
| 06:47:45 | <lambdabot> | Semigroup a => a -> a -> a |
| 06:47:49 | <MarcelineVQ> | The okasaki paper is a bit of a hard read if you're new to it all but it's pretty great, interesting how little progress there's been since it at as well |
| 06:47:51 | <zyklotomic> | which was what dsal meant |
| 06:48:10 | <dsal> | ++ doesn't need to exist in Haskell. Or, perhaps, <> should be ++ |
| 06:48:17 | <dsal> | Same as map vs. fmap |
| 06:48:56 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 240 seconds) |
| 06:49:04 | <MarcelineVQ> | Where your Semigroup is [a] then <> = ++ |
| 06:49:33 | <zyklotomic> | <> should be ++ i think |
| 06:49:43 | <zyklotomic> | ++ looks more natural |
| 06:50:02 | <zyklotomic> | idk about fmap vs map though if you had to pick one of the two |
| 06:50:15 | × | Stanley|00 quits (~stanley00@unaffiliated/stanley00) (Remote host closed the connection) |
| 06:50:30 | <dsal> | Sure. It's just one of those things that is too much legacy code. |
| 06:50:31 | <zyklotomic> | MarcelineVQ: I meant the implementation, I'm not sure if they behave the same |
| 06:50:40 | <zyklotomic> | I get that they're isomorphic |
| 06:50:50 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 06:50:53 | <dsal> | How could they behave differently? |
| 06:50:53 | <zyklotomic> | mconcat xss = [x | xs <- xss, x <- xs] |
| 06:51:05 | <zyklotomic> | (++) [] ys = ys |
| 06:51:07 | <zyklotomic> | (++) (x:xs) ys = x : xs ++ ys |
| 06:51:19 | <dsal> | @quick \l1 l2 -> (l1 ++ l2) === (l1 <> l2) |
| 06:51:19 | <lambdabot> | Not enough privileges |
| 06:51:31 | <dsal> | @check \l1 l2 -> (l1 ++ l2) === (l1 <> l2) |
| 06:51:33 | <lambdabot> | +++ OK, passed 100 tests. |
| 06:51:33 | <MarcelineVQ> | That is the implementation :> http://hackage.haskell.org/package/base-4.14.0.0/docs/src/GHC.Base.html#line-306 |
| 06:52:00 | <zyklotomic> | my bad im barking up the wrong tree |
| 06:52:12 | <zyklotomic> | I looked into Data.Monoid |
| 06:53:48 | <zyklotomic> | wait so that wasnt disagreeing with lists being a somewhat inefficient monoid then |
| 06:54:05 | <n0042> | So when I asked about lists with tail-pointers dsal said "There are many, many reasons you can't do that." I have implemented a few linked lists in C and I've done some LISPing, but I'm far from an expert. I would be interested in hearing some of those reasons. Is it a performance thing, from the days of yore? Thanks again for answering my |
| 06:54:05 | <n0042> | questions. You folks are all very helpful. |
| 06:54:57 | <n0042> | I've learned more just hanging out in here for an hour than in the last two days combined. You guys are great. |
| 06:55:37 | <glguy> | n0042, the issue is that things aren't mutable, so you can't use a reference to the last element to add to the end of a list |
| 06:56:04 | <glguy> | Unless you build a mutable structure explicitly with mutable references that's accessed using IO actions |
| 06:56:27 | → | mananamenos joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 06:56:56 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Ping timeout: 240 seconds) |
| 06:57:25 | <zyklotomic> | I was also thinking, what about [1..] |
| 06:58:00 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-104-55.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 06:58:02 | × | borne quits (~fritjof@200116b864eda200f1dc39039d201adf.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 06:58:04 | <dsal> | let a = 1:a in take 5 a |
| 06:58:09 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 06:58:10 | <dsal> | > let a = 1:a in take 5 a |
| 06:58:12 | <lambdabot> | [1,1,1,1,1] |
| 06:59:17 | <dsal> | > let a = 'x':a in length a |
| 06:59:24 | <lambdabot> | mueval: ExitFailure 1 |
| 06:59:29 | <dsal> | boo. Too many exes. |
| 06:59:44 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Remote host closed the connection) |
| 07:00:10 | <MarcelineVQ> | how many, would you say? |
| 07:00:11 | <dsal> | n0042: A lot of these questions get a lot easier when you try to do the thing you think is probably easy. :) |
| 07:00:27 | × | alp quits (~alp@2a01:e0a:58b:4920:d4c7:761f:e715:72ea) (Ping timeout: 272 seconds) |
| 07:01:13 | <n0042> | That's good advice in general, for sure |
| 07:01:24 | <dsal> | > let a = 'x':a in take 5 (a <> "and then y") |
| 07:01:26 | <lambdabot> | "xxxxx" |
| 07:02:10 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 07:02:18 | <dsal> | I just made a list of infinite length and appended a list to the end of it. Please adjust pointers accordingly. :) |
| 07:06:59 | → | idhugo joins (~idhugo@80-62-116-101-mobile.dk.customer.tdc.net) |
| 07:07:11 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 07:08:02 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 07:08:17 | <n0042> | Is the `<> "and then y"` part ever evaluated? |
| 07:09:02 | → | actuallybatman joins (~sam@S010664777dafd303.cg.shawcable.net) |
| 07:09:06 | <n0042> | lazy evaluation is pretty wild. I'm still trying to wrap my head around that part. |
| 07:09:34 | → | solonarv joins (~solonarv@astrasbourg-653-1-156-4.w90-6.abo.wanadoo.fr) |
| 07:09:54 | × | LKoen quits (~LKoen@169.244.88.92.rev.sfr.net) (Remote host closed the connection) |
| 07:10:59 | <ClaudiusMaximus> | n0042: it's evaluated, just enough to push it down 5 cells: (x : xs) <> ys = x : (xs <> ys) happens 5 times during the evaluation of the result, after which take drops it |
| 07:13:27 | × | zyklotomic quits (~ethan@unaffiliated/chocopuff) (Quit: WeeChat 2.9) |
| 07:14:52 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 07:15:04 | × | idhugo quits (~idhugo@80-62-116-101-mobile.dk.customer.tdc.net) (Quit: Leaving) |
| 07:15:40 | <n0042> | Yeah, I have no idea how you'd do the pointers for that. That's a mind-bender. |
| 07:16:10 | <dsal> | It's really easy to follow if you don't try to think about how you'd write it as a singly linked list in C. |
| 07:16:32 | <n0042> | Conditioning is hard to break '=D |
| 07:16:44 | <n0042> | But thank you for bearing with me. I really appreciate it |
| 07:17:10 | <dsal> | What is `a`? It's a list where the head is 'x' and the tail is some other stuff. If you only need the head, you're done. If you need the tail, you look at that. Oh, it's `a, that's a list where... |
| 07:18:39 | × | alx741 quits (~alx741@181.196.68.148) (Ping timeout: 265 seconds) |
| 07:19:03 | → | Amras joins (~Amras@unaffiliated/amras0000) |
| 07:21:16 | → | chaosmasttter joins (~chaosmast@p200300c4a70b2a01441f1455f36b3658.dip0.t-ipconnect.de) |
| 07:21:33 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:23:51 | × | sfvm quits (~sfvm@37.228.215.148) (Remote host closed the connection) |
| 07:25:08 | → | p8m_ joins (p8m@gateway/vpn/protonvpn/p8m) |
| 07:26:32 | × | p8m quits (p8m@gateway/vpn/protonvpn/p8m) (Ping timeout: 272 seconds) |
| 07:27:41 | <n0042> | If I replace `take 5` with `tail` that sequence generates `x`s forever. That is wild. |
| 07:30:50 | → | acidjnk_new joins (~acidjnk@p200300d0c719ff57608036dc958592ad.dip0.t-ipconnect.de) |
| 07:31:16 | → | alx741 joins (~alx741@181.196.68.156) |
| 07:32:21 | → | dan64- joins (~dan64@dannyadam.com) |
| 07:32:52 | <dsal> | @src tail |
| 07:32:52 | <lambdabot> | tail (_:xs) = xs |
| 07:32:52 | <lambdabot> | tail [] = error "Prelude.tail: empty list" |
| 07:34:49 | × | dan64 quits (~dan64@dannyadam.com) (Ping timeout: 256 seconds) |
| 07:34:59 | <dsal> | :t tail . tail . tail |
| 07:35:01 | <lambdabot> | [a] -> [a] |
| 07:35:16 | → | dhouthoo joins (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be) |
| 07:35:47 | <dsal> | Or you could `drop ∞` and get to that appended bit. |
| 07:36:01 | <dsal> | @src drop |
| 07:36:01 | <lambdabot> | drop n xs | n <= 0 = xs |
| 07:36:01 | <lambdabot> | drop _ [] = [] |
| 07:36:01 | <lambdabot> | drop n (_:xs) = drop (n-1) xs |
| 07:36:13 | <dsal> | drop isn't partial. |
| 07:36:26 | <dsal> | I wonder why `tail` isn't `drop 1` |
| 07:36:41 | <dsal> | @check \l -> tail l === drop 1 l |
| 07:36:43 | <lambdabot> | *Exception: Prelude.tail: empty list |
| 07:36:55 | <dsal> | 👍 |
| 07:37:11 | <n0042> | That's what I was trying to do. I was trying to see what I could put in there to get to the appended part |
| 07:37:12 | <dsal> | Partial functions aren't awesome. |
| 07:37:33 | <dsal> | It's an infinitely long list, do you'd have to drop infinite items first. |
| 07:39:47 | <n0042> | I was trying to get a better grip on the "let" and "in" syntax earlier today, and that was a pretty useful practical example. Thank you. |
| 07:42:11 | → | SourOatMilk joins (SourOatMil@gateway/vpn/protonvpn/souroatmilk) |
| 07:42:12 | <dsal> | This is one of the things I like about the book mentioned earlier. If you think about eager evaluation in C or something, you'll find haskell confusing. If you stop pretending you know things, it'll make a lot more sense. |
| 07:42:25 | × | Sgeo quits (~Sgeo@ool-18b982ad.dyn.optonline.net) (Read error: Connection reset by peer) |
| 07:42:59 | <dsal> | (also worth noting that list isn't mentioned for like, several chapters, and you make it yourself) |
| 07:43:03 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 07:44:23 | <n0042> | That sounds pretty intense |
| 07:44:29 | <n0042> | I'll check it out for sure |
| 07:44:33 | <dsal> | No, there's nothing very special about it. |
| 07:44:54 | <dsal> | There are three or four books you can read and end up finding haskell is actually pretty boring and doesn't have a lot of magic. |
| 07:45:14 | <dsal> | It's just that most other languages are worse and don't give the user much power or ability to generalize things. |
| 07:46:14 | <dsal> | @let data MyList a = Item a | EOL deriving Show |
| 07:46:16 | <lambdabot> | .L.hs:162:1: error: |
| 07:46:16 | <lambdabot> | Multiple declarations of ‘MyList’ |
| 07:46:16 | <lambdabot> | Declared at: .L.hs:158:1 |
| 07:46:31 | × | Flonk quits (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com) (Ping timeout: 246 seconds) |
| 07:46:34 | <n0042> | The things that I really like about it so far are the amazing REPL, the list comprehensions, and recursion-friendly syntax. It's just really easy to write most things I want to write. Except I/O, but I'll get there. |
| 07:46:39 | <dsal> | Er. Ignore the error. That's basically List, plus a few other things (and a slightly fancier Show) |
| 07:46:48 | <dibblego> | Maybe |
| 07:47:13 | <dsal> | er, I messed that up anyway |
| 07:47:38 | × | bob_twinkles quits (~quassel@ec2-52-37-66-13.us-west-2.compute.amazonaws.com) (Quit: No Ping reply in 180 seconds.) |
| 07:47:53 | → | bob_twinkles joins (~quassel@ec2-52-37-66-13.us-west-2.compute.amazonaws.com) |
| 07:48:03 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Ping timeout: 240 seconds) |
| 07:48:28 | <dsal> | @let data MyList a = Item a (MyList a) | EOL deriving Show |
| 07:48:29 | <lambdabot> | Defined. |
| 07:48:30 | → | Flonk joins (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com) |
| 07:48:50 | × | clog quits (~nef@bespin.org) (Ping timeout: 256 seconds) |
| 07:49:05 | <dsal> | > let a = Item 'x' a in a |
| 07:49:07 | <lambdabot> | Item 'x' (Item 'x' (Item 'x' (Item 'x' (Item 'x' (Item 'x' (Item 'x' (Item '... |
| 07:49:44 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 07:51:13 | <dsal> | > let mytake _ EOL = EOL; mytake 0 _ = EOL; mytake n (Item x l) = Item x (mytake (n-1) l); a = Item 'x' a in mytake 3 a |
| 07:51:15 | <lambdabot> | Item 'x' (Item 'x' (Item 'x' EOL)) |
| 07:51:18 | × | jedws quits (~jedws@101.184.150.93) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 07:51:57 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 07:55:29 | → | coot joins (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) |
| 07:58:33 | → | coco joins (~coco@212-51-146-87.fiber7.init7.net) |
| 07:58:40 | <dsal> | @let instance Foldable MyList where foldMap _ EOL = mempty; foldMap f (Item a l) = f a <> foldMap f l |
| 07:58:41 | <lambdabot> | Defined. |
| 07:58:55 | <dsal> | > toList (Item 1 (Item 2 (Item 3 EOL))) |
| 07:58:57 | <lambdabot> | error: |
| 07:58:57 | <lambdabot> | Ambiguous occurrence ‘toList’ |
| 07:58:57 | <lambdabot> | It could refer to |
| 07:59:05 | <dsal> | > sum (Item 1 (Item 2 (Item 3 EOL))) |
| 07:59:08 | <lambdabot> | 6 |
| 07:59:11 | <dsal> | woo |
| 07:59:20 | → | kritzefitz joins (~kritzefit@fw-front.credativ.com) |
| 07:59:22 | <n0042> | nice |
| 07:59:42 | × | SourOatMilk quits (SourOatMil@gateway/vpn/protonvpn/souroatmilk) (Quit: leaving) |
| 08:00:02 | <dsal> | :t fmap |
| 08:00:06 | <lambdabot> | Functor f => (a -> b) -> f a -> f b |
| 08:01:15 | <dsal> | @let instance Functor MyList where fmap _ EOL = EOL; fmap f (Item x l) = Item (f x) (fmap f l) |
| 08:01:17 | <lambdabot> | Defined. |
| 08:01:42 | <dsal> | > (2 ^) <$> Item 1 (Item 2 (Item 3 EOL)) |
| 08:01:44 | <lambdabot> | Item 2 (Item 4 (Item 8 EOL)) |
| 08:03:40 | <dsal> | Throw in monoid, monad, applicative, and probably a few other things and that's basically list. |
| 08:06:20 | → | chele joins (~chele@ip5b416ea2.dynamic.kabel-deutschland.de) |
| 08:07:10 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 08:09:08 | <n0042> | From the POV of someone who's still pretty new to the language, that's impressive stuff. |
| 08:15:07 | → | jedws joins (~jedws@101.184.150.93) |
| 08:16:26 | <dsal> | n0042: It gets cooler. e.g. |
| 08:16:44 | <dsal> | % [1, 2, 3] :: MyList Int |
| 08:16:44 | <yahb> | dsal: Item 1 (Item 2 (Item 3 EOL)) |
| 08:16:47 | → | LKoen joins (~LKoen@169.244.88.92.rev.sfr.net) |
| 08:16:59 | <dsal> | I taught yahb how to understand my list from normal list syntax. |
| 08:17:26 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 08:17:35 | <dsal> | % sum ([1..100] :: MyList Int) |
| 08:17:36 | <yahb> | dsal: ; <interactive>:1:18: error:; Not in scope: type constructor or class `MyList'; Perhaps you meant one of these: `IsList' (imported from GHC.Exts), `TyLit' (imported from Language.Haskell.TH) |
| 08:17:46 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Client Quit) |
| 08:17:47 | × | keep_learning quits (~keep_lear@43.231.26.152) (Quit: Leaving) |
| 08:18:13 | <dsal> | Someone else taught it how to not know that, apparently. heh |
| 08:19:53 | <dsal> | n0042: Anyway, I should've gone to bed a while ago. The main point is that haskell doesn't reserve a lot of magic for the ivory tower. If you see something that looks magical, you can often implement it yourself from scratch. |
| 08:20:04 | → | alp joins (~alp@2a01:e0a:58b:4920:6cd6:5f96:4d6d:5a5) |
| 08:20:33 | <n0042> | That's good to know! Thanks for all the help. I am planning on going through that book with a study group, so I'm looking forward to it. |
| 08:20:44 | <n0042> | Have a good night and thanks again |
| 08:20:58 | <dsal> | (e.g., I could've made a Show instance that displayed my list exactly as regular list does, making it look and and act just like the list you already know) |
| 08:21:48 | <dsal> | It's like learning Santa Claus isn't real. All this wonderful magic is suddenly boring, but then you get to be Santa Claus, so that's nice. |
| 08:21:50 | <dsal> | 'night. :) |
| 08:24:28 | → | Franciman joins (~francesco@host-82-56-223-169.retail.telecomitalia.it) |
| 08:29:06 | ← | n0042 parts (d055ed89@208.85.237.137) () |
| 08:31:09 | → | thc202 joins (~thc202@unaffiliated/thc202) |
| 08:34:35 | → | frogger joins (d055ed89@208.85.237.137) |
| 08:35:16 | → | mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) |
| 08:36:24 | → | ph88^ joins (~ph88@2a02:8109:9e00:7e5c:f073:c081:c2ef:433b) |
| 08:40:31 | × | ph88 quits (~ph88@2a02:8109:9e00:7e5c:a963:461:83fa:2c4) (Ping timeout: 272 seconds) |
| 08:45:18 | × | jedws quits (~jedws@101.184.150.93) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 08:45:38 | → | borne joins (~fritjof@200116b864eda200f1dc39039d201adf.dip.versatel-1u1.de) |
| 08:46:09 | × | frogger quits (d055ed89@208.85.237.137) (Remote host closed the connection) |
| 08:46:54 | → | danvet joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) |
| 08:48:06 | → | n0042 joins (d055ed89@208.85.237.137) |
| 08:48:30 | hackage | mu-rpc 0.4.0.1 - Protocol-independent declaration of services and servers. https://hackage.haskell.org/package/mu-rpc-0.4.0.1 (AlejandroSerrano) |
| 08:49:25 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 08:50:47 | → | danvet_ joins (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) |
| 08:51:25 | → | Boomerang joins (~Boomerang@xd520f68c.cust.hiper.dk) |
| 08:51:52 | <unclechu> | glguy: no i am around, why? |
| 08:53:07 | → | Yumasi joins (~guillaume@2a01cb09b06b29ea0877e1bda345185b.ipv6.abo.wanadoo.fr) |
| 08:53:17 | → | Ariakenom joins (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) |
| 08:54:00 | hackage | compendium-client 0.2.1.1 - Client for the Compendium schema server https://hackage.haskell.org/package/compendium-client-0.2.1.1 (AlejandroSerrano) |
| 08:54:04 | × | hnOsmium0001 quits (uid453710@gateway/web/irccloud.com/x-rpvaqdolaahudqno) (Quit: Connection closed for inactivity) |
| 08:55:24 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 08:57:00 | hackage | mu-avro 0.4.0.2 - Avro serialization support for Mu microservices https://hackage.haskell.org/package/mu-avro-0.4.0.2 (AlejandroSerrano) |
| 08:58:11 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 08:58:29 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Client Quit) |
| 08:59:00 | hackage | mu-protobuf 0.4.0.2 - Protocol Buffers serialization and gRPC schema import for Mu microservices https://hackage.haskell.org/package/mu-protobuf-0.4.0.2 (AlejandroSerrano) |
| 08:59:17 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 09:00:31 | hackage | mu-optics 0.3.0.1 - Optics for @mu-schema@ terms https://hackage.haskell.org/package/mu-optics-0.3.0.1 (AlejandroSerrano) |
| 09:01:31 | hackage | mu-persistent 0.3.1.0 - Utilities for interoperation between Mu and Persistent https://hackage.haskell.org/package/mu-persistent-0.3.1.0 (AlejandroSerrano) |
| 09:02:31 | hackage | mu-grpc-client 0.4.0.1 - gRPC clients from Mu definitions https://hackage.haskell.org/package/mu-grpc-client-0.4.0.1 (AlejandroSerrano) |
| 09:04:31 | hackage | mu-graphql 0.4.1.0 - GraphQL support for Mu https://hackage.haskell.org/package/mu-graphql-0.4.1.0 (AlejandroSerrano) |
| 09:06:56 | → | watt801 joins (~watt801@124.123.105.47) |
| 09:07:23 | × | n0042 quits (d055ed89@208.85.237.137) (Remote host closed the connection) |
| 09:08:26 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 09:10:09 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 09:10:23 | laxask | is now known as sudden |
| 09:10:24 | <idnar> | :t \a -> a <> a |
| 09:10:26 | <lambdabot> | Semigroup a => a -> a |
| 09:10:35 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Quit: mputz) |
| 09:11:30 | × | watt801 quits (~watt801@124.123.105.47) (Ping timeout: 256 seconds) |
| 09:13:28 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 09:13:52 | <idnar> | I guess that's `stimes 2` |
| 09:14:04 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 09:17:18 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 09:17:32 | <avn> | Folks, anyone could hint me some examples of usage for aside/outside/without from Control.Lens.Prisms? |
| 09:20:22 | × | rotty quits (rotty@ghost.xx.vu) (Ping timeout: 260 seconds) |
| 09:23:33 | → | jakob_ joins (~textual@p200300f49f162200c400a7daff5c73c4.dip0.t-ipconnect.de) |
| 09:26:20 | → | kuribas joins (~user@ptr-25vy0i8y4kl4v762twz.18120a2.ip6.access.telenet.be) |
| 09:27:19 | <jophish> | bgamari: is your ring-buffer library worth using? |
| 09:27:31 | <jophish> | It doesn't build at the moment, but I think that's just version bounds |
| 09:30:21 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 09:31:10 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 09:31:27 | × | sagax quits (~sagax_nb@213.138.71.146) (Ping timeout: 260 seconds) |
| 09:34:55 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 09:35:36 | → | ADG1089 joins (~adg1089@223.235.75.84) |
| 09:36:29 | <ADG1089> | @hoogle (FilePath -> IO ()) -> IO [FilePath] -> IO () |
| 09:36:30 | <lambdabot> | Data.Drinkery.Combinators traverseFrom_ :: (Foldable t, Monad m) => m (t a) -> (a -> m b) -> m () |
| 09:36:36 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Remote host closed the connection) |
| 09:36:59 | <ADG1089> | @ty mapM |
| 09:37:01 | <lambdabot> | (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) |
| 09:37:28 | → | Lycurgus joins (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) |
| 09:37:55 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 09:38:08 | × | phaul quits (~phaul@ruby/staff/phaul) (Ping timeout: 256 seconds) |
| 09:38:53 | × | nckx quits (~nckx@tobias.gr) (Quit: Updating my Guix System — https://guix.gnu.org) |
| 09:39:31 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 09:40:00 | → | phaul joins (~phaul@ruby/staff/phaul) |
| 09:41:33 | → | nckx joins (~nckx@tobias.gr) |
| 09:43:02 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 09:43:16 | <boxscape> | % type family Fam :: a :~: b where |
| 09:43:16 | <yahb> | boxscape: |
| 09:43:19 | <boxscape> | % :kind Fam |
| 09:43:20 | <yahb> | boxscape: forall k (a :: k) (b :: k). a :~: b |
| 09:44:16 | <boxscape> | % type family Fam :: a :~: b where Fam = 'Refl |
| 09:44:16 | <yahb> | boxscape: ; <interactive>:24:26: error:; * Couldn't match `a' with `b'; * In the type family declaration for `Fam' |
| 09:44:25 | <boxscape> | % type Fam :: forall k (a :: k) (b :: k) . a :~: b; type family Fam :: a :~: b where Fam = 'Refl |
| 09:44:26 | <yahb> | boxscape: |
| 09:44:31 | → | clog joins (~nef@bespin.org) |
| 09:44:34 | <boxscape> | the inferred kind seems to be the same one I gave it |
| 09:44:41 | <boxscape> | why does it result in an error without type sig? |
| 09:44:44 | <boxscape> | (kind sig) |
| 09:45:22 | <boxscape> | ohh wait |
| 09:45:31 | <boxscape> | is the Refl call changing the inferred kind |
| 09:46:04 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 09:46:40 | <idnar> | jophish: last time I tried to use it, I got segfaults |
| 09:48:25 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 09:48:53 | <idnar> | @type \f x -> traverse_ f =<< x |
| 09:48:54 | <lambdabot> | (Monad m, Foldable t) => (a -> m b) -> m (t a) -> m () |
| 09:49:10 | <idnar> | ADG1089: ^ |
| 09:49:34 | <ADG1089> | Thansk!! |
| 09:50:52 | × | danvet_ quits (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) (Quit: Leaving) |
| 09:54:25 | × | LKoen quits (~LKoen@169.244.88.92.rev.sfr.net) (Remote host closed the connection) |
| 10:01:12 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 260 seconds) |
| 10:02:10 | → | Zetagon joins (~leo@c151-177-52-233.bredband.comhem.se) |
| 10:04:16 | → | chalkmonster joins (~chalkmons@unaffiliated/chalkmonster) |
| 10:06:38 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:07:30 | hackage | jsonifier 0.1.0.5 - Fast and simple JSON encoding toolkit https://hackage.haskell.org/package/jsonifier-0.1.0.5 (NikitaVolkov) |
| 10:07:33 | → | thc202 joins (~thc202@unaffiliated/thc202) |
| 10:08:10 | → | jonatanb joins (jonatanb@gateway/vpn/protonvpn/jonatanb) |
| 10:15:25 | × | jonatanb quits (jonatanb@gateway/vpn/protonvpn/jonatanb) (Ping timeout: 240 seconds) |
| 10:16:18 | → | zyextant joins (~zyextant@120.155.30.153) |
| 10:16:21 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 10:18:07 | × | ben_m quits (~ben_m@unaffiliated/ben-m/x-8385872) (Quit: ZNC 1.7.5 - https://znc.in) |
| 10:18:12 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 10:19:33 | × | guest1119 quits (~user@49.5.6.87) (Quit: ERC (IRC client for Emacs 27.1)) |
| 10:20:52 | → | ben_m joins (~ben_m@56.ip-51-38-127.eu) |
| 10:22:16 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 10:24:41 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 10:26:38 | → | nerded joins (~user@lfbn-idf3-1-374-154.w83-199.abo.wanadoo.fr) |
| 10:26:53 | <nerded> | hi guys |
| 10:27:29 | <Zetagon> | Hello |
| 10:28:10 | → | ubert joins (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) |
| 10:28:31 | × | ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Remote host closed the connection) |
| 10:29:18 | → | patier[m] joins (patiermatr@gateway/shell/matrix.org/x-defohognfbqcqriu) |
| 10:29:43 | × | nerded quits (~user@lfbn-idf3-1-374-154.w83-199.abo.wanadoo.fr) (Client Quit) |
| 10:32:01 | → | ubert joins (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) |
| 10:32:14 | → | mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) |
| 10:32:16 | × | rprije quits (~rprije@124.148.131.132) (Ping timeout: 240 seconds) |
| 10:34:16 | → | fendor joins (~fendor@178.165.131.185.wireless.dyn.drei.com) |
| 10:36:05 | × | fendor_ quits (~fendor@178.165.128.131.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
| 10:36:37 | <jophish> | idnar: cool, thanks |
| 10:36:47 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 10:41:05 | × | ben_m quits (~ben_m@56.ip-51-38-127.eu) (Quit: ZNC 1.7.5 - https://znc.in) |
| 10:41:25 | → | zyklotomic joins (~ethan@unaffiliated/chocopuff) |
| 10:43:25 | × | stree quits (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) (Quit: Caught exception) |
| 10:43:25 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Remote host closed the connection) |
| 10:43:42 | → | stree joins (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) |
| 10:44:48 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 10:46:01 | <bgamari> | jophish, frankly I would need to check |
| 10:46:10 | <bgamari> | jophish, it was a long time ago that I wrote that |
| 10:46:16 | <bgamari> | and I had very particular needs |
| 10:47:10 | ← | ADG1089 parts (~adg1089@223.235.75.84) () |
| 10:48:38 | <dminuoso> | What's the motivation behind: data :~: where Refl :: a :~: a |
| 10:48:50 | <dminuoso> | Err |
| 10:49:00 | <dminuoso> | data a :~: b where Refl :: a :~: a |
| 10:49:14 | <Franciman> | Hi, does happy have some functionality for writing pratt parsers? |
| 10:49:24 | <dminuoso> | I keep staring at this, not quite understanding how this works or what this is for. |
| 10:50:25 | <Franciman> | dminuoso, the motivation is that you can say that two things are the same, when they are the same |
| 10:50:26 | <Franciman> | :P |
| 10:50:47 | <Franciman> | so that you surely want to conclude a = a |
| 10:51:53 | <kuribas> | I am wondering, would namedFieldPuns be prefered over RecordWildCards? |
| 10:51:57 | <dminuoso> | Does GHC bury a (a ~ b) into the GADT? |
| 10:52:20 | <kuribas> | RecordWildCards add hidden fields to the namespace, but namedFieldPuns make them visible. |
| 10:52:21 | <dminuoso> | % import Data.Type.Equality |
| 10:52:22 | <yahb> | dminuoso: |
| 10:52:27 | <dminuoso> | % :t Refl |
| 10:52:27 | <yahb> | dminuoso: forall k (a :: k). a :~: a |
| 10:52:36 | <boxscape> | dminuoso as far as I know it does |
| 10:52:38 | <boxscape> | or wait |
| 10:52:43 | <boxscape> | I thought you wrote a ~ a |
| 10:53:03 | <boxscape> | Oh nevermind |
| 10:53:11 | <boxscape> | a ~ a wouldn't make sense |
| 10:53:20 | <dminuoso> | Well, a ~ a necessarily holds true, no? |
| 10:53:25 | <boxscape> | so yes, as far as I know it does put a ~ b into the GADT |
| 10:53:32 | <boxscape> | dminuoso right, that's what I meant |
| 10:53:55 | <dminuoso> | The above type signature seems strange, Id have expected it to we |
| 10:53:59 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Remote host closed the connection) |
| 10:54:15 | <dminuoso> | Refl :: forall a b. (a ~ b) => a :~: b |
| 10:54:20 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 10:54:22 | <dminuoso> | (ignoring the PolyKinds noise) |
| 10:54:45 | <boxscape> | % :t undefined :: forall a b . (a ~ b) => a :~: b |
| 10:54:45 | <yahb> | boxscape: forall k (b :: k). b :~: b |
| 10:54:53 | <boxscape> | dminuoso same thing |
| 10:54:54 | × | jwynn6 quits (~jwynn6@050-088-122-078.res.spectrum.com) (Ping timeout: 272 seconds) |
| 10:55:36 | → | jwynn6 joins (~jwynn6@050-088-122-078.res.spectrum.com) |
| 10:55:49 | → | zyxtant joins (~zyextant@120.155.30.153) |
| 10:57:07 | <dminuoso> | So Refl is just a reified ~ constraint? |
| 10:57:18 | <boxscape> | yes |
| 10:58:00 | <dminuoso> | im genuinely curious what this could be used for then |
| 10:59:14 | <boxscape> | dminuoso to show that things are equal, for example, if you had data Nat = Z | S Nat, and defined plus for it, you could have plus_comm :: forall (n :: Nat) (m :: Nat) . Plus n m :~: Plus m n |
| 10:59:20 | × | zyextant quits (~zyextant@120.155.30.153) (Ping timeout: 272 seconds) |
| 10:59:31 | <boxscape> | and the proof would contain 2 or 3 Refls |
| 11:00:12 | <dminuoso> | 2 or 3 Refls? |
| 11:00:51 | × | kuribas quits (~user@ptr-25vy0i8y4kl4v762twz.18120a2.ip6.access.telenet.be) (Read error: Connection reset by peer) |
| 11:01:31 | × | zyklotomic quits (~ethan@unaffiliated/chocopuff) (Quit: WeeChat 2.9) |
| 11:01:35 | <boxscape> | as in, the Refl constructor would appear in the proof two or three times - as the base case for the induction (though actually you need to add singleton arguments here I think to match on) |
| 11:02:07 | → | kuribas joins (~user@ptr-25vy0i8y4kl4v762twz.18120a2.ip6.access.telenet.be) |
| 11:03:18 | <boxscape> | so if you also had data SNat :: Nat -> Type where SZ :: SNat Z | SS :: SNat n -> SNat (S n), i.e. the singleton type for Nat, you could have plus_comm :: SNat n -> SNat m -> Plus n m :~: Plus m n, and then the first equation, the inductive base case, could be plus_comm SZ n = Refl |
| 11:03:59 | <boxscape> | assuming Plus is defined as type family Plus n m where Plus Z m = m; Plus (S n) m = S (Plus n m) |
| 11:06:39 | → | ft joins (~ft@shell.chaostreff-dortmund.de) |
| 11:07:25 | × | chalkmonster quits (~chalkmons@unaffiliated/chalkmonster) (Quit: WeeChat 2.9) |
| 11:07:58 | → | zyklotomic joins (~ethan@unaffiliated/chocopuff) |
| 11:08:30 | hackage | hadolint 1.19.0 - Dockerfile Linter JavaScript API https://hackage.haskell.org/package/hadolint-1.19.0 (lorenzo) |
| 11:08:46 | <zyklotomic> | soft question here, is there a reason behind the ". . . $" style? I think it's part of "point-free" style? but I might be wrong |
| 11:09:17 | <boxscape> | (technically that base case isn't quite correct but let me write up the example real quick) |
| 11:09:39 | <zyklotomic> | like just now, I wrote something like `drop 1 . foldl' f [a, start] $ xs`, but I honenstly find this style more difficult to read than `drop 1 $ foldl' f [a, start] $ xs` |
| 11:10:31 | <zyklotomic> | * in the second one, the second $ was a typo / extraneous |
| 11:10:50 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:13:02 | <dminuoso> | zyklotomic: It's personal taste, some people like: . . . $, others prefer (. . .) (. . .), and there's other styles too |
| 11:13:20 | × | ft quits (~ft@shell.chaostreff-dortmund.de) (Ping timeout: 260 seconds) |
| 11:13:48 | <dminuoso> | I tend to avoid ($) generally except for do blocks/lambdas (cant get myself to enable BlockArguments) |
| 11:15:26 | <dminuoso> | In my opinion it's good to use function composition and parens. It gives you a better view on code structure |
| 11:15:28 | <kuribas> | dminuoso: so do you write (f . g . h) x then? |
| 11:16:03 | <dminuoso> | kuribas: Generally I favor `... f x where f = g . h . i` |
| 11:16:21 | × | datajerk quits (~datajerk@sense.net) (Remote host closed the connection) |
| 11:16:26 | kuribas | wonders if he writes everything infix his lisp colleages will like haskell more... |
| 11:16:28 | <dminuoso> | but `f (g (h x))` is not bad either |
| 11:16:35 | kuribas | means prefix |
| 11:16:44 | <dminuoso> | It's somewhat situational |
| 11:16:46 | → | datajerk joins (~datajerk@sense.net) |
| 11:16:49 | <kuribas> | dminuoso: lispers agree :) |
| 11:16:55 | <kuribas> | dminuoso: but clojurers not |
| 11:17:12 | <zyklotomic> | ah i see |
| 11:17:15 | <zyklotomic> | thanks for sharing |
| 11:17:28 | <zyklotomic> | i've been generally writing (f . g . h) x too |
| 11:17:37 | <zyklotomic> | and $ felt a bit unnatural at first |
| 11:17:54 | <kuribas> | clojurers write (-> x h g f). IMO it's strictly worse than ($) or (.), as it is a syntactic, rather than semantic construct. |
| 11:18:30 | <dminuoso> | zyklotomic: Using function composition brings functions as first class objects more into view |
| 11:18:43 | <dminuoso> | Say `fmap (f . g) ...` |
| 11:18:51 | <kuribas> | zyklotomic: I think the reasoning behidn . . . $ is that if you remove the last argument it still works. |
| 11:19:14 | <dminuoso> | (You could call this "point-free", but often its useful to think of functions as pipelines you can just compose to do more complex things) |
| 11:19:15 | <boxscape> | dminuoso Refl example: https://gist.github.com/JakobBruenker/38251269a93cdd1f4979b771e613f4e6 |
| 11:19:18 | <kuribas> | zyklotomic: f x = g . h $ x => f = g . h |
| 11:19:20 | <zyklotomic> | yeah, i do `fmap (f . g)` too |
| 11:19:44 | <zyklotomic> | like the other pattern i've seen that parallels this, is f <*> g <$> h |
| 11:19:47 | <kuribas> | zyklotomic: but with f x = g $ h $ x you have to replace all the ($)'s |
| 11:19:50 | <zyklotomic> | which well it does make sense |
| 11:20:17 | <boxscape> | dminuoso in the pattern guards the equality constraint is extracted |
| 11:20:25 | <dminuoso> | zyklotomic: If you explore this much, there's some pretty cool tricks |
| 11:20:31 | <kuribas> | zyklotomic: in the end it's your own preference |
| 11:20:33 | <dminuoso> | Personally Im a big fan of foldMap for example |
| 11:20:45 | × | alp quits (~alp@2a01:e0a:58b:4920:6cd6:5f96:4d6d:5a5) (Ping timeout: 272 seconds) |
| 11:20:45 | <zyklotomic> | dminuoso: wait, I finally see exactly what you mean about the last argument now |
| 11:20:53 | <zyklotomic> | I never came upon that realization |
| 11:21:13 | <dminuoso> | % getSum . foldMap Sum $ [1,2,3,4] :: Integer |
| 11:21:14 | <yahb> | dminuoso: 10 |
| 11:21:14 | <zyklotomic> | it was always trying to work out the order of operations/priority of the operetors idk what it's called |
| 11:21:19 | <zyklotomic> | precedence? |
| 11:21:43 | <zyklotomic> | like the PEMDAS of operators, i'm not sure what to calli t |
| 11:22:06 | <dminuoso> | boxscape: Okay, so Im staring at this, my head is not quite ready to be contorted. |
| 11:22:16 | <dminuoso> | Superficially, I can read it and understand what this is doing |
| 11:22:23 | <dminuoso> | But not quite why this works inductively |
| 11:22:40 | × | pfurla_ quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 11:22:40 | <dminuoso> | Is this essentially a theorem prover like coq in action? |
| 11:23:00 | <boxscape> | dminuoso yes, the main difference being that we can't be sure they're actually proofs because the totality checker is missing |
| 11:23:01 | → | alp joins (~alp@2a01:e0a:58b:4920:7900:a63:b56e:5a9) |
| 11:23:15 | <boxscape> | (though if a proof terminates successfully for an input, you've proven it for that input) |
| 11:23:20 | <dminuoso> | boxscape: Oh you mean because I can just sneak `undefined` in at any point to prove whatever? |
| 11:23:24 | <boxscape> | right |
| 11:23:55 | <kuribas> | dminuoso: how is that better than foldr (+) 0 [1, 2, 3, 4] ? |
| 11:24:23 | <dminuoso> | kuribas: Sum carries monoid laws implictly |
| 11:24:23 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds) |
| 11:24:32 | <boxscape> | dminuoso tbh these kinds of proofs are a lot easier to understand while writing than while reading, because you can look at the hole types along the way |
| 11:24:33 | <dminuoso> | with foldr you cant reason about laws |
| 11:24:43 | → | pfurla joins (~pfurla@190.15.195.173.client.static.strong-in52.as13926.net) |
| 11:25:01 | <dminuoso> | say, will `foldr (+) 0 [1,2,3,4]` and `foldl (+) 0 [1,2,3,4]` do the same thing? |
| 11:25:12 | <dminuoso> | Dunno really |
| 11:25:44 | <dminuoso> | I mean for this case I can of course tell, but the associativity and identity is not clearly communicated, and it's extra verbose |
| 11:25:48 | <kuribas> | dminuoso: depends on the Num instance |
| 11:25:59 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 11:26:00 | <dminuoso> | kuribas: Im just very fond of traverse and foldMap |
| 11:26:08 | <boxscape> | for example `plus_Z (SS n) = _` has hole type `'S (Plus n1 'Z) :~: 'S n1`, so we can call plus_Z n recursively and match on that to get out the `Plus n1 Z ~ n1` constraint, and then we just have to make something of type `S n1 :~: S n1`, which is Refl |
| 11:26:09 | <kuribas> | also foldMap Sum is very ineffecient |
| 11:26:20 | <kuribas> | it's too lazy |
| 11:26:46 | <dminuoso> | Often efficiency is not a problem I need, expressivity is more important to me :) |
| 11:27:01 | <dminuoso> | Consider this trick to implement traverse: |
| 11:27:04 | <kuribas> | I prefer both |
| 11:27:11 | × | sdx23 quits (~sdx23@unaffiliated/sdx23) (Remote host closed the connection) |
| 11:27:16 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 240 seconds) |
| 11:27:20 | <kuribas> | I mean efficiency and expressivity are not necessary mutually exclusive |
| 11:27:26 | → | sdx23 joins (~sdx23@unaffiliated/sdx23) |
| 11:27:30 | <dminuoso> | % ala ZipList traverse [[1,2,3],[10,20,30],[100,200,300]] |
| 11:27:30 | <yahb> | dminuoso: ; <interactive>:32:1: warning: [-Wtype-defaults]; * Defaulting the following constraints to type `Integer'; (Show b0) arising from a use of `print' at <interactive>:32:1-55; (Num b0) arising from a use of `it' at <interactive>:32:1-55; * In a stmt of an interactive GHCi command: print it; [[1,10,100],[2,20,200],[3,30,300]] |
| 11:27:39 | <dminuoso> | % ala ZipList traverse [[1,2,3],[10,20,30],[100,200,300]] :: [[Integer]] |
| 11:27:40 | <yahb> | dminuoso: [[1,10,100],[2,20,200],[3,30,300]] |
| 11:28:02 | <dminuoso> | Can't deny there's a certain beauty of both foldMap and traverse :) |
| 11:28:38 | <dminuoso> | kuribas: Also, we have foldMap' now :p |
| 11:29:07 | <dminuoso> | % ala Product foldMap [1,2,3,4] |
| 11:29:07 | <yahb> | dminuoso: ; <interactive>:34:1: warning: [-Wtype-defaults]; * Defaulting the following constraints to type `Integer'; (Show a0) arising from a use of `print' at <interactive>:34:1-29; (Num a0) arising from a use of `it' at <interactive>:34:1-29; * In a stmt of an interactive GHCi command: print it; 24 |
| 11:29:27 | <dminuoso> | % ala Product foldMap [1,2,3,4] |
| 11:29:28 | <yahb> | dminuoso: 24 |
| 11:29:30 | <kuribas> | foldMap' evaluated from left? |
| 11:29:44 | <dminuoso> | foldMap' f = foldl' (\ acc a -> acc <> f a) mempty |
| 11:29:52 | <dminuoso> | foldMap f = foldr (mappend . f) mempty |
| 11:29:56 | <kuribas> | ah cool |
| 11:30:20 | <nshepperd> | i presume foldMap' is strictly evaluated in whatever direction makes most sense for the type? |
| 11:30:52 | <kuribas> | nshepperd: is that even possible? |
| 11:31:06 | <kuribas> | nshepperd: ah by type you mean the foldable? |
| 11:31:21 | <nshepperd> | ie. foldl' for lists, foldr' for snoc lists |
| 11:31:24 | <nshepperd> | yeah |
| 11:33:40 | → | berberman_ joins (~berberman@unaffiliated/berberman) |
| 11:34:41 | × | berberman quits (~berberman@unaffiliated/berberman) (Ping timeout: 272 seconds) |
| 11:35:47 | → | chalkmonster joins (~chalkmons@unaffiliated/chalkmonster) |
| 11:36:31 | <dminuoso> | what is a snoc list? |
| 11:37:04 | <pjb> | A list from the end? |
| 11:37:24 | <dminuoso> | And that is different from a list... how? |
| 11:37:54 | <boxscape> | I guess it's different in that foldl has been renamed to foldr and vice versa? |
| 11:38:36 | <dminuoso> | boxscape: How's that? |
| 11:38:46 | <dminuoso> | The difference between foldl and foldr is not the order of the lits |
| 11:39:19 | <dminuoso> | It's how the function we replace the cons with associates |
| 11:39:39 | <boxscape> | dminuoso I know, but for that you need to have some mental image of what left and right means in a list, right? |
| 11:39:58 | <boxscape> | which isn't fundamentally part of the type |
| 11:40:16 | <kuribas> | (a <> (b <> (c <> d))) should be the same as (((a <> b) <> c) <> d) |
| 11:40:25 | <kuribas> | but one may be more efficient to calculate |
| 11:40:34 | <boxscape> | so if you swap directions of that mental image, you rename foldr to foldl and foldl to foldr, and perhaps write the constructor as [a] : a, and I imagine that's what a snoc list would be |
| 11:40:38 | <boxscape> | functionally the same as a list |
| 11:40:55 | <dminuoso> | Ill await nshepperd's response. :) |
| 11:40:59 | <dminuoso> | To clarify |
| 11:40:59 | <boxscape> | that's fair |
| 11:41:00 | <kuribas> | > foldMap' (<>) [a, b, c, d] |
| 11:41:02 | <lambdabot> | <Expr -> Expr> |
| 11:41:24 | <kuribas> | > foldMap' Sum [a, b, c, d] |
| 11:41:26 | <lambdabot> | Sum {getSum = 0 + a + b + c + d} |
| 11:41:30 | <kuribas> | > foldMap Sum [a, b, c, d] |
| 11:41:32 | <lambdabot> | Sum {getSum = a + (b + (c + (d + 0)))} |
| 11:41:51 | <dminuoso> | kuribas: The difference matters in two respects: Is the input data structure infinite, and do we need to be lazy on the output (do we build a chain of data constructors) |
| 11:42:18 | <kuribas> | those aren't the same value |
| 11:42:24 | <kuribas> | are they? |
| 11:42:24 | × | chaosmasttter quits (~chaosmast@p200300c4a70b2a01441f1455f36b3658.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 11:42:59 | <kuribas> | ah they are since 0 is the empty element |
| 11:43:16 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 240 seconds) |
| 11:43:20 | <dminuoso> | kuribas: by monoid laws they are the same |
| 11:43:41 | <dminuoso> | because precisely, a monoid is associative (so it doesnt matter how they associate) and mempty is the identity element (it doesnt matter where you slap it onto) |
| 11:44:15 | → | ft joins (~ft@shell.chaostreff-dortmund.de) |
| 11:44:47 | <dminuoso> | Guess that's the sort of things that makes foldMap so cool. You can just replace it with foldMap' without worrying whether it changes its meaning |
| 11:44:55 | <dminuoso> | with foldr/foldl |
| 11:45:07 | <dminuoso> | you have to manually check for associativity and identity |
| 11:46:55 | × | zyklotomic quits (~ethan@unaffiliated/chocopuff) (Quit: WeeChat 2.9) |
| 11:46:58 | → | Alleria_ joins (~AllahuAkb@2604:2000:1484:26:ef:21ba:eb1b:b066) |
| 11:47:05 | <boxscape> | hmm I wonder if a monoid with separate left and right identity elements could be useful |
| 11:47:31 | <tomjaguarpaw> | If you had left and right identities el and er what would el <> er be? |
| 11:48:26 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) () |
| 11:48:53 | <boxscape> | that's a very good question |
| 11:49:17 | <boxscape> | I guess it wouldn't be useful then |
| 11:49:36 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 2.9) |
| 11:49:53 | × | Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds) |
| 11:50:32 | <kuribas> | dminuoso: it does change meaning wrt bottom |
| 11:50:35 | → | jeet1 joins (~jeet@183.83.41.219) |
| 11:50:48 | <boxscape> | Although, I guess you could have a (not-quite-)monoid that *only* has left identity (or only right-identity) |
| 11:51:22 | <kuribas> | > foldMap First [1, 2, undefined] |
| 11:51:24 | <lambdabot> | error: |
| 11:51:24 | <lambdabot> | • No instance for (Num (Maybe ())) arising from a use of ‘e_112’ |
| 11:51:24 | <lambdabot> | • In the expression: e_112 |
| 11:51:50 | <nshepperd> | yeah a snoc list is just a cons list that has had left and right renamed |
| 11:52:41 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Remote host closed the connection) |
| 11:53:02 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 11:53:04 | <kuribas> | > foldMap First [Just 1, Just 2, undefined] |
| 11:53:06 | <lambdabot> | First {getFirst = Just 1} |
| 11:53:12 | <kuribas> | > foldMap' First [Just 1, Just 2, undefined] |
| 11:53:14 | <lambdabot> | First {getFirst = Just 1} |
| 11:53:47 | × | noctux quits (~noctux@unaffiliated/noctux) (Read error: Connection reset by peer) |
| 11:53:48 | <nshepperd> | you won't often find them in the wild |
| 11:54:25 | → | noctux joins (~noctux@unaffiliated/noctux) |
| 11:54:36 | <kuribas> | > foldMap All [True, False, undefined] |
| 11:54:37 | <lambdabot> | All {getAll = False} |
| 11:54:41 | <kuribas> | > foldMap' All [True, False, undefined] |
| 11:54:42 | <lambdabot> | All {getAll = False} |
| 11:54:49 | <kuribas> | hmmm |
| 11:55:10 | → | m0rphism joins (~m0rphism@HSI-KBW-095-208-098-207.hsi5.kabel-badenwuerttemberg.de) |
| 11:55:36 | <dminuoso> | nshepperd: That sounds.. like a list. |
| 11:56:04 | <nshepperd> | well yeah |
| 11:56:38 | <nshepperd> | you can just do things with lists, and remember to reverse things in your head when reading code |
| 11:57:27 | × | agrajag` quits (~agrajag`@84.39.117.57) (Remote host closed the connection) |
| 11:57:31 | <nshepperd> | but sometimes it's easier to have a different type so that the syntax corresponds to the intended ordering |
| 11:57:56 | <dminuoso> | So roughly a `data Tsil a = Snoc a (Tsil a) | Lin` differs from [] by conceptually reversing before folding/traversing? |
| 11:58:15 | <dminuoso> | (or in case of traverse, revere, traverse, and then reverse again) |
| 11:58:15 | <kuribas> | they are the same even with bottom then? |
| 11:59:14 | <boxscape> | the list matches the intended left right order better with Snoc (Tsil a) a: Lin `SNoc` 3 `Snoc` 2 `Snoc` 1 |
| 11:59:17 | <nshepperd> | generally you write SnocList a = Nil | Snoc (SnocList a) a |
| 11:59:29 | → | chaosmasttter joins (~chaosmast@p200300c4a70b2a01441f1455f36b3658.dip0.t-ipconnect.de) |
| 11:59:48 | <dminuoso> | Why not just use Dual? |
| 12:00:02 | × | jeet1 quits (~jeet@183.83.41.219) (Quit: WeeChat 2.9) |
| 12:00:11 | <nshepperd> | performance |
| 12:00:23 | <dminuoso> | Mmm, fair |
| 12:00:34 | <nshepperd> | also, pattern matching |
| 12:00:44 | × | Lycurgus quits (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) (Quit: Exeunt) |
| 12:00:45 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 12:00:46 | × | pfurla quits (~pfurla@190.15.195.173.client.static.strong-in52.as13926.net) (Ping timeout: 272 seconds) |
| 12:00:56 | <dminuoso> | boxscape: Ill take a look at your gist later tonight, think I need to sit down and employ the good ol' fashioned Feynman algorithm |
| 12:00:57 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 12:01:18 | <dminuoso> | nshepperd: well, the pattern matching is a mood argument, since it's no different from (:) |
| 12:01:37 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 12:01:44 | <nshepperd> | nooo |
| 12:01:58 | <dminuoso> | Whether you write `1:2:3:[]` or `[]:%3:%2:%1` seems no different at all |
| 12:02:07 | <nshepperd> | i mean, you can't use Dual when you're doing type level lists |
| 12:02:07 | × | AWizzArd quits (~code@unaffiliated/awizzard) (Read error: Connection reset by peer) |
| 12:02:10 | <dminuoso> | ah |
| 12:02:41 | → | AWizzArd joins (~code@gehrels.uberspace.de) |
| 12:03:42 | <boxscape> | dminuoso In a way I think these proofs are even harder to understand in Haskell than in some other languages, because the way constraint resolution makes it so it's not obvious how things are actually plugged together (though at least these are small proofs). But replacing the rhss with typed holes should help. |
| 12:03:44 | × | xff0x quits (~fox@2001:1a81:534b:a000:20f1:4040:a0e2:f16) (Ping timeout: 240 seconds) |
| 12:03:58 | <boxscape> | s/the way// |
| 12:04:32 | <kuribas> | I find myself going back from typed holes to tuples |
| 12:04:45 | → | xff0x joins (~fox@2001:1a81:534b:a000:65df:cebc:ef3d:70f7) |
| 12:04:48 | <kuribas> | the error message is much better |
| 12:05:06 | <__monty__> | Do you mean unit? |
| 12:05:13 | <kuribas> | __monty__: yes |
| 12:05:36 | <kuribas> | my-fun = () $ partial-implementation |
| 12:06:11 | <__monty__> | That does change how associativity is parsed, no? |
| 12:06:42 | <boxscape> | oh huh |
| 12:06:45 | <dminuoso> | boxscape: Btw, I think there's a mistake in your proof |
| 12:06:48 | <boxscape> | the error message is better, you're right |
| 12:06:50 | <boxscape> | dminuoso oh? |
| 12:06:53 | <dminuoso> | boxscape: plus_Z :: SNat n -> Plus n Z :~: n |
| 12:06:58 | <dminuoso> | boxscape: Think you mixed up the order to Plus there |
| 12:07:14 | <dminuoso> | The identity is only on one side in the tyfam |
| 12:07:26 | <dminuoso> | Or am I confusing things? |
| 12:07:46 | <boxscape> | dminuoso the identity of Plus Z n = n is trivial, but I have to write this proof to convince ghc that the other direction works, too |
| 12:08:33 | <dminuoso> | boxscape: Ohh, so `plus_Z SZ = Refl` gives us `Plus Z Z ~ Z` for the base case |
| 12:08:40 | <boxscape> | right |
| 12:08:51 | <dminuoso> | (Which evalutaes to Z ~ Z, dischargable because every type is automatically equal to itself) |
| 12:08:58 | <dminuoso> | So we dont need to provide proof ofZ ~ Z |
| 12:09:29 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 12:09:35 | <boxscape> | I would hope that if there were a mistake ghc would have caught it, otherwise there'd be a bug in ghc (or in my copy-paste abilites) |
| 12:10:15 | <boxscape> | uh, assuming it's not the sort of mistake that makes a proof non-total |
| 12:10:34 | <dminuoso> | plus_Z (SS n) | Refl <- plus_Z n = Refl |
| 12:10:44 | <dminuoso> | How does this inductive step work exaclty from the constraint solvers point of view? |
| 12:13:17 | <boxscape> | so, if you write plus_Z (SS n), what you have to solve is 'S (Plus n 'Z) :~: 'S n. plus_Z n has type (Plus n Z) :~: n, so by matching on that, we can unify Plus n Z with n, and we have to solve S n :~: S n |
| 12:13:31 | <boxscape> | and Refl is a value with that type, so we can just write Refl |
| 12:13:39 | <boxscape> | dminuoso |
| 12:14:14 | <dminuoso> | "what you have to solve is 'S (Plus n 'Z) :~: 'S n" |
| 12:14:21 | → | oerjan joins (~oerjan@195.206.169.184) |
| 12:14:26 | <dminuoso> | do you mean `S (Plus n 'Z) ~ 'S`? |
| 12:15:06 | <boxscape> | hmm I don't think I do. S by itself isn't a natural number, but S (Plus n Z) is a natural number, so that appears to be a kind error. |
| 12:15:15 | <dminuoso> | err |
| 12:15:37 | → | Tario joins (~Tario@201.192.165.173) |
| 12:16:17 | <boxscape> | ah but |
| 12:16:23 | <boxscape> | I should have used a different letter |
| 12:16:32 | <dminuoso> | boxscape: Sorry I think I cut off a quote there. We want to produce a value of type: 'S (Plus n 'Z) :~: 'S n |
| 12:16:32 | <boxscape> | like S (Plus m 'Z) :~: 'S m |
| 12:16:42 | <dminuoso> | So we use the data constructor Refl. That requires us to solve for a constraint |
| 12:16:50 | <dminuoso> | 'S (Plus n 'Z) ~ 'S n |
| 12:17:26 | <boxscape> | Ah, fair. What I meant by "solve" was "we have to write a value of that type on the rhs", but the terminology was a bit off, I admit |
| 12:17:59 | <dminuoso> | The pattern matching `Refl <- plus_Z n` uncovers the dictionary for the proof of the inductive hypothesis |
| 12:18:07 | <boxscape> | right |
| 12:18:30 | <dminuoso> | And from that we can show that (Plus n 'Z) ~ n |
| 12:18:36 | <dminuoso> | (or GHC can) |
| 12:18:42 | <dminuoso> | Thus leading us to conclude that |
| 12:18:50 | <dminuoso> | 'S n ~ 'S n |
| 12:18:52 | × | alp quits (~alp@2a01:e0a:58b:4920:7900:a63:b56e:5a9) (Ping timeout: 260 seconds) |
| 12:19:08 | <boxscape> | yeah, that sounds right |
| 12:19:08 | <dminuoso> | which is what Refl demands |
| 12:19:18 | <dminuoso> | mmm okay |
| 12:19:43 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 12:20:02 | <dminuoso> | So the value here of :~: is that we can have it in *positive* position, such that things can *produce* proofs of this |
| 12:20:12 | <dminuoso> | Whereas with => its, in effect, in negative position |
| 12:20:15 | → | alp joins (~alp@2a01:e0a:58b:4920:7562:27bf:89c5:b0d) |
| 12:20:18 | → | enoq joins (~textual@194-208-146-143.lampert.tv) |
| 12:20:24 | <boxscape> | right |
| 12:22:27 | → | Entertainment joins (~entertain@104.246.132.210) |
| 12:22:51 | <dminuoso> | actually I missed one step! |
| 12:22:57 | <dminuoso> | 13:18:42 dminuoso | Thus leading us to conclude that |
| 12:23:15 | <dminuoso> | This requires injectivity of 'S |
| 12:23:36 | <dminuoso> | Or.. mmm |
| 12:23:48 | <boxscape> | I think any function would do |
| 12:24:03 | <boxscape> | going the other way around would though |
| 12:24:18 | × | noctux quits (~noctux@unaffiliated/noctux) (Remote host closed the connection) |
| 12:24:18 | <dminuoso> | I should really reimplement the type system myself to get an idea |
| 12:24:23 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 12:24:37 | × | xacktm quits (xacktm@gateway/shell/panicbnc/x-wtuwnbsvfqpgvaqk) (Quit: PanicBNC - http://PanicBNC.net) |
| 12:24:47 | <dminuoso> | It's a bit mysterous what we can do with this though |
| 12:25:17 | <dminuoso> | Surely the value is not to prove commutativity of peano naturals to ourselves, using GHC. |
| 12:25:29 | → | noctux joins (~noctux@unaffiliated/noctux) |
| 12:25:43 | <boxscape> | dminuoso the value is in using this proof for value level functions, let me see if I can think of a good example |
| 12:26:01 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) (Ping timeout: 264 seconds) |
| 12:26:01 | → | Kaeipi joins (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 12:26:13 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 12:28:16 | <boxscape> | dminuoso hmm for example you could use it to prove things about other value level functions, like if you wanted to prove that (<>) :: Vec n a -> Vec m a -> Vec (Plus n m) a is associative, you would need associativity of Plus first |
| 12:28:52 | × | ArsenArsen quits (~Arsen@fsf/member/ArsenArsen) (Quit: bye) |
| 12:29:13 | → | ArsenArsen joins (~Arsen@fsf/member/ArsenArsen) |
| 12:29:13 | <boxscape> | dminuoso but it can also be useful for writing some regular type-level functions with complex types without explicitly trying to prove something about them, can't quite think of an example of that right now though |
| 12:30:03 | <dminuoso> | boxscape: Well but whats the value of *proving* this to GHC? |
| 12:30:16 | <dminuoso> | I mean providing a proof seems only useful if there's something demanding that proof |
| 12:30:47 | <__monty__> | Certified libraries? |
| 12:30:54 | <boxscape> | Right, that's what I meant with the example I can't think of right now :) Though I would say a proof is also useful to convice yourself that the function you wrote is correct |
| 12:30:59 | × | Entertainment quits (~entertain@104.246.132.210) () |
| 12:32:25 | → | Entertainment joins (~entertain@104.246.132.210) |
| 12:32:40 | <boxscape> | dminuoso also when I wrote "regular type-level functions" I mean "regular value-level functions" |
| 12:37:07 | → | p0a joins (~user@unaffiliated/p0a) |
| 12:37:26 | <p0a> | Hello why is this happening to `stack ghci' in every new stack project of mine? https://pastebin.com/SHVA1zET |
| 12:39:07 | <__monty__> | p0a: Looks like the same filename in a lib and an executable? Not sure why it's a problem though. |
| 12:39:26 | <__monty__> | Is the fully qualified name identical? |
| 12:39:47 | <p0a> | I don't know how to check whta you're asking me __monty__ |
| 12:39:58 | <merijn> | Who was asking about languages for low level/embedded stuff yesterday? I realised I forgot to mention a totally obvious candidate.. |
| 12:40:21 | <p0a> | __monty__: what lib has the same filename as an executable? |
| 12:40:40 | <p0a> | merijn: texasny-something I believe |
| 12:40:54 | <__monty__> | p0a: Paths_read_binfiles |
| 12:41:28 | <__monty__> | I think the problem is the module identifiers are identical and GHC doesn't know which one to pick. |
| 12:41:28 | <p0a> | __monty__: I don't know if it's a problem but `stack ghci' has some weird modules loaded |
| 12:41:36 | <p0a> | who decided on these names __monty__ ? |
| 12:41:47 | <__monty__> | Don't know. |
| 12:42:08 | <__monty__> | @hackage read-binfiles |
| 12:42:08 | <lambdabot> | https://hackage.haskell.org/package/read-binfiles |
| 12:42:10 | <merijn> | Paths_ modules are autogenerated by Cabal to access datafiles |
| 12:42:18 | <p0a> | It happens to all my new projects __monty__ |
| 12:43:13 | <merijn> | Make an issue on the stack github? Presumably they'll know how to debug what's going on |
| 12:43:29 | <p0a> | ok wanted to make sure it's not something obvious |
| 12:44:09 | → | mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) |
| 12:45:49 | <merijn> | It might be, but I don't use stack, so who knows :p |
| 12:47:59 | <boxscape> | dminuoso I ran into an example yesterday where I did need a proof, though not an equality proof, and it was on the type level, but I think should work equally well on the value level: Let's say you have an ordered list, where the cons constructor carries a proof that a cons'd element is less than the next element in the list (thus making sure it |
| 12:47:59 | <boxscape> | actually is ordered). If you want to delete an element in that list, you'll need a proof that less-than is transitive, as e.g. if you have [a,b,c] and want to delete b, you'll need to somehow construct a proof that a<c to get a new ordered list |
| 12:48:56 | <dminuoso> | Makes sense |
| 12:49:18 | <dminuoso> | So providing this proof is just to be able to re-construct this provably ordered list after the operation |
| 12:49:23 | × | gxt quits (~gxt@gateway/tor-sasl/gxt) (Ping timeout: 240 seconds) |
| 12:49:24 | <boxscape> | right |
| 12:49:39 | <dminuoso> | And the value is, you have some provable assurance the ordering is preserved by all operations |
| 12:49:46 | <boxscape> | yes |
| 12:50:24 | <dminuoso> | (in the absence of shortcircuiting the proof with bottom, of course) |
| 12:50:34 | × | p0a quits (~user@unaffiliated/p0a) (Quit: bye) |
| 12:50:45 | <boxscape> | right, though at least you can be sure that if your program *does* produce a result, it's a correct result |
| 12:51:07 | <dminuoso> | well that depends though, if the proof of transitivity is just bottom.. ? |
| 12:51:13 | <dminuoso> | It has to be runnable code |
| 12:51:21 | <Boomerang> | We use Refl very often at work when writing circuits in Clash. Clash uses type level Nat everywhere, it's often useful to choose which sub-circuit to use depending on the type |
| 12:51:59 | <boxscape> | right, it's still run to construct the actual proof object. Richard Eisenberg actually suggested in his thesis to replace equality proofs with unsafeCoerce Refl via a rewrite rule if you're sure they're total, for performance's sake |
| 12:52:10 | → | gxt joins (~gxt@gateway/tor-sasl/gxt) |
| 12:53:24 | <dminuoso> | Ah right, because Refl still has a runtime representation |
| 12:53:31 | <boxscape> | yeah |
| 12:59:23 | <boxscape> | (Though you can't do this unsafeCoerce stuff with all proofs, because for less-than for example, proofs will typically have different run-time reprenentations depending on how large the difference between the two values is, at least for comparing data Nat = S Nat | Z) |
| 13:00:15 | × | shangxiao quits (~davids@101.181.159.140) (Quit: WeeChat 2.9) |
| 13:01:59 | <boxscape> | (that is, data (<) :: Nat -> Nat -> Type where ZltS :: Z < (S n); SltS :: n < m -> (S n) < (S m), so for example SltS (SltS (ZltS) :: 2 < 5) |
| 13:02:19 | <boxscape> | (I guess what matters there is actually the size of the first value, not the difference between them) |
| 13:02:30 | × | troydm quits (~troydm@unaffiliated/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 13:02:36 | × | elliott__ quits (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 13:03:08 | → | elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) |
| 13:03:11 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) |
| 13:05:15 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 13:07:41 | → | xacktm joins (xacktm@gateway/shell/panicbnc/x-fxbrslxxjjorsbbu) |
| 13:07:47 | × | kritzefitz quits (~kritzefit@fw-front.credativ.com) (Read error: Connection timed out) |
| 13:08:15 | → | n0042 joins (d055ed89@208.85.237.137) |
| 13:10:14 | → | urodna joins (~urodna@unaffiliated/urodna) |
| 13:12:47 | → | texasmynsted joins (~texasmyns@212.102.45.112) |
| 13:13:16 | × | valdyn quits (~valdyn@host-88-217-143-53.customer.m-online.net) (Ping timeout: 260 seconds) |
| 13:14:29 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 13:15:55 | → | christo joins (~chris@81.96.113.213) |
| 13:16:00 | × | jwynn6 quits (~jwynn6@050-088-122-078.res.spectrum.com) (Read error: Connection reset by peer) |
| 13:16:19 | → | jwynn6 joins (~jwynn6@050-088-122-078.res.spectrum.com) |
| 13:18:14 | → | tromp_ joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 13:18:15 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Read error: Connection reset by peer) |
| 13:21:47 | × | bitmapper quits (uid464869@gateway/web/irccloud.com/x-xpsufctbszodgohs) (Quit: Connection closed for inactivity) |
| 13:22:26 | → | troydm joins (~troydm@unaffiliated/troydm) |
| 13:22:36 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 265 seconds) |
| 13:24:45 | × | chalkmonster quits (~chalkmons@unaffiliated/chalkmonster) (Ping timeout: 240 seconds) |
| 13:24:57 | → | kritzefitz joins (~kritzefit@fw-front.credativ.com) |
| 13:31:30 | → | aarvar joins (~foewfoiew@50.35.43.33) |
| 13:31:36 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 13:32:47 | → | christo joins (~chris@81.96.113.213) |
| 13:32:57 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 13:33:46 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 13:35:42 | × | n0042 quits (d055ed89@208.85.237.137) (Remote host closed the connection) |
| 13:38:46 | × | gnumonic_ quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Read error: Connection reset by peer) |
| 13:39:37 | → | n0042 joins (d055ed89@208.85.237.137) |
| 13:39:49 | → | LKoen joins (~LKoen@169.244.88.92.rev.sfr.net) |
| 13:40:00 | hackage | subG 0.4.1.0 - Some extension to the Foldable and Monoid classes. https://hackage.haskell.org/package/subG-0.4.1.0 (OleksandrZhabenko) |
| 13:40:22 | <n0042> | Are there any rules or guidelines for messing with the Lambdabot? That looks like fun but I don't want to break it or anything |
| 13:40:59 | <Uniaika> | don't try to form an emotional connection with it, you'll be disappointed |
| 13:41:21 | <n0042> | :O |
| 13:41:31 | <boxscape> | n0042 you may know this but if you want to mess with it without spamming #haskell, you can do so in DMs. If you do find a way to break it, seems like a great opportunity for a bug report |
| 13:41:34 | <boxscape> | @botsnack |
| 13:41:34 | <lambdabot> | :) |
| 13:41:36 | <geekosaur> | .oO { if you can break it, we did it wrong } |
| 13:41:36 | <tdammers> | I thought lambdabot was a "she"? |
| 13:42:08 | <Uniaika> | I don't have a habit of anthropomorphising bots |
| 13:42:10 | <n0042> | Thank you boxscape. That is a good tip |
| 13:42:25 | <tdammers> | ships are "she" too |
| 13:43:13 | <Uniaika> | tdammers: that's a maritime culture convention :P |
| 13:43:33 | <boxscape> | countries do, too |
| 13:43:42 | <boxscape> | s/do/are |
| 13:43:53 | <Uniaika> | is that so? |
| 13:44:18 | <boxscape> | yes, I mostly hear it in geopolitical commentary |
| 13:44:26 | <boxscape> | or cgpgrey's videos |
| 13:44:39 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:2da3:37d0:5114:5834) |
| 13:46:07 | <boxscape> | ..or, actually, I think in geopolitical commentary I usually see the capital being used |
| 13:46:24 | × | cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Ping timeout: 260 seconds) |
| 13:46:40 | <n0042> | That's definitely a thing. |
| 13:46:41 | <tdammers> | Uniaika: if sailors can have weird traditions, why can't we |
| 13:47:24 | <boxscape> | because if you anthropomorphize lambdabot, you'll form emotional connections with it, and as we learned that means you'll be disappointed |
| 13:47:32 | × | wei2912 quits (~wei2912@unaffiliated/wei2912) (Remote host closed the connection) |
| 13:47:57 | <ski> | lambdabot was anthropomorphized as a she, rather long ago, yes |
| 13:48:06 | <dminuoso> | authoritatively? |
| 13:48:19 | dminuoso | didn't get the memo |
| 13:48:27 | <n0042> | What is the command to make Lambdabot evaluate an expression or list comprehension? |
| 13:48:47 | <boxscape> | > [ x | x <- [1..5] ] |
| 13:48:49 | <lambdabot> | [1,2,3,4,5] |
| 13:48:56 | <ski> | the South Park style avatar for lambdabot, chosen by voting in #haskell-blah, was definitely female |
| 13:48:59 | <dminuoso> | > fix error |
| 13:49:02 | <lambdabot> | "*Exception: *Exception: *Exception: *Exception: *Exception: *Exception: *Ex... |
| 13:49:03 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 13:49:09 | <boxscape> | (a list comprehension is an expression fwiw) |
| 13:49:12 | <Uniaika> | ski: is that channel still alive? |
| 13:49:17 | <boxscape> | ish |
| 13:49:23 | → | __monty_1 joins (~toonn@unaffiliated/toonn) |
| 13:49:24 | <boxscape> | #haskell-offtopic is more popular |
| 13:49:34 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:2da3:37d0:5114:5834) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 13:49:36 | <dminuoso> | ski: Maybe we could have the Haskell Foundation make an announcement then, as their first official act. |
| 13:49:43 | <dminuoso> | It seems relevant. |
| 13:49:58 | <Uniaika> | hahaha |
| 13:50:05 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Ping timeout: 240 seconds) |
| 13:50:05 | <n0042> | Excellent, thank you. I tried to do it without a space after the prompt, which is why it wasn't working. |
| 13:50:11 | <ski> | i'm not sure if the page where there were some South Park style avatars for some people on #haskell / #haskell-blah, is still available somewhere. the original link doesn't work anymore, at least |
| 13:51:08 | ski | idly recalls the `@vixen' command |
| 13:52:21 | <hpc> | i liked it better when @vixen was removed and it autocorrected to @nixon :D |
| 13:52:33 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 13:52:40 | <ski> | that still happens |
| 13:53:08 | <boxscape> | https://wiki.haskell.org/Lambdabot still has the lambdabot avatar, at least |
| 13:53:22 | <ski> | yes, that was the one |
| 13:54:53 | <ski> | (i think the idea was to portray someone being a bit overworked, eyes glazing over, by lots of queries, many of them not that interesting) |
| 13:56:12 | <ski> | but there were also some similar style avatars selected, by some other channel regulars, including shapr, me, Philippa, &c. |
| 13:57:28 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Remote host closed the connection) |
| 13:58:07 | <siraben> | What's the shortest way to write r x y z = y z x, in pointfree? |
| 13:58:22 | <siraben> | @pl \x y z -> y z x |
| 13:58:22 | <lambdabot> | flip flip |
| 13:58:37 | <ski> | @keal |
| 13:58:37 | <lambdabot> | i try make program called Glyph to do it but my script lang called T too slow. i invent T |
| 13:58:47 | <ski> | @palomer |
| 13:58:47 | <lambdabot> | Brump! |
| 14:01:04 | <n0042> | That's a pretty great bot lol. Its creators should be proud |
| 14:01:20 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 14:02:31 | lep-delete | is now known as test |
| 14:03:00 | test | is now known as Guest56787 |
| 14:03:07 | Guest56787 | is now known as lep-delete |
| 14:03:23 | <boxscape> | tbh I tend to use yahb more often these days, it's nice to have a proper ghci with alls bells and whistles. Then again, you can't do this with yahb: |
| 14:03:24 | <boxscape> | @pl \a b d c d e f -> f b d c a e |
| 14:03:24 | <lambdabot> | ((const . ((flip .) .)) .) . flip (flip . ((flip . (flip .)) .) . flip . (flip .) . flip . flip id) |
| 14:04:01 | <siraben> | boxscape: yahb? |
| 14:04:15 | <boxscape> | % print "yahb" |
| 14:04:15 | <yahb> | boxscape: "yahb" |
| 14:04:31 | hackage | prolude 0.0.0.9 - ITProTV's custom prelude https://hackage.haskell.org/package/prolude-0.0.0.9 (saramuse) |
| 14:04:43 | ski | remembers preflex |
| 14:08:56 | → | invaser1 joins (~Thunderbi@31.148.23.125) |
| 14:10:03 | <kuribas> | I was just thinking how similar destructuring syntax for records in haskell is to clojure hashmaps. |
| 14:10:15 | <kuribas> | with NamedFieldPuns it's almost the same. |
| 14:10:36 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 240 seconds) |
| 14:10:36 | invaser1 | is now known as invaser |
| 14:11:16 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-zkpwgkjicmhndtdh) |
| 14:11:24 | <kuribas> | And while haskell records are not extensible, you can still simulate it with overloadedFields and RecordWildCards. |
| 14:12:00 | hackage | subG 0.4.2.0 - Some extension to the Foldable and Monoid classes. https://hackage.haskell.org/package/subG-0.4.2.0 (OleksandrZhabenko) |
| 14:12:05 | <kuribas> | For example merging: merge PartialUser1{..} PartialUser2{..} = User{..} |
| 14:12:58 | <kuribas> | the "drawback" is having to define partial types, although I think that's a feature, not a drawback. |
| 14:13:16 | × | ft quits (~ft@shell.chaostreff-dortmund.de) (Ping timeout: 246 seconds) |
| 14:13:50 | <kuribas> | haskell has a reputation for being terrible with records, my experience is quite positive. |
| 14:14:35 | <ski> | it's too bad that Haskell records binds selector functions to the field names |
| 14:14:46 | <kuribas> | yeah true |
| 14:14:56 | → | hexfive joins (~hexfive@50-47-142-195.evrt.wa.frontiernet.net) |
| 14:14:59 | <ski> | the ML way is, imho, much better |
| 14:15:14 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 14:16:36 | → | aveltras joins (uid364989@gateway/web/irccloud.com/x-jtdricnolbjelrxi) |
| 14:16:47 | → | christo joins (~chris@81.96.113.213) |
| 14:17:14 | <merijn> | ski: That's fixed soon! |
| 14:17:26 | <kuribas> | and with overloadedLabels selector functions are even more useless |
| 14:17:26 | <merijn> | ski: There was a GHC proposal for -XNoFieldSelectors |
| 14:17:28 | <ski> | writing `#x pt' or `pt #x' or something along those lines would be much better than to write `x pt'. that way, you don't shadow the field extraction, with `NamedFieldPuns' |
| 14:17:44 | <merijn> | ski: It's already implemented and slated to merge into 9.2, iirc? |
| 14:18:06 | → | hseg joins (~gesh@185.120.126.113) |
| 14:18:06 | <ski> | yea, i've heard that mentioned. is there are proposal for a replacement field selector syntax, that you know ? |
| 14:18:07 | → | Lycurgus joins (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) |
| 14:18:31 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Ping timeout: 246 seconds) |
| 14:18:39 | <merijn> | Not directly, but if you use it the namespace is free to generate, for example, lenses with the field names |
| 14:18:56 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 14:19:07 | ski | nods |
| 14:20:19 | <xsperry> | ski, how does ML do it? |
| 14:20:39 | → | christo joins (~chris@81.96.113.213) |
| 14:20:43 | <ski> | (also, users (especially newbies) wouldn't be confused by the cognitive dissonance by the field signature `x :: Int' vs. the field extraction function signature `x :: Point -> Int') |
| 14:21:18 | <ski> | xsperry : if `x' is a field in a record, then `#x' is a field extraction function, taking the record and extracting the field. that's in SML |
| 14:21:28 | <ski> | O'Caml does `pt .x', iirc |
| 14:21:54 | <xsperry> | so fields are in separate namespace? |
| 14:22:01 | <ski> | (but the main point is to not simply bind the field name to a field extraction function) |
| 14:22:22 | <ski> | yes |
| 14:22:26 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 14:22:41 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 14:22:44 | → | renzhi joins (~renzhi@2607:fa49:655f:e600::28da) |
| 14:23:17 | → | AlterEgo- joins (~ladew@124-198-158-163.dynamic.caiway.nl) |
| 14:23:28 | <xsperry> | and what if multiple objects have field named x? |
| 14:23:33 | <xsperry> | multiple types* |
| 14:23:58 | <merijn> | xsperry: With NoFieldSelectors, yes |
| 14:24:16 | <merijn> | xsperry: i.e. you can only use them in pattern matches/record creation |
| 14:24:18 | <ski> | in SML, you must pin down the record type |
| 14:24:21 | <xsperry> | I mean in ML/Ocaml. just wondering if it basically works like structs/classes in mainstream languages |
| 14:24:26 | → | ft joins (~ft@shell.chaostreff-dortmund.de) |
| 14:24:53 | <ski> | in OCaml, iirc, field extraction is polymorphic, using row types |
| 14:25:02 | → | noteness joins (noteness@unaffiliated/nessessary129) |
| 14:25:26 | <merijn> | ski: uh |
| 14:25:33 | <merijn> | ski: OCaml doesn't have rowtypes, does it? |
| 14:25:47 | <ski> | (ML is a family of languages, including SML,O'Caml,F#,Alice ML,..) |
| 14:25:50 | <ski> | it does |
| 14:25:52 | <merijn> | Unless they added those super recently |
| 14:26:32 | × | forell quits (~forell@unaffiliated/forell) (Ping timeout: 260 seconds) |
| 14:28:00 | → | sagax joins (~sagax_nb@213.138.71.146) |
| 14:28:12 | → | forell joins (~forell@unaffiliated/forell) |
| 14:28:37 | → | Amras joins (~Amras@unaffiliated/amras0000) |
| 14:29:38 | → | GilReiter joins (4d7e19c5@77.126.25.197) |
| 14:29:56 | × | n0042 quits (d055ed89@208.85.237.137) (Remote host closed the connection) |
| 14:29:57 | <ski> | object types and polymorphic variants have long been in O'Caml |
| 14:30:00 | × | forell quits (~forell@unaffiliated/forell) (Client Quit) |
| 14:30:37 | <ski> | "If 'ident denotes an explicit polymorphic variable, and typexpr denotes either an object or polymorphic variant type, the row variable of typexpr is captured by 'ident, and quantified upon." |
| 14:31:19 | × | elliott__ quits (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 256 seconds) |
| 14:31:21 | → | forell joins (~forell@unaffiliated/forell) |
| 14:34:10 | → | oish joins (~charlie@217.169.25.228) |
| 14:34:14 | <ski> | "The type <{ method-type ;} ..> is the type of an object whose method names and types are described by method-type ₁ …, method-type ₙ, possibly some other methods represented by the ellipsis. This ellipsis actually is a special kind of type variable (called row variable in the literature) that stands for any number of extra method types." |
| 14:34:44 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 14:35:12 | <ski> | (that's from <https://caml.inria.fr/pub/docs/manual-ocaml/types.html>) |
| 14:40:10 | → | ystael joins (~ystael@209.6.50.55) |
| 14:40:44 | <ski> | xsperry : ah, ok. so it's just method selection for object types that's polymororphic, not field selection for record types. see < |
| 14:40:50 | × | ystael quits (~ystael@209.6.50.55) (Read error: Connection reset by peer) |
| 14:41:55 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Remote host closed the connection) |
| 14:42:25 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 14:43:05 | → | christo joins (~chris@81.96.113.213) |
| 14:43:16 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 14:44:55 | <ski> | see <https://caml.inria.fr/pub/docs/manual-ocaml/coreexamples.html#ss:record-and-variant-disambiguation> and <https://caml.inria.fr/pub/docs/manual-ocaml/objectexamples.html> |
| 14:45:01 | × | byorgey quits (~byorgey@155.138.238.211) (Quit: leaving) |
| 14:45:13 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 14:45:28 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 14:45:30 | × | toorevitimirp quits (~tooreviti@117.182.180.118) (Remote host closed the connection) |
| 14:46:01 | → | toorevitimirp joins (~tooreviti@117.182.180.118) |
| 14:46:23 | → | christo joins (~chris@81.96.113.213) |
| 14:46:47 | × | Lycurgus quits (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) (Quit: Exeunt) |
| 14:47:26 | → | ystael joins (~ystael@209.6.50.55) |
| 14:50:31 | × | hseg quits (~gesh@185.120.126.113) (Quit: WeeChat 2.9) |
| 14:50:56 | × | cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Ping timeout: 240 seconds) |
| 14:52:19 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Quit: mputz) |
| 14:53:12 | → | knupfer joins (~Thunderbi@dynamic-046-114-144-166.46.114.pool.telefonica.de) |
| 14:55:30 | × | knupfer quits (~Thunderbi@dynamic-046-114-144-166.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 14:56:36 | × | oish quits (~charlie@217.169.25.228) (Ping timeout: 240 seconds) |
| 14:57:52 | → | Sgeo joins (~Sgeo@ool-18b982ad.dyn.optonline.net) |
| 15:00:13 | × | LKoen quits (~LKoen@169.244.88.92.rev.sfr.net) (Read error: Connection reset by peer) |
| 15:00:13 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 15:00:31 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 15:00:48 | × | DataComputist quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Quit: Leaving...) |
| 15:01:34 | → | LKoen joins (~LKoen@169.244.88.92.rev.sfr.net) |
| 15:02:39 | × | GilReiter quits (4d7e19c5@77.126.25.197) (Remote host closed the connection) |
| 15:07:38 | → | nbloomf joins (~nbloomf@76.217.43.73) |
| 15:08:35 | → | conal joins (~conal@64.71.133.70) |
| 15:08:50 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 15:09:46 | × | coco quits (~coco@212-51-146-87.fiber7.init7.net) (Quit: WeeChat 2.9) |
| 15:12:02 | × | xff0x quits (~fox@2001:1a81:534b:a000:65df:cebc:ef3d:70f7) (Ping timeout: 264 seconds) |
| 15:12:19 | × | nbloomf quits (~nbloomf@76.217.43.73) (Ping timeout: 265 seconds) |
| 15:13:55 | → | xff0x joins (~fox@141.98.255.145) |
| 15:14:34 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 272 seconds) |
| 15:15:20 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 15:15:43 | × | alp quits (~alp@2a01:e0a:58b:4920:7562:27bf:89c5:b0d) (Ping timeout: 272 seconds) |
| 15:22:18 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 2.9) |
| 15:24:13 | × | xff0x quits (~fox@141.98.255.145) (Ping timeout: 264 seconds) |
| 15:24:55 | → | st8less joins (~st8less@2603:a060:11fd:0:744d:b66f:d608:4e8e) |
| 15:25:02 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:f4f3:bbb1:9462:91ce) |
| 15:26:07 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 260 seconds) |
| 15:26:09 | → | xff0x joins (~fox@2001:1a81:534b:a000:65df:cebc:ef3d:70f7) |
| 15:26:53 | → | xerox_ joins (~xerox@unaffiliated/xerox) |
| 15:29:55 | × | toorevitimirp quits (~tooreviti@117.182.180.118) (Read error: Connection reset by peer) |
| 15:32:36 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Remote host closed the connection) |
| 15:35:11 | → | Shiranai joins (beed0255@gateway/web/cgi-irc/kiwiirc.com/ip.190.237.2.85) |
| 15:39:03 | → | Sarma joins (~Amras@unaffiliated/amras0000) |
| 15:39:15 | × | __monty_1 quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 15:41:03 | × | Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds) |
| 15:46:07 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 256 seconds) |
| 15:46:15 | → | ddellacosta joins (dd@gateway/vpn/mullvad/ddellacosta) |
| 15:47:04 | → | bitmapper joins (uid464869@gateway/web/irccloud.com/x-uhdfbowqpmvzztxz) |
| 15:47:58 | → | Mrkz71 joins (c1ef2595@193-239-37-149.ksi-system.net) |
| 15:48:41 | × | carlomagno quits (~cararell@148.87.23.12) (Remote host closed the connection) |
| 15:49:01 | → | carlomagno joins (~cararell@148.87.23.5) |
| 15:51:57 | <dminuoso> | Mmm, I have a file with lines of varying indention, and I intend to interpret that as a tree like this https://gist.github.com/dminuoso/7911cb8e16c4de0d48de20e7270ebc68 |
| 15:52:24 | <dminuoso> | I can cook up some sort of stateful unfold, but I was wondering whether there was some tree related library that would give me this for free |
| 15:52:43 | → | northman_ joins (~textual@204.111.252.124) |
| 15:53:02 | <dminuoso> | (Doesnt have to be that exact tree data type) |
| 15:53:03 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 15:53:55 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-104-55.w86-212.abo.wanadoo.fr) |
| 15:56:37 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 264 seconds) |
| 15:57:28 | <[exa]> | dminuoso: you can preprocess the leading whitespace to 'indent' and 'unindent' marks easily, then it's pretty easy to do |
| 15:57:40 | → | hnOsmium0001 joins (uid453710@gateway/web/irccloud.com/x-lviokxjrzjjmnlqh) |
| 16:01:39 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 16:01:45 | → | Codaraxis joins (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) |
| 16:01:55 | → | coot joins (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) |
| 16:01:59 | <dminuoso> | [exa]: Mmm, what kind of un/indent mark are you referring to? Should these become conceptual push/pop instructions of a stack of things? |
| 16:03:20 | × | Codaraxis_ quits (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) (Ping timeout: 244 seconds) |
| 16:04:19 | → | Codaraxis_ joins (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) |
| 16:04:26 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 16:05:24 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Max SendQ exceeded) |
| 16:05:48 | × | concept2 quits (~concept2@unaffiliated/tubo) (Ping timeout: 256 seconds) |
| 16:05:51 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 16:06:32 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-sgcggzhikhhgebxn) |
| 16:06:42 | × | Shiranai quits (beed0255@gateway/web/cgi-irc/kiwiirc.com/ip.190.237.2.85) (Quit: Connection closed) |
| 16:06:47 | → | concept2 joins (~concept2@unaffiliated/tubo) |
| 16:06:59 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Max SendQ exceeded) |
| 16:07:26 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 16:07:54 | × | Codaraxis quits (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) (Ping timeout: 265 seconds) |
| 16:08:34 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Max SendQ exceeded) |
| 16:09:05 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 16:11:15 | <[exa]> | dminuoso: yeah, it's not supersmart but safest way around I found |
| 16:11:17 | → | hyperisco joins (~hyperisco@d192-186-117-226.static.comm.cgocable.net) |
| 16:12:01 | <dmj`> | why can't we :unset -Werror in ghci |
| 16:14:19 | <dolio> | Seems like it doesn't no how to :unset any -W flag. |
| 16:14:25 | <dolio> | Know, even. |
| 16:15:00 | hackage | subG-instances 0.1.0.0 - Additional instances for the InsertLeft class from subG package. https://hackage.haskell.org/package/subG-instances-0.1.0.0 (OleksandrZhabenko) |
| 16:15:45 | <dminuoso> | [exa]: heh yeah that's what Im already doing. I just keep the previous indention as state around, so if it increases it becomes a push on a buffer where I push things onto, and on a pop I just flush the butter |
| 16:15:49 | <boxscape> | does :set -Wno-error work? |
| 16:15:52 | <dminuoso> | this is incredibly imperative, sadly |
| 16:16:06 | <[exa]> | https://gist.github.com/exaexa/9920eb85d2bd20f4c575f2f1d307ae96 |
| 16:16:08 | <dolio> | You can `:set -Wwarn` |
| 16:16:13 | <boxscape> | ah |
| 16:16:14 | <dolio> | Which is supposed to reverse it. |
| 16:16:26 | <dminuoso> | % :set -Wno-warn |
| 16:16:26 | <yahb> | dminuoso: ; <no location info>: warning: unrecognised warning flag: -Wno-warn |
| 16:16:33 | <dminuoso> | % :set -Wno-error |
| 16:16:33 | <yahb> | dminuoso: ; <no location info>: warning: unrecognised warning flag: -Wno-error |
| 16:16:35 | <dminuoso> | Mmm |
| 16:16:45 | <dolio> | There's no `no-` for those for some reason. |
| 16:16:52 | × | northman_ quits (~textual@204.111.252.124) (Quit: Textual IRC Client: www.textualapp.com) |
| 16:17:02 | <[exa]> | dminuoso: I guess there's no better way, the indented stream itself is a series of commands encoded in the spaces...so what. :] |
| 16:17:03 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Read error: Connection reset by peer) |
| 16:17:19 | <dminuoso> | [exa]: Well I can always throw `indents` at it! |
| 16:17:41 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 16:18:21 | <boxscape> | hm I suppose if -Wno-warn existed the intuitive interpretation would be that it turns off warnings alltogether, and then it would be unclear if -Wno-error should put warnings into -Wwarn mode or into -Wno-warn mode |
| 16:18:44 | → | northman_ joins (~textual@204.111.252.124) |
| 16:19:36 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 16:19:51 | × | northman_ quits (~textual@204.111.252.124) (Client Quit) |
| 16:20:12 | → | larou joins (5eae2591@gateway/web/cgi-irc/kiwiirc.com/ip.94.174.37.145) |
| 16:20:17 | <larou> | hello! |
| 16:20:42 | <boxscape> | hi |
| 16:20:46 | → | huskyhaskell joins (~user@2001:9b1:29fe:fc00:55d8:279e:df7e:2d64) |
| 16:20:52 | <larou> | I have code!! |
| 16:21:10 | <[exa]> | dminuoso: careful not to end up with python. :D |
| 16:21:16 | <larou> | no i dont, i only have rumours of code |
| 16:21:28 | → | northman_ joins (~northman@204.111.252.124) |
| 16:21:45 | ← | huskyhaskell parts (~user@2001:9b1:29fe:fc00:55d8:279e:df7e:2d64) () |
| 16:22:08 | <larou> | i have a new type of tree |
| 16:22:17 | × | howdoi quits (uid224@gateway/web/irccloud.com/x-zkpwgkjicmhndtdh) (Quit: Connection closed for inactivity) |
| 16:22:25 | <larou> | its better than normal trees |
| 16:22:41 | <larou> | it has upwards branches |
| 16:22:48 | <larou> | iv been trying to do it for ages |
| 16:22:55 | [exa] | briefly recalls "normal" trees |
| 16:23:08 | <larou> | yeah, those have only downwards branches |
| 16:23:32 | <larou> | these are way better |
| 16:23:34 | <[exa]> | I mean the nature ones |
| 16:24:03 | <larou> | never mind your vacant wonderings |
| 16:24:42 | <larou> | they typecheck and everything |
| 16:24:45 | <boxscape> | does it have upwards as well as downward branches or only upwards branches? |
| 16:24:45 | → | knupfer joins (~Thunderbi@200116b82cfb87004c47b2fffe20891d.dip.versatel-1u1.de) |
| 16:24:45 | × | knupfer quits (~Thunderbi@200116b82cfb87004c47b2fffe20891d.dip.versatel-1u1.de) (Client Quit) |
| 16:25:01 | hackage | git-lfs 1.1.1 - git-lfs protocol https://hackage.haskell.org/package/git-lfs-1.1.1 (JoeyHess) |
| 16:25:05 | <larou> | sure, its not just an upside down tree... |
| 16:25:08 | → | knupfer joins (~Thunderbi@200116b82cfb8700fd61a7f6e9856548.dip.versatel-1u1.de) |
| 16:25:14 | <boxscape> | ah, good |
| 16:25:24 | <larou> | i put functions on them |
| 16:25:30 | <larou> | at the branches |
| 16:25:41 | <larou> | MIMO functions (multiple inputs multiple outputs) |
| 16:25:58 | <larou> | just one input and one output argument, that are HLists |
| 16:25:59 | boxscape | thinks the upwards branches should be called "roots" |
| 16:26:13 | <larou> | original! |
| 16:26:20 | → | p-core joins (~Thunderbi@2001:718:1e03:5128:2ab7:7f35:48a1:8515) |
| 16:26:38 | <larou> | i call them output edges |
| 16:26:43 | → | jneira joins (02896ac0@gateway/web/cgi-irc/kiwiirc.com/ip.2.137.106.192) |
| 16:26:47 | <larou> | inputs go at the leafs |
| 16:27:09 | <larou> | and they do the cyclic thing perfectly!!! |
| 16:27:20 | <merijn> | So...graphs? |
| 16:27:21 | <larou> | they are a list, instead of a free thing |
| 16:27:34 | × | cocreature quits (~cocreatur@eirene.uberspace.de) (Read error: Connection reset by peer) |
| 16:27:34 | <larou> | meijn: no they are trees |
| 16:27:41 | <larou> | they just have lookup tables |
| 16:27:49 | <larou> | but its just the same |
| 16:27:50 | <merijn> | trees are graphs |
| 16:28:02 | <larou> | but graphs can be cyclic, while trees cant |
| 16:28:04 | <merijn> | They're just a more boring subset of graphs (i.e. on without cycles) |
| 16:28:08 | <larou> | thats what makes them trees not graphs |
| 16:28:11 | <larou> | and this is a tree |
| 16:28:12 | → | cocreature joins (~cocreatur@eirene.uberspace.de) |
| 16:28:31 | × | Mrkz71 quits (c1ef2595@193-239-37-149.ksi-system.net) (Remote host closed the connection) |
| 16:28:33 | <larou> | so... not graphs... |
| 16:28:40 | <larou> | i have also "sparks" |
| 16:28:47 | <larou> | these are the bits that make them not graphs |
| 16:28:58 | <larou> | when you see a cycle, you must make a spark |
| 16:29:01 | <larou> | it is a state |
| 16:29:06 | <[exa]> | larou: data structure folks demand a precise written definition |
| 16:29:11 | × | justan0theruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds) |
| 16:29:21 | <merijn> | [exa]: non-data structure folk too :p |
| 16:29:41 | <larou> | it goes to an output instead of to the input variable, this is externally stored, as a state, and fed back in at the input at the next itteration |
| 16:30:07 | <larou> | it would have been imposible to reference its current value to calculate itself at this iteration, so it has to be from the last |
| 16:30:13 | <larou> | thats why we get "spark states" |
| 16:30:51 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 16:31:01 | <[exa]> | like seriously, this sounds like the random rnn-generated paper about quantum physics. Get a piece of LaTeX and write it down, with examples and pics. |
| 16:31:13 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 16:31:18 | <larou> | [exa]: its definition is an extension of the GADT for list, in that it has extra params on the thing being consed to. also, there is another record to the datatype which just wraps itself, but has a constraint that checks to see the sparks are correct in preventing cycles |
| 16:31:49 | <larou> | oh you want the code, hang on |
| 16:32:27 | × | enoq quits (~textual@194-208-146-143.lampert.tv) (Quit: Textual IRC Client: www.textualapp.com) |
| 16:33:06 | <larou> | here |
| 16:33:07 | <larou> | https://pastebin.com/raw/Kq05pARC |
| 16:34:50 | <larou> | and here; https://pastebin.com/raw/gHZaze9F |
| 16:34:51 | <[exa]> | on which line are the trees and sparks? |
| 16:35:04 | <larou> | in the 2nd paste, its "Net" |
| 16:35:07 | × | Ariakenom quits (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) (Quit: Leaving) |
| 16:35:26 | → | Ariakenom joins (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) |
| 16:35:50 | × | kritzefitz quits (~kritzefit@fw-front.credativ.com) (Remote host closed the connection) |
| 16:36:13 | <[exa]> | ok cool, does it work? |
| 16:36:14 | <larou> | now here i can specify the same graph, and using the definition of the input output pairs broken by designating "Sparks" |
| 16:36:28 | <larou> | then, it will return a graph which passes the matrix test |
| 16:36:33 | <larou> | ie, is not cyclic |
| 16:36:42 | <larou> | this is the constraint on the CloseNet constructor |
| 16:36:58 | <larou> | so you can, if you specify the correct sparks, as this check ensures you must |
| 16:37:04 | × | jakob_ quits (~textual@p200300f49f162200c400a7daff5c73c4.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 16:38:01 | <larou> | you add functions to your net any which old way, and ensure that you have a way in mind to break the cycles (where you put the sparks, which inputs matched with outputs you do not pass as internal edges |
| 16:38:03 | <larou> | ) |
| 16:38:15 | <larou> | [exa]: i didnt make a graph yet |
| 16:38:36 | <larou> | i need to shuffle them so the inputs to outputs are well ordered in the list of functions |
| 16:38:40 | × | bob_twinkles quits (~quassel@ec2-52-37-66-13.us-west-2.compute.amazonaws.com) (Read error: Connection reset by peer) |
| 16:38:44 | <larou> | so you can supply inputs to each of them in a fold |
| 16:39:00 | <larou> | and the values it calculates serve as inputs to the rest |
| 16:39:02 | × | knupfer quits (~Thunderbi@200116b82cfb8700fd61a7f6e9856548.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 16:39:17 | <larou> | you specify type level symbols as annotations to the edges of the Net |
| 16:39:26 | <larou> | thats how these new type of trees work |
| 16:39:56 | <larou> | they dont sit underneath each other in a GADT, appearing as a self reference within a list, like a regular tree |
| 16:40:20 | <larou> | so you give each of the edges a label, and have the nodes that are on either end of it both reference that |
| 16:40:35 | → | bob_twinkles joins (~quassel@ec2-52-37-66-13.us-west-2.compute.amazonaws.com) |
| 16:40:38 | <larou> | the matrix is a numerical representation of the resulting adjacency matrix |
| 16:40:45 | <larou> | well, its directed from inputs to outputs |
| 16:41:11 | <larou> | and then you exponentiate that to get, "if it is above itself" which would throw an error as a cycle |
| 16:41:34 | <larou> | the constraint on the CloseNet constructor would not hold |
| 16:41:44 | <larou> | you would have to specify better sparks as a type annotation |
| 16:42:13 | → | invaser1 joins (~Thunderbi@31.148.23.125) |
| 16:42:18 | <larou> | so what do you recon!? solved the ancient, upwards branching trees thing, finally |
| 16:42:25 | <merijn> | I propose implementing a prototype and showing that to people, rather than roughly explaining in english |
| 16:42:27 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 16:42:40 | <larou> | it works as in the links provided |
| 16:42:50 | <[exa]> | cabal install <what> |
| 16:42:52 | <larou> | i dont have it doing what i want yet though |
| 16:43:06 | <merijn> | So...it doesn't work yet |
| 16:43:16 | <larou> | i need to shuffle them so the nodes at the leafs pass inputs along for functions to be evaluated |
| 16:43:30 | <larou> | merijn: exactly what i described is demonstrated in those pastes |
| 16:43:38 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 16:43:41 | <larou> | what it doesnt do yet, it does not yet do |
| 16:43:54 | <larou> | so its not with "the final demo" |
| 16:44:04 | <larou> | which would probably be what you would want |
| 16:44:27 | <larou> | so, basically its a state function |
| 16:44:32 | <larou> | so i can put it on a graph! |
| 16:44:36 | <larou> | and that makes it a monad |
| 16:44:39 | <larou> | which is pretty mad |
| 16:44:47 | <larou> | the "net" thing, with actual functions on |
| 16:44:52 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 260 seconds) |
| 16:44:52 | invaser1 | is now known as invaser |
| 16:44:59 | <larou> | its the monad from; "programs are monads" |
| 16:45:14 | <merijn> | "and that makes it a monad" <- I doubt that without a proof |
| 16:45:14 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 16:45:22 | <larou> | i have explicitly named bound variables expressed at type level |
| 16:45:26 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 16:45:31 | <larou> | meijn: it is a monad though... |
| 16:45:53 | → | justan0theruser joins (~justanoth@unaffiliated/justanotheruser) |
| 16:45:56 | <larou> | you can break programs down and compose them, programs aka functions |
| 16:46:10 | <larou> | anyway, the point is its a *state* |
| 16:46:12 | <larou> | so it changes |
| 16:46:17 | <larou> | the whole program |
| 16:46:26 | <larou> | and thats where these sparks sit, internally as states |
| 16:46:51 | <larou> | they go along internal edges that you have brokn to make them external inputs and outputs directed to a state variable that acts as a memory store |
| 16:46:59 | <[exa]> | larou: it makes no sense, seriously |
| 16:47:20 | <larou> | you have the graph of functions, and with it, all of the spark states, that are returned when you run the function on its inputs and previous spark states |
| 16:47:48 | <larou> | and you package all of that up as a state function |
| 16:48:08 | × | pavonia quits (~user@unaffiliated/siracusa) (Quit: Bye!) |
| 16:48:15 | <larou> | and put it on a graph of functions, with its cycles broken as another layer of sparks, stored as states in another state function wrapper and so on |
| 16:48:19 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 16:48:23 | <larou> | its the "and so on" thats the monadic recursion |
| 16:49:01 | <larou> | nodes, that internally, are graphs of functions |
| 16:49:11 | <larou> | the "nets as neurons" monad |
| 16:49:14 | × | Feuermagier quits (~Feuermagi@213.178.26.41) (Remote host closed the connection) |
| 16:49:36 | <larou> | you partition the program any which way into functions, depending on how you define them and with synonyms |
| 16:49:43 | <larou> | or unpartition it |
| 16:49:47 | <larou> | thats cobind and bind |
| 16:50:08 | <merijn> | Just because you call them that, doesn't mean they obey the monad laws |
| 16:50:15 | <larou> | yeah but they do though |
| 16:50:37 | <larou> | in the same way a tree is |
| 16:50:47 | <larou> | i guess i need them to be nonempty etc |
| 16:50:58 | <larou> | but yeah, theres a monad there, no doubt |
| 16:51:18 | <larou> | anyway, thats not the fun part |
| 16:51:21 | → | alp joins (~alp@2a01:e0a:58b:4920:e0d5:8136:ac9f:8cb7) |
| 16:51:35 | <larou> | the spark states get "hidden" when you package them into a state function wrapper placed on the net |
| 16:51:52 | <larou> | because the net can handle state functions, so the sparks just get absorbed by that machinery |
| 16:52:00 | <larou> | you get new nodes to the graph |
| 16:52:29 | <merijn> | I suggest writing a blogpost, rather than writing a novel in a channel meant for discussion |
| 16:52:42 | <larou> | the spark cycles, end up at an input and output terminus, that stores the spark state, and can be written to and read from |
| 16:52:59 | × | cocreature quits (~cocreatur@eirene.uberspace.de) (Remote host closed the connection) |
| 16:53:05 | <larou> | merijn: thanks for keeping me on track. |
| 16:53:21 | → | cocreature joins (~cocreatur@eirene.uberspace.de) |
| 16:53:22 | <larou> | i have presented these new trees |
| 16:55:22 | × | mananamenos quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 260 seconds) |
| 16:55:33 | <larou> | anyway, all this stuff to do with new nodes for the sparks when the nets handle state functions on the nodes - is just the next part of the todo - and is just to say what i have shown does not yet do |
| 16:55:46 | <larou> | so far it just checks to see that the sparks provided are correct |
| 16:55:56 | <larou> | so you cant make it wrong! |
| 16:56:04 | <larou> | almost as good as making it right... |
| 16:56:41 | <larou> | you basically just have to be sure the edges you define dont cause a cycle |
| 16:56:50 | <larou> | but it will tell you if there is |
| 16:57:27 | <larou> | the only thing worth discussing really is the fact we have a new notion of tree |
| 16:57:36 | <larou> | not, how far i am at making it better |
| 16:57:50 | <larou> | what i show completely defines it |
| 16:58:07 | <larou> | but many other implementations of the same idea exist |
| 16:58:13 | ChanServ | sets mode +q *!*@*/ip.94.174.37.145 |
| 16:58:52 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Ping timeout: 260 seconds) |
| 17:00:02 | → | he9388 joins (2fe3e53b@047-227-229-059.res.spectrum.com) |
| 17:00:28 | <he9388> | Hi everyone, I'm trying to install the Haskell extension for VSCode, and I'm getting the error "Couldn't figure out what GHC version the project is using" |
| 17:00:43 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 17:00:48 | <he9388> | I couldn't figure out what's the issue. Can anyone give a pointer? Thanks a lot. |
| 17:01:04 | <merijn> | are you using stack or cabal? |
| 17:01:17 | <he9388> | Cabal |
| 17:01:32 | <he9388> | Or I believe so at least... |
| 17:01:35 | <merijn> | he9388: Is GHC in your path? |
| 17:01:51 | <he9388> | Which path? |
| 17:01:57 | <he9388> | Sorry, I am beginner :) |
| 17:03:05 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 240 seconds) |
| 17:03:10 | <he9388> | I get some message like this:Couldn't figure out what GHC version the project is using: /home/he/.config/Code/User/globalStorage/haskell.haskell/haskell-language-server-wrapper-0.6.0-linux --project-ghc-version exited with exit code 1: Module "/home/he/Documents/learn4haskell/a" is loaded by Cradle: Cradle {cradleRootDir = |
| 17:03:11 | <he9388> | "/home/he/Documents/learn4haskell", cradleOptsProg = CradleAction: Cabal} Failed to get project GHC version:CradleError {cradleErrorDependencies = [], cradleErrorExitCode = ExitFailure 1, cradleErrorStderr = ["Error when calling cabal v2-exec ghc -v0 -- --numeric-version","","cabal: unrecognised command: v2-exec (try --help)\n"]} |
| 17:03:17 | <merijn> | he9388: Let's rewind further: What OS? :p |
| 17:03:20 | → | jlamothe joins (~jlamothe@198.251.55.207) |
| 17:03:26 | <he9388> | I am on Ubuntu |
| 17:03:41 | <merijn> | he9388: If you run "which ghc" in your shell, what do you get? |
| 17:03:55 | → | byorgey joins (~byorgey@155.138.238.211) |
| 17:04:20 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 17:04:25 | <he9388> | Ok, weird, I ran in two different directory and got two different location :) |
| 17:04:44 | <he9388> | One I get: /usr/bin/ghc. The other: /home/he/.ghcup/bin/ghc |
| 17:05:15 | <merijn> | The first is probably from your package manager, the second from ghcup. So step one is figuring out which you want :p |
| 17:05:26 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 17:05:55 | <he9388> | What's the difference :) |
| 17:06:05 | <monochrom> | Ubuntu's is much older. |
| 17:06:18 | <he9388> | Then probably I'll stick to the new one |
| 17:06:37 | × | ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Remote host closed the connection) |
| 17:06:38 | <monochrom> | How old? How bad? Answer: So old that only a few profs who never take a look at the current outside world still think it's in use. |
| 17:06:52 | → | valdyn joins (~valdyn@host-88-217-143-53.customer.m-online.net) |
| 17:07:20 | <monochrom> | So old that it's like some Windows users hold on to Windows 98 because they still hold on to WinFax. (OK this is an exaggeration.) |
| 17:07:39 | <he9388> | Point taken, ready to get rid of it :) |
| 17:07:58 | → | mananamenos joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 17:08:14 | <merijn> | he9388: Also, ghcup lets you install multiple different versions at the same time so you can test across compiler versions |
| 17:08:22 | <he9388> | What's the proper way to get rid of it |
| 17:08:33 | <monochrom> | sudo apt remove |
| 17:08:50 | <he9388> | oh right |
| 17:08:54 | <he9388> | was almost going to rm -rf it... |
| 17:09:04 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 17:09:24 | <he9388> | now it says ghc not found |
| 17:09:28 | <he9388> | when I run which ghc |
| 17:09:31 | hackage | rosebud 0.2.0.0 - Common rose tree/forest functions https://hackage.haskell.org/package/rosebud-0.2.0.0 (jship) |
| 17:10:05 | <monochrom> | You will need /home/he/.ghcup/bin to be an element of your PATH |
| 17:10:24 | <he9388> | OK, got it! Now this part works |
| 17:11:06 | × | motte quits (~weechat@unaffiliated/motte) (Quit: WeeChat 1.9.1) |
| 17:12:14 | <he9388> | Now I am getting this error message: The Haskell (learn4haskell) server crashed 5 times in the last 3 minutes. The server will not be restarted. |
| 17:12:39 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 17:12:43 | <merijn> | hmm, what's learn4haskell? |
| 17:13:19 | <he9388> | https://github.com/kowainik/learn4haskell |
| 17:13:26 | <he9388> | It's tutorial I'm going through :) |
| 17:13:44 | × | acidjnk_new quits (~acidjnk@p200300d0c719ff57608036dc958592ad.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 17:13:44 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 17:14:01 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 17:14:31 | <merijn> | hmmm |
| 17:14:44 | <he9388> | Why should the extension be dependent on the server? |
| 17:15:15 | <monochrom> | Never heard of it. |
| 17:15:18 | × | jneira quits (02896ac0@gateway/web/cgi-irc/kiwiirc.com/ip.2.137.106.192) (Quit: Ping timeout (120 seconds)) |
| 17:16:11 | <merijn> | he9388: No clue. tbh, the editor plugin landscape has evolved rather dramatically over the past year, but it isn't quite at the "works reliably in all setups" state yet |
| 17:17:01 | <merijn> | That said, for the vast majority of my haskell career I've worked without editor plugins just fine. It's not ideal, but I can't really recommend investing a lot of time into getting it working now |
| 17:17:22 | <he9388> | Having type checking would be nice :) |
| 17:17:40 | <he9388> | I'm just starting to develop |
| 17:18:12 | <merijn> | he9388: Yeah, but the current editor plugin landscape that you can either invest hours fixing things or wait a month and the plugins has improved much more :p |
| 17:18:22 | <monochrom> | -fdefer-type-errors achieves 90% of the same goal at 0.1% of the cost |
| 17:18:43 | <merijn> | monochrom: -fdefer-typed-holes >> -fdefer-type-errors :) |
| 17:19:18 | <merijn> | he9388: You can always try something like ghcid running in a separate terminal |
| 17:19:28 | <monochrom> | It means it demotes die-hard-erroring-out to just warning. This means functions that are unaffected by the type error are still usable, so you can continue to explore and figure out what to do. |
| 17:19:53 | <merijn> | he9388: That gets you 80% of the way there |
| 17:20:16 | <monochrom> | my "cost" refers to installation cost |
| 17:20:59 | <monochrom> | cost of one-time installing extra software and long-time babysitting said fragile perpetually-in-beta-quality software |
| 17:21:05 | <he9388> | Did not know about ghcide either haha |
| 17:21:06 | <monochrom> | s/long-time/long-term/ |
| 17:21:21 | <merijn> | he9388: Confusingly ghcid and ghcide are different things :) |
| 17:21:22 | <monochrom> | Oh, and ghcid != ghcide |
| 17:21:43 | <he9388> | oh |
| 17:21:45 | <monochrom> | This is ghcid: http://hackage.haskell.org/package/ghcid |
| 17:22:05 | <merijn> | he9388: ghcide is what your current plugin probably uses, but it's not as robust as ghcid yet. ghcid is basically a program that just repeatedly runs compile for you and reports errors |
| 17:22:30 | × | larou quits (5eae2591@gateway/web/cgi-irc/kiwiirc.com/ip.94.174.37.145) (Quit: Connection closed) |
| 17:22:51 | <monochrom> | It is just an inotify loop over "oh you have updated Foo.hs again, so let me run ghc again so you see the error messages" |
| 17:23:17 | → | crdrost joins (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) |
| 17:23:32 | <monochrom> | I think it is very misleading to call it anything related to IDE. |
| 17:23:44 | <monochrom> | I would describe it as continuous smoke-testing |
| 17:24:04 | <sm[m]> | I will say that VS Code + Haskell extension is quite likely to just work and give he9388 a really nice experience these days |
| 17:24:15 | <monochrom> | You save a file, it reruns type checking, build checking, and test cases. |
| 17:24:19 | <he9388> | I am using VS Code + Haskell extension actually... |
| 17:24:41 | <sm[m]> | he9388: isn't it giving you realtime type errors, types on hover, etc ? |
| 17:24:50 | <merijn> | monochrom: Well to be fair it was "ghci daemon", presumably |
| 17:25:01 | <merijn> | sm[m]: Well, no, it kept crashing, hence the start of this discussion :p |
| 17:25:08 | <he9388> | Oh, the extension is not loading: when I make new folder, I got "The Haskell (test) server crashed 5 times in the last 3 minutes. The server will not be restarted" |
| 17:25:19 | <sm[m]> | oops, missed that. #haskell-ide-engine would help |
| 17:25:28 | <sm[m]> | would also help. |
| 17:25:35 | <he9388> | Ok, thank you for the reference |
| 17:26:15 | × | aveltras quits (uid364989@gateway/web/irccloud.com/x-jtdricnolbjelrxi) (Quit: Connection closed for inactivity) |
| 17:26:45 | × | christo quits (~chris@81.96.113.213) (Read error: Connection reset by peer) |
| 17:27:09 | → | christo joins (~chris@81.96.113.213) |
| 17:30:37 | × | alp quits (~alp@2a01:e0a:58b:4920:e0d5:8136:ac9f:8cb7) (Ping timeout: 272 seconds) |
| 17:31:06 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-dgisunxwmcstbixs) |
| 17:33:16 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 240 seconds) |
| 17:35:49 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 17:36:27 | × | glguy quits (x@freenode/staff/haskell.developer.glguy) (Ping timeout: 615 seconds) |
| 17:36:51 | → | glguy joins (x@freenode/staff/haskell.developer.glguy) |
| 17:37:25 | × | kav quits (~kari@dsl-hkibng42-56733f-225.dhcp.inet.fi) (Ping timeout: 240 seconds) |
| 17:37:40 | × | valdyn quits (~valdyn@host-88-217-143-53.customer.m-online.net) (Read error: No route to host) |
| 17:37:48 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) () |
| 17:38:20 | × | avn quits (~avn@78-56-108-78.static.zebra.lt) (Ping timeout: 260 seconds) |
| 17:38:51 | × | ph88^ quits (~ph88@2a02:8109:9e00:7e5c:f073:c081:c2ef:433b) (Ping timeout: 272 seconds) |
| 17:38:52 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 17:40:40 | × | Boomerang quits (~Boomerang@xd520f68c.cust.hiper.dk) (Ping timeout: 260 seconds) |
| 17:41:16 | → | alp joins (~alp@2a01:e0a:58b:4920:6867:806e:6b2d:b0d) |
| 17:42:08 | <koz_> | monochrom: I don't recall if it was you, but someone complained that we say 'Big-O', not 'Big-omikron'. Bird and Gibbons' algorithms book is here to right this wrong! |
| 17:42:31 | hackage | easy-args 0.1.0.1 - Parses command line arguments https://hackage.haskell.org/package/easy-args-0.1.0.1 (jlamothe) |
| 17:42:33 | <boxscape> | "Big-omikron" isn't that just regular o |
| 17:42:44 | <merijn> | I say death to Big O analysis :p |
| 17:43:11 | <merijn> | It's just a mathematical way of lying about performance :p |
| 17:43:31 | hackage | cryptol 2.10.0 - Cryptol: The Language of Cryptography https://hackage.haskell.org/package/cryptol-2.10.0 (AaronTomb) |
| 17:43:41 | <c_wraith> | People are very bad at it, and believe lies like "hash table insert and lookup are O(1)" with shocking credulity |
| 17:44:09 | <merijn> | c_wraith: A reasonable number people know about *that* |
| 17:44:24 | × | codeAlways quits (uid272474@gateway/web/irccloud.com/x-rnqcrwigssxuyxdw) (Quit: Connection closed for inactivity) |
| 17:44:30 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 2.8) |
| 17:44:53 | → | avn joins (~avn@78-56-108-78.static.zebra.lt) |
| 17:44:53 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 17:45:15 | <merijn> | The people that realise "the fundamental base of assumption of Big O is just 100% lies" is dramatically less :p |
| 17:46:39 | <boxscape> | which assumption is that? |
| 17:46:51 | <maerwald> | it's one of those things that make you look smart in interviews |
| 17:46:54 | <dminuoso> | boxscape: Stuff like constant random memory access. |
| 17:46:59 | <merijn> | It only seems to work because people in general mostly only care about the happy path |
| 17:47:04 | → | kav joins (~kari@dsl-hkibng42-56733f-225.dhcp.inet.fi) |
| 17:47:14 | <koz_> | maerwald: Alternatively, if you inhabit certain academic spaces. |
| 17:47:17 | <koz_> | (which was my fate) |
| 17:47:22 | <dminuoso> | If that's your model of computation, fine, but the truth of the matter is memory access is not constant on a computer implemented within the laws of physics. |
| 17:47:27 | <merijn> | boxscape: random memory access is constant time |
| 17:47:40 | <c_wraith> | that's only an assumption if you make it one... |
| 17:47:40 | <merijn> | maerwald: It has real world implications |
| 17:47:44 | <boxscape> | is the problem there caching or something else? |
| 17:47:48 | <merijn> | boxscape: Yeah |
| 17:47:51 | <boxscape> | I see |
| 17:47:57 | <koz_> | Yeah, the memory hierarchy is a thing. |
| 17:47:58 | <dminuoso> | boxscape: blackhole thermodynamics and relativity, roughly |
| 17:48:01 | <koz_> | For good reason. |
| 17:48:12 | <merijn> | You can construct algorithms that are "worse" per big O complexity while being *much* faster in reality |
| 17:48:36 | <koz_> | merijn: And that's before we get to abuses of the form 'simplex is exponential'. |
| 17:48:55 | <merijn> | c_wraith: eh, that assumption is baked into classical big O analysis as taught in CS and parroted when talking data structure complexity |
| 17:49:10 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 17:49:24 | <c_wraith> | merijn: hmm. not in my courses/textbooks. They explicitly called out that they were working in the RAM model |
| 17:49:24 | <dminuoso> | c_wraith: Well, the question is what conclusions you can draw from complexity analysis if the model doesn't fit reality well |
| 17:50:22 | × | kav quits (~kari@dsl-hkibng42-56733f-225.dhcp.inet.fi) (Read error: Connection timed out) |
| 17:50:25 | <merijn> | c_wraith: Well, *CLRS* assumes that throughout the book and even calls it out as a wildly unrealistic assumption in the first 1 or 2 chapters |
| 17:50:35 | <merijn> | Anyway, dinner time |
| 17:50:54 | <koz_> | merijn: Yeah, you get this a lot. 'This isn't realistic, but we're just goin' with it.' came up a bunch when I was learning a lot of algorithms-related things. |
| 17:51:00 | <merijn> | c_wraith: What does "RAM model" mean? Did they include caches or not? |
| 17:51:16 | <merijn> | (Actually, don't bother answering, 'cause dinner time :p) |
| 17:51:25 | <koz_> | merijn: I assume Random Access Model. AKA 'all memory is flat, if you have an address, you have that memory in Theta(1)'. |
| 17:51:26 | <c_wraith> | merijn: it's the standard name for the model in which all memory accesses have the same cost |
| 17:52:05 | → | codeAlways joins (uid272474@gateway/web/irccloud.com/x-zbflumxjrtygmhzc) |
| 17:52:08 | → | kav joins (~kari@dsl-hkibng42-56733f-225.dhcp.inet.fi) |
| 17:52:20 | × | toxix quits (~DTZUZU@207.81.171.116) (Ping timeout: 256 seconds) |
| 17:52:23 | <koz_> | I think monochrom (maybe?) mentioned that many presentations of Dijkstra's algorithm straight-up lie about their actual performance because they assume magical thinking in priority changes. |
| 17:54:44 | <monochrom> | Rather, an important implementation question of decrease-priority is grossed over. |
| 17:55:02 | <koz_> | I _love_ the expression 'to gross over'. |
| 17:55:25 | → | wroathe_ joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 17:56:02 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 17:56:04 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Ping timeout: 272 seconds) |
| 17:56:36 | <monochrom> | In practice, I think people just gave up. |
| 17:56:48 | <koz_> | In general, the folks that taught me algorithm-related stuff in CS had an attitude to implementation that was roughly 'ehh, it can be done somehow, who cares, now do more analysis'. |
| 17:57:05 | → | acowley joins (~acowley@c-68-83-22-43.hsd1.nj.comcast.net) |
| 17:57:10 | <koz_> | (one was outright dismissive, the other just mentioned that these issues were resolvable but gave zero explanation how) |
| 17:57:53 | <monochrom> | I have seen programming-contest-quality code libraries that don't use a log-time priority queue at all. Every extract-min and decrease-priority is linear brute-force search over an array. |
| 17:57:58 | × | oerjan quits (~oerjan@195.206.169.184) (Remote host closed the connection) |
| 17:58:03 | wroathe_ | is now known as wroathe |
| 17:58:20 | <monochrom> | Dijkstra himself also said he did that for his first demo, it was fast enough for him. |
| 17:58:53 | <koz_> | monochrom: So wait, their priority queue essentially amounts to Vector (Int, a) or so? |
| 18:00:02 | <monochrom> | I gross over details too. But I make a judgment: If I think an average student can think up how to code it up, I can gross over it; if it would be new and clever to them, I have to spell it out. |
| 18:00:10 | <monochrom> | Yeah! |
| 18:01:00 | <koz_> | Somewhat ironically, this makes me feel better about a recent Real Haskell Job call I had to make. |
| 18:01:03 | <geekosaur> | considering the kinds of things your average student comes up with, you must have to spell things out a lot |
| 18:01:22 | <monochrom> | And this is U of bloody Waterloo world class for-ACM-ICPC has-been-world-champion code library they bring on paper to the contests. |
| 18:01:48 | <monochrom> | Fortunately, it's in C, so it is still fast. >:) |
| 18:02:58 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 18:02:59 | <monochrom> | Oh, to be sure, "average student" still depends on which school we're talking about. |
| 18:03:36 | → | enoq joins (~textual@194-208-146-143.lampert.tv) |
| 18:04:12 | <monochrom> | Suppose you pose the 1st-year-CS problem of "find the max of an array" for example. Actually, more honestly, a word problem that doesn't say outright "find max of array" but if you understand the wordy problem you see it's that. |
| 18:04:42 | <monochrom> | In my school, the average students wouldn't have any difficulty. |
| 18:04:56 | <monochrom> | In U of Waterloo, haha are you kidding, that's too easy. |
| 18:06:18 | → | jneira joins (02896ac0@gateway/web/cgi-irc/kiwiirc.com/ip.2.137.106.192) |
| 18:06:44 | <monochrom> | So, that kind of word problems is the usual kind of problems you see during the warm-up practice stage of an ACM-ICPC-style programming contest. The warm-up practice stage being the whole point being familiarizing yourself with the computing environment, so let's solve a trivial problem so you can focus on learning how to use vi and gcc, say. |
| 18:06:48 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:9217:95c7:973d:d0ad) |
| 18:07:46 | <monochrom> | I overheard the conversation of a team from another school. <Coach> So, what do you think? <Contestant> No clue. |
| 18:08:11 | <monochrom> | That's their contestant. So now imagine the average of that school. But compare to the average of Waterloo. |
| 18:10:08 | <maerwald> | Man. Why not just get under the sun at the beach, instead of all this programming. |
| 18:11:18 | → | foursaph joins (~foursaph@dynamic-077-000-101-034.77.0.pool.telefonica.de) |
| 18:11:25 | ski | . o O ( "The Myth of RAM, part I" by Emil Ernerfeldt in 2014-04-21 at <https://www.ilikebigbits.com/2014_04_21_myth_of_ram_1.html> ) |
| 18:11:28 | <monochrom> | IKR? I saw a lot of people working hard for their 100-metre dash, or marathon, or something. |
| 18:11:43 | <monochrom> | Why not just get a ride? |
| 18:11:54 | <monochrom> | Why not just call uber? |
| 18:11:58 | <koz_> | ski: Thanks! I was hoping someone did a teardown. |
| 18:12:43 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds) |
| 18:13:22 | × | AWizzArd quits (~code@gehrels.uberspace.de) (Changing host) |
| 18:13:22 | → | AWizzArd joins (~code@unaffiliated/awizzard) |
| 18:13:34 | → | toxix joins (~DTZUZU@207.81.171.116) |
| 18:14:12 | → | ph88^ joins (~ph88@2a02:8109:9e00:7e5c:f073:c081:c2ef:433b) |
| 18:15:07 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 18:16:38 | × | jrm quits (~jrm@freebsd/developer/jrm) (Ping timeout: 256 seconds) |
| 18:16:50 | × | Yumasi quits (~guillaume@2a01cb09b06b29ea0877e1bda345185b.ipv6.abo.wanadoo.fr) (Ping timeout: 264 seconds) |
| 18:17:07 | <koz_> | @unmtl StateT s Maybe a |
| 18:17:07 | <lambdabot> | s -> Maybe (a, s) |
| 18:18:28 | → | Tracerneo1 joins (~Tracerneo@193.56.252.12) |
| 18:18:51 | → | neiluj joins (~jco@91-167-203-101.subs.proxad.net) |
| 18:18:51 | × | neiluj quits (~jco@91-167-203-101.subs.proxad.net) (Changing host) |
| 18:18:51 | → | neiluj joins (~jco@unaffiliated/neiluj) |
| 18:19:35 | × | chele quits (~chele@ip5b416ea2.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 18:20:16 | <koz_> | :t guard |
| 18:20:17 | <lambdabot> | Alternative f => Bool -> f () |
| 18:21:11 | <koz_> | And of course 'guard' is from Control.Monad. That odd sock drawer of a module. |
| 18:21:11 | <dolio> | I think people should really leave out the 'black hole' stuff from write-ups like this. |
| 18:23:02 | <koz_> | Rod Downey famously claims that 'it's an open problem' is an 80% accurate heuristic for correct answers to complexity theory questions. At this point, I think 'Control.Monad' is an 80% accurate heuristic for correct answers to 'where on earth in base is this function?'-type questions. |
| 18:23:58 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 18:24:13 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 18:24:22 | <monochrom> | You have to narrow the scope to "combinators that are good for all Applicatives, Alternatives, Monads, or MonadPluses". But yeah. |
| 18:24:27 | × | ph88^ quits (~ph88@2a02:8109:9e00:7e5c:f073:c081:c2ef:433b) (Ping timeout: 272 seconds) |
| 18:24:43 | <koz_> | monochrom: I dunno if I'm just special, but those are the kinds of things I need a lot, and can never find. |
| 18:24:45 | → | conal joins (~conal@64.71.133.70) |
| 18:25:05 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 18:25:21 | <monochrom> | It is historical. 2 decades ago, there was only Functor and Monad, and module-wise there was only Control.Monad, not even Data.Functor, so all the cool tools got into there. |
| 18:25:58 | <monochrom> | I guess 2 decades ago the module name was just Monad, too. |
| 18:26:01 | <ski> | (and before hierarchical, wasn't there just `Monad' ?) |
| 18:26:06 | <monochrom> | Yeah that |
| 18:26:37 | <koz_> | Oh, I get why it is that way. |
| 18:26:44 | <koz_> | It's just amusing to me. |
| 18:27:27 | → | conal joins (~conal@64.71.133.70) |
| 18:27:28 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 18:27:31 | hackage | ivory-avr-atmega328p-registers 0.1.0.0 - Ivory register bindings for the Atmega328p https://hackage.haskell.org/package/ivory-avr-atmega328p-registers-0.1.0.0 (erdeszt) |
| 18:28:49 | × | ulidtko quits (~ulidtko@193.111.48.79) (Read error: Connection reset by peer) |
| 18:29:36 | × | ishutin quits (~Ishutin@92-249-179-45.pool.digikabel.hu) (Ping timeout: 240 seconds) |
| 18:30:33 | → | ishutin joins (~Ishutin@77-234-92-253.pool.digikabel.hu) |
| 18:31:32 | → | conal joins (~conal@64.71.133.70) |
| 18:32:04 | → | mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) |
| 18:32:59 | <monochrom> | I enjoy using history to explain why things suck today. Those who have learned from history are doomed to helplessly watching other people repeat it. |
| 18:33:24 | → | alephu5[m] joins (alephu5mat@gateway/shell/matrix.org/x-ldzorvnirgjegsey) |
| 18:33:37 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 18:35:20 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 18:35:20 | × | avn quits (~avn@78-56-108-78.static.zebra.lt) (Read error: Connection reset by peer) |
| 18:35:29 | → | avn joins (~avn@78-56-108-78.static.zebra.lt) |
| 18:36:28 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Ping timeout: 256 seconds) |
| 18:37:34 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Quit: leaving) |
| 18:38:57 | <koz_> | monochrom: After all, everything is either history or applied history? :P |
| 18:39:01 | × | alp quits (~alp@2a01:e0a:58b:4920:6867:806e:6b2d:b0d) (Ping timeout: 272 seconds) |
| 18:39:57 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 18:40:47 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 18:40:47 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 18:41:02 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 18:42:05 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Ping timeout: 240 seconds) |
| 18:43:07 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 18:45:35 | × | Ariakenom quits (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) (Read error: Connection reset by peer) |
| 18:45:58 | → | Ariakenom joins (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) |
| 18:46:46 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 18:47:13 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 18:47:31 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 18:48:24 | × | thc202 quits (~thc202@unaffiliated/thc202) (Quit: thc202) |
| 18:50:59 | <zincy__> | koz_: Are you by any chance from New Zealand? |
| 18:51:10 | <koz_> | zincy__: I am, by chance, from there. |
| 18:51:19 | <koz_> | Was the Rod Downey mention the giveaway? |
| 18:52:14 | × | jespada quits (~jespada@90.254.245.49) (Ping timeout: 265 seconds) |
| 18:52:55 | <zincy__> | Juspay? |
| 18:53:03 | <koz_> | zincy__: Contractor, but yes. |
| 18:53:22 | <zincy__> | Yes we talked a bit about logic and discrete mathematics there |
| 18:53:32 | <koz_> | Oh hi! |
| 18:53:35 | <zincy__> | hehe |
| 18:53:45 | <zincy__> | Hi |
| 18:54:03 | <koz_> | Guess it figures Haskellers hang out here. |
| 18:54:33 | <zincy__> | Yeah I saw the name and thought hmm that is a familiar name. |
| 18:54:43 | <koz_> | I'm some variant of 'Koz' everywhere. |
| 18:55:16 | → | jespada joins (~jespada@90.254.245.49) |
| 18:55:28 | → | zx__ joins (~oracle@unaffiliated/oracle) |
| 18:55:42 | × | SanchayanM quits (~Sanchayan@223.226.123.235) (Quit: SanchayanM) |
| 18:58:05 | × | kish` quits (~oracle@unaffiliated/oracle) (Ping timeout: 240 seconds) |
| 19:00:07 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 19:01:28 | × | DavidEichmann quits (~david@62.110.198.146.dyn.plus.net) (Remote host closed the connection) |
| 19:01:50 | → | DavidEichmann joins (~david@62.110.198.146.dyn.plus.net) |
| 19:02:21 | → | knupfer joins (~Thunderbi@200116b82cfb870024438394791f27e9.dip.versatel-1u1.de) |
| 19:02:25 | × | Lord_of_Life quits (~Lord@46.217.218.252) (Ping timeout: 240 seconds) |
| 19:02:54 | → | Lord_of_Life joins (~Lord@46.217.218.252) |
| 19:02:54 | × | Lord_of_Life quits (~Lord@46.217.218.252) (Changing host) |
| 19:02:54 | → | Lord_of_Life joins (~Lord@unaffiliated/lord-of-life/x-0885362) |
| 19:03:32 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 19:03:37 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 19:04:14 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Ping timeout: 245 seconds) |
| 19:04:24 | × | berberman_ quits (~berberman@unaffiliated/berberman) (Ping timeout: 240 seconds) |
| 19:04:28 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Ping timeout: 272 seconds) |
| 19:05:11 | → | buckworst joins (~nate@125.161.129.195) |
| 19:05:29 | × | kuribas quits (~user@ptr-25vy0i8y4kl4v762twz.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 19:06:27 | × | buckworst quits (~nate@125.161.129.195) (Client Quit) |
| 19:08:24 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 19:09:31 | × | he9388 quits (2fe3e53b@047-227-229-059.res.spectrum.com) (Remote host closed the connection) |
| 19:11:26 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 272 seconds) |
| 19:13:16 | → | buckworst joins (~nate@125.161.129.195) |
| 19:13:42 | × | DavidEichmann quits (~david@62.110.198.146.dyn.plus.net) (Remote host closed the connection) |
| 19:14:00 | hackage | nonempty-vector 0.2.1.0 - Non-empty vectors https://hackage.haskell.org/package/nonempty-vector-0.2.1.0 (topos) |
| 19:15:01 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 19:15:02 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 19:17:16 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 256 seconds) |
| 19:17:23 | × | bsima quits (~bsima@simatime.com) (Quit: ZNC 1.7.5 - https://znc.in) |
| 19:18:00 | → | bsima joins (~bsima@simatime.com) |
| 19:18:36 | → | Tario joins (~Tario@201.192.165.173) |
| 19:19:13 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 19:23:57 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 19:30:09 | → | comerijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:30:26 | → | nbloomf_ joins (~nbloomf@2600:1700:ad14:3020:c5d0:5105:4451:33e9) |
| 19:31:04 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 246 seconds) |
| 19:31:44 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 19:31:48 | × | st8less quits (~st8less@2603:a060:11fd:0:744d:b66f:d608:4e8e) (Quit: WeeChat 2.9) |
| 19:32:52 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:f4f3:bbb1:9462:91ce) (Ping timeout: 260 seconds) |
| 19:34:04 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 19:35:23 | → | coot joins (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) |
| 19:39:49 | × | Sarma quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds) |
| 19:40:22 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 19:40:34 | × | dcoutts_ quits (~duncan@33.14.75.194.dyn.plus.net) (Ping timeout: 272 seconds) |
| 19:40:35 | × | dustypacer quits (~pi@2600:6c50:80:2f4a:e9d0:6569:1cea:d1d4) (Remote host closed the connection) |
| 19:41:01 | → | dustypacer joins (~pi@2600:6c50:80:2f4a:e9d0:6569:1cea:d1d4) |
| 19:41:42 | × | nbloomf_ quits (~nbloomf@2600:1700:ad14:3020:c5d0:5105:4451:33e9) (Quit: Textual IRC Client: www.textualapp.com) |
| 19:41:58 | → | acidjnk_new joins (~acidjnk@p200300d0c719ff356dc4eeabe79b61ea.dip0.t-ipconnect.de) |
| 19:44:18 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:7958:7d8e:4908:c843) |
| 19:45:05 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 19:47:52 | comerijn | is now known as merijn |
| 19:47:59 | oats | is now known as hafer |
| 19:48:06 | → | EyalSK joins (~EyalSK@bzq-84-109-128-227.red.bezeqint.net) |
| 19:48:06 | × | EyalSK quits (~EyalSK@bzq-84-109-128-227.red.bezeqint.net) (Client Quit) |
| 19:49:57 | → | christo joins (~chris@81.96.113.213) |
| 19:51:57 | → | christo_ joins (~chris@81.96.113.213) |
| 19:51:57 | × | christo quits (~chris@81.96.113.213) (Read error: Connection reset by peer) |
| 19:52:06 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 19:52:12 | → | waskell_ joins (~quassel@d66-183-127-166.bchsia.telus.net) |
| 19:52:41 | × | christo_ quits (~chris@81.96.113.213) (Read error: Connection reset by peer) |
| 19:52:57 | → | christo joins (~chris@81.96.113.213) |
| 19:54:36 | × | waskell quits (~quassel@d66-183-127-166.bchsia.telus.net) (Ping timeout: 260 seconds) |
| 19:54:43 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 19:55:31 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 19:57:17 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 19:57:39 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 20:04:23 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 20:06:29 | → | remby joins (~rg@2607:fea8:2c40:307::1ef6) |
| 20:06:51 | × | Zetagon quits (~leo@c151-177-52-233.bredband.comhem.se) (Remote host closed the connection) |
| 20:09:06 | × | neiluj quits (~jco@unaffiliated/neiluj) (Quit: leaving) |
| 20:10:05 | × | infinity0 quits (~infinity0@freenet/developer/infinity0) (Remote host closed the connection) |
| 20:10:12 | × | knupfer quits (~Thunderbi@200116b82cfb870024438394791f27e9.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 20:10:58 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Ping timeout: 246 seconds) |
| 20:11:47 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 20:12:09 | → | coot_ joins (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) |
| 20:13:31 | hackage | pcg-random 0.1.3.7 - Haskell bindings to the PCG random number generator. https://hackage.haskell.org/package/pcg-random-0.1.3.7 (cchalmers) |
| 20:13:56 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Ping timeout: 256 seconds) |
| 20:13:57 | coot_ | is now known as coot |
| 20:19:12 | × | AlterEgo- quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Quit: Leaving) |
| 20:19:19 | → | buckwors1 joins (~nate@180.251.220.35) |
| 20:19:38 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Remote host closed the connection) |
| 20:19:42 | → | waskell joins (~quassel@d66-183-127-166.bchsia.telus.net) |
| 20:19:43 | × | waskell_ quits (~quassel@d66-183-127-166.bchsia.telus.net) (Ping timeout: 265 seconds) |
| 20:20:17 | × | ClaudiusMaximus quits (~claude@unaffiliated/claudiusmaximus) (Quit: ->) |
| 20:20:25 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 20:21:22 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 20:21:25 | × | buckworst quits (~nate@125.161.129.195) (Ping timeout: 240 seconds) |
| 20:24:48 | → | Deide joins (~Deide@217.155.19.23) |
| 20:29:07 | <dminuoso> | dolio: The black hole stuff is what justifies O(sqrt(n)) for random access. Without it, you'd arrive at the notion that the maximum of information storable in a region of space is defined by its volume, not its surface. |
| 20:29:19 | → | coot joins (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) |
| 20:29:39 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 20:31:27 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 20:31:32 | × | Franciman quits (~francesco@host-82-56-223-169.retail.telecomitalia.it) (Quit: Leaving) |
| 20:31:45 | × | andi- quits (~andi-@NixOS/user/andi-) (Ping timeout: 272 seconds) |
| 20:32:07 | <dolio> | It doesn't justify it for anything close to an approximation of practical situations, though. And I've heard doubt that the theoretical stuff actually means what people say it means. So it's both unnecessary and potentially discredits you. |
| 20:33:01 | <dminuoso> | Well, it just so happens that the O(sqrt(n)) asymptotics nicely match what we observe in cache hierarchies, local storage, remote storage, etc.. |
| 20:33:18 | <dolio> | Right, so you don't need to appeal to black hole stuff. |
| 20:33:31 | hackage | phonetic-languages-permutations 0.1.0.0 - Commonly used versions of the phonetic-languages-common package https://hackage.haskell.org/package/phonetic-languages-permutations-0.1.0.0 (OleksandrZhabenko) |
| 20:33:39 | <dolio> | So don't. |
| 20:33:45 | <dminuoso> | What's the alternative. "Random access is O(sqrt(n)) but I wont tell you why?" |
| 20:34:00 | <dolio> | They already explained why before talking about the black hole stuff. |
| 20:34:26 | <monochrom> | In the interest of pruning dependencies you don't actually use, if your analysis just needs cache hierarchies, prune everything else. |
| 20:35:53 | <dminuoso> | I guess it depends on the audience, really. |
| 20:35:55 | <dolio> | The reason is that nobody actually knows how to effectively cool 3D stuff on the small scale, so memory is effectively planar. |
| 20:36:07 | <dminuoso> | From the theoretical approach of studying real asymptotics, it seems suitable |
| 20:36:26 | <dolio> | And even when you scale up to data centers, you build on the surface of the earth, so you don't actually scale arbitrarily in 3 dimensions. |
| 20:36:28 | <dminuoso> | Fair, I guess that's a good reason |
| 20:37:37 | × | acidjnk_new quits (~acidjnk@p200300d0c719ff356dc4eeabe79b61ea.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 20:38:23 | <dminuoso> | I was just under the impression that complexity analysis didn't just care for "How does this function behave in some arbitrarily fixed region", but about the limiting factor in theory |
| 20:39:30 | <dminuoso> | But your arguments about 2-dimensionality are still valid, as it's reasonable to assume that if we increase memory, we still will approximately only fill the surface of the earth |
| 20:40:15 | <dminuoso> | But then we should take into account that there's large regions on the earth where we wont build data centers |
| 20:40:30 | <dminuoso> | And that we have limited resources to even build memory |
| 20:41:00 | hackage | phonetic-languages-permutations 0.1.1.0 - Commonly used versions of the phonetic-languages-common package https://hackage.haskell.org/package/phonetic-languages-permutations-0.1.1.0 (OleksandrZhabenko) |
| 20:41:07 | → | Boomerang joins (~Boomerang@xd520f68c.cust.hiper.dk) |
| 20:41:29 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-sgcggzhikhhgebxn) (Quit: Connection closed for inactivity) |
| 20:42:25 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 20:42:48 | <dolio> | How is that going to inform a better asymptotic cost of memory access than √n? |
| 20:43:08 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 20:43:34 | <dolio> | You don't need to address every possible nitpick. There just needs to be a reason to use one model over another. |
| 20:45:03 | <dolio> | √n is actually better for a lot of things empirically, regardless of any theoretical justification. The latter only helps you understand why. |
| 20:45:41 | → | andi- joins (~andi-@NixOS/user/andi-) |
| 20:47:11 | → | mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) |
| 20:48:20 | nckx | is now known as jorts |
| 20:49:48 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 20:50:24 | × | borne quits (~fritjof@200116b864eda200f1dc39039d201adf.dip.versatel-1u1.de) (Ping timeout: 240 seconds) |
| 20:50:35 | <monochrom> | More meta-ly, a lot of programmers are unable to accept that we have and use models, not absolute truths; and even that some of those models are purely empirical, i.e., no one bothered to dig deeper for why the model fits observation. |
| 20:51:08 | <monochrom> | Engineers have made peace with that for a long time, and it's why engineers are so successful. |
| 20:51:42 | × | buckwors1 quits (~nate@180.251.220.35) (Quit: WeeChat 2.9) |
| 20:51:42 | <monochrom> | This is one of many aspects programmers still have a long way to go before we can legitimately call them "software engineers". |
| 20:52:21 | <dolio> | And since no one is using black holes for memory (and won't for the forseeable future), that isn't a good explanation for why the model works anyway. |
| 20:53:20 | <monochrom> | From the engineering point of view, a model is judged for merely this: For the scope of your application (possibly very niche and narrow), how much computation you need to get how much prediction accuracy. |
| 20:53:36 | × | foursaph quits (~foursaph@dynamic-077-000-101-034.77.0.pool.telefonica.de) (Ping timeout: 240 seconds) |
| 20:54:01 | <monochrom> | (A scientist then dig deeper for why the model works so nicely, what is the deeper model behind it.) |
| 20:54:11 | <merijn> | monochrom: Not if you're me |
| 20:54:23 | jorts | is now known as nckx |
| 20:54:41 | <merijn> | Then you just go "you guys all suck so hard at engineering I had to spend most of my phd doing the engineering to even investigate these models and now I can't tell you why it works and I blame you" :p |
| 20:55:00 | hackage | phonetic-languages-simplified-common 0.1.0.0 - A simplified version of the phonetic-languages-functionality https://hackage.haskell.org/package/phonetic-languages-simplified-common-0.1.0.0 (OleksandrZhabenko) |
| 20:55:36 | <monochrom> | The fact that programmers are so unhealthy OCD with absolute truths is one of many reasons why I say that programmers are in the same genre as priests. |
| 20:55:37 | × | conal quits (~conal@64.71.133.70) (Read error: Connection reset by peer) |
| 20:55:48 | <alephu5[m]> | monochrom: Do you really think that programmers are more bound to theory than traditional engineers? That's not my experience of the industry at all |
| 20:56:12 | <merijn> | alephu5[m]: His point is that they are, but the industry refuses to acknowledge it |
| 20:56:19 | <merijn> | Which is why they keep building broken trash :p |
| 20:56:33 | <aoei> | monochrom: lmao |
| 20:56:34 | <monochrom> | I am saying that programmers are bound to theory in the wrong way. |
| 20:56:38 | → | conal joins (~conal@64.71.133.70) |
| 20:56:55 | → | Sgeo_ joins (~Sgeo@ool-18b982ad.dyn.optonline.net) |
| 20:57:02 | <aoei> | monochrom: I was in academic science for a few years.. many of those people are also like that :P |
| 20:58:01 | × | seanparsons quits (~sean@cpc145088-gill21-2-0-cust281.20-1.cable.virginm.net) (Quit: ZNC 1.8.1 - https://znc.in) |
| 20:58:06 | <merijn> | Most of the HPC/"empirical" side of CS is a joke, tbh >.> |
| 20:58:32 | <monochrom> | You give a piece of theory to engineers, they take it as a model. It works? Cool. It doesn't work? They just look for another model. |
| 20:59:06 | <aoei> | monochrom: smart folk |
| 20:59:10 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 20:59:21 | <monochrom> | You give a piece of theory to programmers, they take it as a religion. It can only be absolutely true or absolutely heretic. |
| 20:59:45 | × | Sgeo quits (~Sgeo@ool-18b982ad.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 20:59:45 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 21:00:00 | <aoei> | i wonder if programmers is too broad and you mean a specific subset |
| 21:00:16 | <dolio> | Well, it isn't just programmers, either. |
| 21:00:17 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 21:00:22 | <merijn> | monochrom: Pfft, I belief in paraconsistent logics, I'm perfectly happy believing piece of theory to be simultaneously absolutely true *and* heretical :) |
| 21:00:27 | → | seanparsons joins (~sean@cpc145088-gill21-2-0-cust281.20-1.cable.virginm.net) |
| 21:00:29 | <monochrom> | Modulo the programer in question actually has the intellectual capacity to properly read the piece of theory in the first place, of course. |
| 21:00:30 | <alephu5[m]> | But if assumptions A, B and C imply a particular model that fails drastically, it's often useful to the pragmatist to know that the assumptions are wrong |
| 21:00:42 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 21:00:42 | × | zx__ quits (~oracle@unaffiliated/oracle) (Read error: Connection reset by peer) |
| 21:00:44 | <davean> | Yah, and I mean thats also true for one side of it. On the mathematical side its either true of false, on the HW side it can be more varied. Both sides often want approximations. |
| 21:01:39 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 21:01:46 | → | kish` joins (~oracle@unaffiliated/oracle) |
| 21:02:26 | → | bitmagie joins (~Thunderbi@200116b806fd8d007960b9f54c7c6d5e.dip.versatel-1u1.de) |
| 21:03:03 | <dolio> | The usual "theory vs. practice" truism is really a nonsense way of thinking. Theories are useful when they can be applied to practice, and they should be informed and developed by practice. And practice can be assisted by a good/suitable theory. |
| 21:03:46 | <dolio> | Learning a "theory" that never applies to practice is just kind of useless unless you enjoy the activity in itself. |
| 21:04:09 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 21:04:12 | <monochrom> | Yeah. Knuth said: The best theory is inspired by practice. The best practice is inspired by theory. (I forgot whether that's his order haha.) |
| 21:04:19 | × | bitmagie quits (~Thunderbi@200116b806fd8d007960b9f54c7c6d5e.dip.versatel-1u1.de) (Client Quit) |
| 21:05:25 | → | borne joins (~fritjof@200116b864eda200f1dc39039d201adf.dip.versatel-1u1.de) |
| 21:06:00 | → | britva joins (~britva@2a02:aa13:7240:2980:9169:d6ce:8b28:2e63) |
| 21:06:46 | → | Lycurgus joins (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) |
| 21:07:05 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 240 seconds) |
| 21:07:07 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 21:08:17 | <maerwald> | monochrom: you got that wrong... some priests are good people :) |
| 21:08:58 | × | arahael quits (~arahael@125-209-166-120.tpgi.com.au) (Ping timeout: 256 seconds) |
| 21:10:04 | <alephu5[m]> | <dolio "Learning a "theory" that never a"> Isn't that philosophy? |
| 21:11:06 | × | Ariakenom quits (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) (Quit: Leaving) |
| 21:11:08 | → | arahael joins (~arahael@14-203-208-142.tpgi.com.au) |
| 21:11:16 | <davean> | maerwald: unlike any programmers |
| 21:11:28 | <maerwald> | I didn't say thate :p |
| 21:11:34 | <maerwald> | (but I thought it) |
| 21:12:04 | <dolio> | alephu5[m]: Maybe. I don't put a lot of stock in philosophy. :) |
| 21:12:19 | → | sand_dull joins (~theuser@c-73-149-95-105.hsd1.ct.comcast.net) |
| 21:13:40 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Remote host closed the connection) |
| 21:15:06 | × | sand_dull quits (~theuser@c-73-149-95-105.hsd1.ct.comcast.net) (Client Quit) |
| 21:15:10 | Lycurgus | .oO( what part of perpetuating stupid lies about the nature of reality and man's relation to it is good?) |
| 21:15:33 | → | sand_dull joins (~theuser@c-73-149-95-105.hsd1.ct.comcast.net) |
| 21:15:54 | × | Lycurgus quits (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) (Quit: Exeunt) |
| 21:15:55 | glguy | wonders how far back he'd need to read to find Haskell in this |
| 21:16:44 | → | son0p joins (~son0p@181.136.122.143) |
| 21:18:28 | <zincy__> | monochrom: Right, but don't most programmers implicitly accept they are using models? |
| 21:18:56 | <zincy__> | A voltage is never exactly "high" or "low" ... |
| 21:19:59 | <zincy__> | We dont even need electricity to build computers |
| 21:20:05 | × | sand_dull quits (~theuser@c-73-149-95-105.hsd1.ct.comcast.net) (Client Quit) |
| 21:20:19 | <zincy__> | Surely an acceptance of these facts is an implicit agreement that we use models |
| 21:20:21 | <dolio> | Good thing the model doesn't talk about voltages, then. |
| 21:20:34 | → | neiluj joins (~jco@91-167-203-101.subs.proxad.net) |
| 21:20:34 | × | neiluj quits (~jco@91-167-203-101.subs.proxad.net) (Changing host) |
| 21:20:34 | → | neiluj joins (~jco@unaffiliated/neiluj) |
| 21:20:35 | → | sand_dull joins (~theuser@c-73-149-95-105.hsd1.ct.comcast.net) |
| 21:20:44 | <zincy__> | dolio: What do you mean |
| 21:21:18 | <dolio> | If you're not using electricity to implement computation, it wouldn't make much sense for your model of computation to talk about voltages. |
| 21:22:12 | <zincy__> | Yeah |
| 21:22:47 | × | chaosmasttter quits (~chaosmast@p200300c4a70b2a01441f1455f36b3658.dip0.t-ipconnect.de) (Quit: WeeChat 2.9) |
| 21:24:10 | <zincy__> | What is it Marvin Minsky said, a computer is a a physical model of an abstract process. |
| 21:25:10 | × | son0p quits (~son0p@181.136.122.143) (Quit: Lost terminal) |
| 21:25:34 | → | son0p joins (~son0p@181.136.122.143) |
| 21:25:35 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 21:25:55 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 21:26:29 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 21:26:54 | × | zyxtant quits (~zyextant@120.155.30.153) (Ping timeout: 265 seconds) |
| 21:28:07 | × | gienah quits (~mwright@gentoo/developer/gienah) (Quit: leaving) |
| 21:28:44 | × | danvet quits (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) (Ping timeout: 240 seconds) |
| 21:28:57 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 21:29:10 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 21:30:06 | → | knupfer joins (~Thunderbi@200116b82cfb8700905b10fffed96eb6.dip.versatel-1u1.de) |
| 21:30:07 | × | knupfer quits (~Thunderbi@200116b82cfb8700905b10fffed96eb6.dip.versatel-1u1.de) (Client Quit) |
| 21:30:20 | → | knupfer joins (~Thunderbi@87.123.206.167) |
| 21:34:14 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 21:34:16 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 21:35:24 | → | alp joins (~alp@2a01:e0a:58b:4920:8196:f1ff:e993:87c3) |
| 21:36:06 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 21:39:20 | → | Bad_K4rMa joins (~Bad_K4rMa@unaffiliated/rjphares) |
| 21:40:41 | <Bad_K4rMa> | couple haskell books for sale cheap less than 24 hours left: https://www.ebay.com/usr/roph-rjp-nb5hus5uzh |
| 21:41:36 | × | justan0theruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 240 seconds) |
| 21:42:24 | × | sand_dull quits (~theuser@c-73-149-95-105.hsd1.ct.comcast.net) (Ping timeout: 256 seconds) |
| 21:45:13 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Read error: Connection reset by peer) |
| 21:45:38 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 21:47:15 | → | rprije joins (~rprije@124.148.131.132) |
| 21:47:20 | → | aidecoe joins (~aidecoe@unaffiliated/aidecoe) |
| 21:49:01 | → | benb joins (52456307@82-69-99-7.dsl.in-addr.zen.co.uk) |
| 21:49:56 | → | knupfer1 joins (~Thunderbi@200116b82cfb8700286c2aae4538dae1.dip.versatel-1u1.de) |
| 21:49:56 | × | knupfer quits (~Thunderbi@87.123.206.167) (Read error: Connection reset by peer) |
| 21:49:56 | knupfer1 | is now known as knupfer |
| 21:53:42 | × | neiluj quits (~jco@unaffiliated/neiluj) (Quit: leaving) |
| 21:55:15 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 21:55:19 | × | dhouthoo quits (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be) (Quit: WeeChat 2.9) |
| 21:56:03 | → | christo joins (~chris@81.96.113.213) |
| 21:56:53 | → | zerstroyer[m] joins (zerstroyer@gateway/shell/matrix.org/x-thvxsfmerzqegbym) |
| 21:59:54 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Ping timeout: 256 seconds) |
| 22:00:28 | × | christo quits (~chris@81.96.113.213) (Ping timeout: 256 seconds) |
| 22:02:28 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 260 seconds) |
| 22:04:40 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:9217:95c7:973d:d0ad) (Quit: cosimone) |
| 22:06:27 | → | falafel joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) |
| 22:06:44 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Quit: leaving) |
| 22:10:45 | × | hyperisco quits (~hyperisco@d192-186-117-226.static.comm.cgocable.net) (Ping timeout: 240 seconds) |
| 22:14:25 | → | conal joins (~conal@64.71.133.70) |
| 22:16:16 | × | mananamenos quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 246 seconds) |
| 22:18:46 | × | britva quits (~britva@2a02:aa13:7240:2980:9169:d6ce:8b28:2e63) (Quit: This computer has gone to sleep) |
| 22:18:54 | × | cyphase quits (~cyphase@unaffiliated/cyphase) (Ping timeout: 272 seconds) |
| 22:19:25 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 264 seconds) |
| 22:21:27 | × | Bad_K4rMa quits (~Bad_K4rMa@unaffiliated/rjphares) (Ping timeout: 260 seconds) |
| 22:21:39 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 22:21:56 | → | Rudd0 joins (~Rudd0@185.189.115.108) |
| 22:22:22 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 22:22:55 | → | dcoutts_ joins (~duncan@33.14.75.194.dyn.plus.net) |
| 22:24:30 | → | magma joins (~magma@host-87-20-128-180.retail.telecomitalia.it) |
| 22:24:40 | × | magma quits (~magma@host-87-20-128-180.retail.telecomitalia.it) (Read error: Connection reset by peer) |
| 22:26:42 | × | knupfer quits (~Thunderbi@200116b82cfb8700286c2aae4538dae1.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 22:26:48 | → | cyphase joins (~cyphase@unaffiliated/cyphase) |
| 22:28:03 | → | britva joins (~britva@2a02:aa13:7240:2980:9169:d6ce:8b28:2e63) |
| 22:28:43 | × | Boomerang quits (~Boomerang@xd520f68c.cust.hiper.dk) (Ping timeout: 260 seconds) |
| 22:29:12 | hafer | is now known as didymos |
| 22:31:26 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 22:32:12 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds) |
| 22:32:50 | × | britva quits (~britva@2a02:aa13:7240:2980:9169:d6ce:8b28:2e63) (Client Quit) |
| 22:33:08 | × | crdrost quits (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) (Quit: This computer has gone to sleep) |
| 22:37:36 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Ping timeout: 240 seconds) |
| 22:44:00 | × | conal quits (~conal@64.71.133.70) (Ping timeout: 260 seconds) |
| 22:46:35 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:7958:7d8e:4908:c843) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 22:47:12 | → | DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) |
| 22:47:19 | → | conal joins (~conal@ip-66-115-176-195.creativelink.net) |
| 22:47:43 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 256 seconds) |
| 22:47:51 | × | DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection) |
| 22:48:17 | → | DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) |
| 22:48:24 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 22:54:38 | × | p8m_ quits (p8m@gateway/vpn/protonvpn/p8m) (Quit: birdd) |
| 22:54:58 | → | p8m joins (p8m@gateway/vpn/protonvpn/p8m) |
| 22:56:00 | hackage | pandoc 2.11.2 - Conversion between markup formats https://hackage.haskell.org/package/pandoc-2.11.2 (JohnMacFarlane) |
| 22:56:08 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 260 seconds) |
| 22:56:17 | <monochrom> | zincy__: Consider how many programmers simply insist that recursive calls must consume call stack space except for tail recursion under TCO. Especially being very unambiguously specific about "stack", "call stack", and "tail". |
| 22:57:29 | <monochrom> | Here in #haskell we enjoy a pretty good proxy statistics based on the frequency of someone coming in to ask "so, does Haskell do TCO?" |
| 22:57:46 | × | jwynn6 quits (~jwynn6@050-088-122-078.res.spectrum.com) (Ping timeout: 265 seconds) |
| 22:58:34 | <monochrom> | A clear sign that the askers took their models too religiously. |
| 22:58:53 | → | Feuermagier joins (~Feuermagi@213.178.26.41) |
| 22:58:58 | → | crdrost joins (~crdrost@2601:646:8280:85f0:90f7:1b03:f01f:afae) |
| 22:59:19 | → | jwynn6 joins (~jwynn6@050-088-122-078.res.spectrum.com) |
| 23:00:43 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 23:00:43 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Client Quit) |
| 23:01:05 | <monochrom> | OK, at least that's my model of why they ask it. |
| 23:02:41 | toxix | is now known as DTZUZU |
| 23:02:43 | <monochrom> | Better examples would be: hash table lookups are O(1)-time, big-O means worst case. Those they really hold dear to. |
| 23:03:05 | ski | . o O ( TCMC ) |
| 23:03:10 | <dolio> | Haskell's dead. He doesn't do anything. |
| 23:03:44 | <ski> | @where haskel |
| 23:03:44 | <lambdabot> | <http://web.archive.org/web/20070703001910/http://www.cs.chalmers.se/~augustss/pics/haskel.gif> |
| 23:04:37 | <monochrom> | OK, obOnTopic: I'm reading the paper "Splittable Pseudorandom Number Generators using Cryptographic Hashing", it's pretty neat. |
| 23:07:50 | <monochrom> | Heh, actually the only reason it's on-topic is because for some reason Claesen and Palka sent it to the Haskell 2013 Symposium. |
| 23:08:46 | <monochrom> | splittable PRNGs are now a non-Haskell-specific topic, the Java and Rust people are equally interested for concurrent algorithms. |
| 23:10:18 | <dolio> | I'm not sure being on topic here requires not being on topic anywhere else. |
| 23:10:23 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Quit: WeeChat 2.9) |
| 23:10:35 | <monochrom> | OK! |
| 23:10:57 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 23:11:53 | <monochrom> | Conjecture: If Koen Claessen proves P/=NP one day, he'll submit it to a Haskell Symposium or ICFP. >:) |
| 23:12:26 | <Rembane> | ^^ |
| 23:13:42 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 23:14:09 | ski | imagines "You know, I recently proved this cool result : .." in Claessen's voice |
| 23:14:35 | <Rembane> | :D |
| 23:14:56 | <Rembane> | I wonder what the reason is that they started working on the number generators |
| 23:15:00 | <Rembane> | QuickCheck maybe... |
| 23:15:49 | <monochrom> | Yeah, that paper begins with how the old random's split sucked totally for pretty simple QuickCheck use cases. |
| 23:17:02 | <Rembane> | Ha! Nice! :D |
| 23:17:03 | × | andi- quits (~andi-@NixOS/user/andi-) (Ping timeout: 272 seconds) |
| 23:17:43 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 23:18:17 | <monochrom> | This paper and the splitmix paper, together with what the splitmix paper cites and improves upon, all 3 use this basic idea: |
| 23:18:27 | <dolio> | Maybe I shouldn't drag back the previous conversation, but P vs. NP seems like one of the most overhyped problems. |
| 23:18:44 | <dolio> | Probably irrelevant to practice. |
| 23:19:55 | <monochrom> | Your generator state consists of the initial seed, the history of how you got here via splitting (a list of lefts and rights), and how many times you've called "next". |
| 23:20:14 | <monochrom> | And your random number is simply the hash of that state. |
| 23:20:46 | → | magma joins (~magma@host-87-20-128-180.retail.telecomitalia.it) |
| 23:21:26 | → | andi- joins (~andi-@NixOS/user/andi-) |
| 23:21:30 | <monochrom> | The implementation details are what hashing to use, and how to make that incremental so you never rehash the same lengthy history prefix. |
| 23:22:03 | → | erisco joins (~erisco@d24-57-249-233.home.cgocable.net) |
| 23:22:24 | <Rembane> | It's beautiful. |
| 23:22:37 | <Rembane> | How do you know if you should pick left or right? |
| 23:23:00 | <davean> | The operation you're doing defines which you're doing. |
| 23:23:06 | <monochrom> | Say my history is <left, right, left>, and I call split. |
| 23:23:30 | <monochrom> | Now the two new states are <left, right, left, left> and <left, right, left, right>, respectively |
| 23:24:12 | → | Franciman joins (~francesco@host-82-56-223-169.retail.telecomitalia.it) |
| 23:24:17 | × | magma quits (~magma@host-87-20-128-180.retail.telecomitalia.it) (Client Quit) |
| 23:24:44 | <monochrom> | split (seed, history, counter) = ((seed, history++[left], counter), (seed, history++[right], counter)) |
| 23:25:19 | × | Franciman quits (~francesco@host-82-56-223-169.retail.telecomitalia.it) (Client Quit) |
| 23:25:28 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 23:25:30 | hackage | codeworld-api 0.7.0 - Graphics library for CodeWorld https://hackage.haskell.org/package/codeworld-api-0.7.0 (ChrisSmith) |
| 23:26:18 | <monochrom> | Now you need to bet everything on the quality of your hash function, yeah. :) |
| 23:26:28 | × | theorbtwo quits (~theorb@cpc81822-swin19-2-0-cust3.3-1.cable.virginm.net) (Ping timeout: 260 seconds) |
| 23:27:21 | <Rembane> | Oh. Got it! That's clever. |
| 23:27:23 | <monochrom> | splitmix basically just ran DieHard1 etc and reported very good scores. |
| 23:27:30 | hackage | zydiskell 0.1.1.0 - Haskell language binding for the Zydis library, a x86/x86-64 disassembler. https://hackage.haskell.org/package/zydiskell-0.1.1.0 (nerded) |
| 23:27:55 | <monochrom> | Claessen and Palka's simply went crypto. |
| 23:28:09 | → | christo joins (~chris@81.96.113.213) |
| 23:29:36 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 23:29:52 | → | xerox_ joins (~xerox@unaffiliated/xerox) |
| 23:32:08 | <monochrom> | The next cleverness is how to eliminate storing that lengthy history, bringing the time cost back down to O(1) regardless of how many times you've called split. |
| 23:33:31 | × | son0p quits (~son0p@181.136.122.143) (Quit: leaving) |
| 23:33:31 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 23:34:02 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 23:34:42 | <monochrom> | For Claessen and Palka, it turns out that popular crypto hash functions run a block cipher for as many rounds as your input (which is the history here), so you can just save "the hash so far" instead of the full history. |
| 23:35:22 | <monochrom> | For splitmix, the hash is an inner product, so again you can just save "the inner product so far". |
| 23:35:37 | <monochrom> | actually s/inner/dot/ to be specific. |
| 23:36:20 | → | elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) |
| 23:37:07 | → | hekkaidekapus{ joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 23:37:09 | <monochrom> | Those two papers are both very fun and pleasing to read. |
| 23:37:10 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 23:37:35 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 23:38:00 | → | jayw99 joins (2fe3e53b@047-227-229-059.res.spectrum.com) |
| 23:38:16 | <jayw99> | hi! is there a way to use the @ syntax for data types defined as records |
| 23:38:23 | × | hekkaidekapus_ quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds) |
| 23:38:42 | <jayw99> | say I have: data A = A { field :: Int } |
| 23:38:53 | <jayw99> | and i want to make a function f {field=f} |
| 23:39:02 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 23:39:04 | <jayw99> | is there a way to do something like f a@{field=f} |
| 23:39:06 | <monochrom> | f x@A{field=y} = y+1 |
| 23:39:21 | <jayw99> | oh you have to have the A |
| 23:39:27 | <monochrom> | Yeah, that's all. |
| 23:39:28 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 23:39:34 | <jayw99> | thx! |
| 23:40:07 | × | benb quits (52456307@82-69-99-7.dsl.in-addr.zen.co.uk) (Remote host closed the connection) |
| 23:40:56 | × | Chi1thangoo quits (~Chi1thang@87.112.60.168) (Ping timeout: 240 seconds) |
| 23:41:43 | × | hekkaidekapus{ quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds) |
| 23:45:04 | × | jayw99 quits (2fe3e53b@047-227-229-059.res.spectrum.com) (Ping timeout: 245 seconds) |
| 23:48:51 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 23:48:51 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 23:49:01 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 23:49:11 | → | acidjnk_new joins (~acidjnk@p200300d0c719ff356dc4eeabe79b61ea.dip0.t-ipconnect.de) |
| 23:49:54 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 23:52:31 | hackage | yi-language 0.19.0 - Collection of language-related Yi libraries. https://hackage.haskell.org/package/yi-language-0.19.0 (TomMurphy) |
| 23:56:48 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 23:56:58 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 23:58:18 | → | falafel_ joins (~falafel@c-73-79-82-198.hsd1.pa.comcast.net) |
| 23:58:38 | → | p-core1 joins (~Thunderbi@2a0e:1c80:4:1023::1004) |
| 23:58:45 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 23:58:46 | → | hekkaidekapus{ joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 23:59:26 | × | p-core quits (~Thunderbi@2001:718:1e03:5128:2ab7:7f35:48a1:8515) (Ping timeout: 264 seconds) |
| 23:59:26 | p-core1 | is now known as p-core |
All times are in UTC on 2020-11-19.