Logs on 2021-12-30 (liberachat/#haskell)
| 00:00:03 | <geekosaur> | this is a common mistake with concurrency in Haskell |
| 00:00:16 | <Henson> | how would a thread be defined incorrectly? |
| 00:00:33 | <geekosaur> | generally its operations are too lazy |
| 00:01:17 | <Henson> | would doing a single putStr "." to fix the problem be something that would be a hallmark of this kind of problem? |
| 00:01:33 | <geekosaur> | it can be, yes |
| 00:01:36 | × | vglfr quits (~vglfr@88.155.24.19) (Ping timeout: 245 seconds) |
| 00:01:39 | <Henson> | ok, that might be what's going on |
| 00:01:58 | <geekosaur> | if that forces everything else to happen instead of being passed back as one big unevaluated thunk |
| 00:02:10 | → | vglfr joins (~vglfr@88.155.24.19) |
| 00:02:45 | <geekosaur> | at this point, since we can't see the code, it might be best to point you to |
| 00:02:50 | <geekosaur> | @where parconc |
| 00:02:50 | <lambdabot> | https://www.safaribooksonline.com/library/view/parallel-and-concurrent/9781449335939/ |
| 00:04:10 | <EvanR> | Henson, btw, are you using unsafePerformIO anywhere? |
| 00:04:11 | <Henson> | the thread is just a function that calls a C function to get an image from the camera, then puts that image onto the end of a list in an MVar. I just call "handle <- async functionName" to get it rolling, then later "cancel handle" it. |
| 00:04:37 | <EvanR> | or unsafeInterleaveIO |
| 00:05:04 | <geekosaur> | use $! whenh setting the MVar, maybe |
| 00:05:17 | <glguy> | mjrosenb: I cleaned up that solution to deal with the off-by-one-turn "error" I introduced and worked around :) now it probably looks even more like yours https://glguy.net/advent/sln_2021_21/Main.html |
| 00:05:18 | <EvanR> | because normally when you fork a thread, it definitely runs |
| 00:05:25 | <Henson> | EvanR: no, all of the functions calling the camera functions happen in IO. They're also defined as "foreign import ccall unsafe" which apparently can block the calling thread until the function returns, which I think is resonable. I don't know if it block the entire runtime, or just the thread calling it. Each camera has these functions called by a separate Haskell thread. |
| 00:05:27 | <geekosaur> | otherwise the MVar ends up a list of thunks to be evaluated later |
| 00:05:30 | <EvanR> | regardless of whether someone evaluates something somewhere |
| 00:05:57 | <EvanR> | are you using the -threaded flag |
| 00:06:05 | <Henson> | EvanR: yeah, even without the printing, the thread does run, but very unreliably and sporadically |
| 00:06:08 | <Henson> | EvanR: yes |
| 00:06:28 | <geekosaur> | unsafe has a number of side effects, some of which may be unexpected (like preventing garbage collection) |
| 00:07:11 | <geekosaur> | and will blokc the runtime if not -threaded and possibly even with -threaded (moral: never use unsafe if it blocks. really.) |
| 00:07:20 | <Henson> | geekosaur: should I be using "safe" instead? |
| 00:08:29 | <Henson> | geekosaur: setting the MVar like this: putMVar $! mvarName mvarContents |
| 00:08:56 | <EvanR> | that definitely evaluates mvarName |
| 00:09:07 | <EvanR> | maybe that's the problem, you missed |
| 00:09:08 | <geekosaur> | putMVar mvarName $! mvarContents |
| 00:09:28 | <geekosaur> | the other would be a type error because it treats mvarName as a function |
| 00:10:04 | <geekosaur> | and yes, "safe" is preferable. it's slightly slower with respect to Haskell but avoids a lot of problems and won't break unexpectedly |
| 00:10:19 | <hpc> | generally you don't want to "unsafe" unless you know what you're doing |
| 00:11:13 | <hpc> | it's not one of those goofy keywords that doesn't have a human-interpretable meaning, it's there to make you look at it |
| 00:11:18 | → | alx741 joins (~alx741@157.100.93.160) |
| 00:14:08 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 00:14:08 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 00:14:11 | allbery_b | is now known as geekosaur |
| 00:17:13 | × | DNH quits (~DNH@2a02:8108:1100:16d8:7898:e7cb:a448:daff) (Quit: Textual IRC Client: www.textualapp.com) |
| 00:17:45 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 00:17:45 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 00:17:45 | → | wroathe joins (~wroathe@user/wroathe) |
| 00:18:45 | <Henson> | hpc: well, it looks like changing "unsafe" to "safe" makes it work now. I wrote the FFI part of the code several years ago, and at the time I guess I thought "unsafe" was the right choice. You're right about the name implying that it's not safe to use, but for some reason I've since forgotten I chose to use it. Obviously I chose poorly :-) |
| 00:19:25 | <Henson> | geekosaur: does the $! for setting the MVar also apply to TVars? Can I do something like "atomically $ writeTVar tvarName $! contents" ? |
| 00:20:19 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 00:20:56 | → | Omen joins (~Omen@2600:1702:2e30:1a40:8511:a2a3:f354:5a5e) |
| 00:21:03 | <EvanR> | unsafe comes with extra caveats and requirements to satisfy, things the compiler can't check |
| 00:21:27 | → | desantra joins (~skykanin@user/skykanin) |
| 00:21:31 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 00:21:54 | <Henson> | EvanR: is "safe" the call that blocks Haskell? Does it only block the thread that is calling it, or the whole runtime? |
| 00:22:00 | <hpc> | if that's just strict ($) i don't see why not |
| 00:22:17 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 00:22:18 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:23:29 | <EvanR> | your thread blocks until the call returns regardless. Blocking the whole runtime is a function of -threaded or not, number of capabilities, I'm not sure what the interactions are |
| 00:23:42 | <Henson> | ok, I've got some directions to investigate. It seems to work now with "safe" and MVars, so I'll go back to the TVar code add switch to "safe" and see if that works, and add "$!" if it doesn't help. |
| 00:26:03 | <EvanR> | you can also do |
| 00:26:07 | <EvanR> | evaluate contents |
| 00:26:21 | <EvanR> | atomically (writeTVar tv contents) |
| 00:26:50 | <Henson> | EvanR: so with "-threaded" it should be similar to calling the image capture functions from C threads, right? Haskell doesn't have something like the GIL in Python where it doesn't do concurrency well. From what I've read, Haskell should have excellent concurrency and multi-processing abilities, right? |
| 00:26:57 | <geekosaur> | it's just strict $ and yes that should also work |
| 00:27:13 | <geekosaur> | as long as you use -threaded, yes |
| 00:27:45 | <geekosaur> | note that not using -threaded can lead to some not well tested areas of the runtime, although it's also more debuggable for non-RTS-related stuff |
| 00:28:06 | <geekosaur> | but if you're using threads like this you *really* want -threaded |
| 00:28:52 | <geekosaur> | this said, iirc even without -threaded a call like that will be run separately in an RTS-owned thread and let the rest of the program run normally |
| 00:29:44 | <geekosaur> | (unless you use "unsafe", in which case on your own head be it) |
| 00:31:20 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 00:31:49 | <Henson> | geekosaur: haha, "on your own head be it" :-) |
| 00:31:53 | <monochrom> | Haha would be funny if it's just a matter of -threaded all along. |
| 00:31:59 | <Henson> | hahaha |
| 00:32:10 | <EvanR> | yeah I asked that almost first thing |
| 00:32:22 | <EvanR> | when I saw unsafe |
| 00:32:40 | <Henson> | geekosaur: this will be running on a multi-core system, and the plan is to make liberal use of threads and all the system's cores |
| 00:32:48 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 00:34:07 | <monochrom> | You should default to "safe" until you have hard proof that performance matters to the point you need "unsafe", and even then you pay a price somewhere else and you need to decide if it's worth it. |
| 00:34:20 | → | zaquest joins (~notzaques@5.130.79.72) |
| 00:34:33 | <Henson> | monochrom: ok |
| 00:34:51 | <monochrom> | And it is a trivally easy default. If you don't say "unsafe" then it's "safe". Yes, one of those nice times when it takes effort to add a bug. |
| 00:35:15 | × | waleee quits (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 268 seconds) |
| 00:35:24 | <hpc> | once you're using -threaded there's various things you can try to make sure your ffi stays on one capability and the rest of the code stays well away from it |
| 00:35:45 | <hpc> | that might minimize the "ffi halting other threads" thing |
| 00:36:39 | → | waleee joins (~waleee@h-98-128-229-110.NA.cust.bahnhof.se) |
| 00:37:07 | × | madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 256 seconds) |
| 00:37:50 | <Henson> | hpc: what kinds of things? |
| 00:38:50 | → | alx741 joins (~alx741@157.100.93.160) |
| 00:40:47 | <hpc> | forkOS, and a thing i don't remember the name for that decides what capabilities a forkIO thread can live on |
| 00:40:49 | <Henson> | by the way, everyone, thanks so much for all your advice. I've got several avenues to pursue to try to resolve the problem. |
| 00:41:14 | <Henson> | hpc: something about pinned OS threads, right? |
| 00:41:43 | <hpc> | something like that? i have never had a use case for it so it was always "oh that's neat" whenever i scroll through haddock |
| 00:48:47 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 00:51:34 | × | desantra quits (~skykanin@user/skykanin) (Quit: WeeChat 3.3) |
| 00:51:58 | → | mvk joins (~mvk@2607:fea8:5cdd:f000::917a) |
| 00:52:28 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 00:53:56 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 00:53:56 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 00:54:25 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 00:55:27 | → | perrierjouet joins (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) |
| 00:55:33 | → | AlexNoo__ joins (~AlexNoo@94.233.241.181) |
| 00:55:43 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Remote host closed the connection) |
| 00:56:07 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 00:58:32 | × | AlexNoo_ quits (~AlexNoo@94.233.241.181) (Ping timeout: 240 seconds) |
| 01:02:24 | × | jgeerds quits (~jgeerds@55d4ac73.access.ecotel.net) (Ping timeout: 268 seconds) |
| 01:04:53 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 01:11:16 | × | phma quits (~phma@2001:5b0:211f:d0f8:a0d5:904f:4002:7904) (Read error: Connection reset by peer) |
| 01:11:44 | → | phma joins (phma@2001:5b0:211f:d0f8:a0d5:904f:4002:7904) |
| 01:12:05 | → | yauhsien joins (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
| 01:12:17 | → | alx741 joins (~alx741@157.100.93.160) |
| 01:14:34 | × | infinity0 quits (~infinity0@occupy.ecodis.net) (Ping timeout: 260 seconds) |
| 01:14:46 | → | infinity0 joins (~infinity0@occupy.ecodis.net) |
| 01:16:47 | × | yauhsien quits (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Ping timeout: 256 seconds) |
| 01:19:32 | × | otherwise quits (~otherwise@c-71-231-39-206.hsd1.wa.comcast.net) (Ping timeout: 240 seconds) |
| 01:23:01 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 01:30:53 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 01:36:42 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 01:40:37 | × | acidjnk quits (~acidjnk@pd9e0bdc0.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 01:41:30 | → | kmein joins (~weechat@user/kmein) |
| 01:42:49 | × | kmein quits (~weechat@user/kmein) (Client Quit) |
| 01:43:05 | → | kmein joins (~weechat@user/kmein) |
| 01:46:24 | × | kmein quits (~weechat@user/kmein) (Client Quit) |
| 01:46:42 | → | kmein joins (~weechat@user/kmein) |
| 01:48:42 | → | alx741 joins (~alx741@157.100.93.160) |
| 01:50:29 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 268 seconds) |
| 01:51:55 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 01:51:55 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 01:51:55 | → | wroathe joins (~wroathe@user/wroathe) |
| 01:52:20 | × | Morrow quits (~quassel@bzq-110-168-31-106.red.bezeqint.net) (Remote host closed the connection) |
| 01:53:05 | → | lavaman joins (~lavaman@98.38.249.169) |
| 01:54:09 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 01:54:13 | → | gcdotdev joins (~gcdotdev@user/gcdotdev) |
| 01:54:32 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 01:56:39 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 01:56:57 | → | kmein joins (~weechat@user/kmein) |
| 01:57:23 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 250 seconds) |
| 01:59:03 | × | gcdotdev quits (~gcdotdev@user/gcdotdev) (Quit: Client closed) |
| 02:05:22 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 02:06:18 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 02:06:33 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 02:07:08 | → | otherwise joins (~otherwise@c-73-221-44-172.hsd1.wa.comcast.net) |
| 02:10:27 | × | fjmorazan quits (~quassel@user/fjmorazan) (Quit: fjmorazan) |
| 02:11:00 | → | fjmorazan joins (~quassel@user/fjmorazan) |
| 02:11:45 | × | curiousgay quits (~curiousga@77-120-141-90.kha.volia.net) (Ping timeout: 256 seconds) |
| 02:12:08 | → | alx741 joins (~alx741@157.100.93.160) |
| 02:14:31 | × | Tuplanolla quits (~Tuplanoll@91-159-69-90.elisa-laajakaista.fi) (Quit: Leaving.) |
| 02:18:15 | → | moonlighter69 joins (~moonlight@47.146.14.64) |
| 02:18:41 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 02:26:23 | × | ajb quits (~ajb@cupid.whatbox.ca) (Remote host closed the connection) |
| 02:28:14 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 02:28:33 | → | kmein joins (~weechat@user/kmein) |
| 02:29:04 | × | moonlighter69 quits (~moonlight@47.146.14.64) (Remote host closed the connection) |
| 02:31:36 | × | kmein quits (~weechat@user/kmein) (Client Quit) |
| 02:31:52 | → | kmein joins (~weechat@user/kmein) |
| 02:33:01 | × | infinity0 quits (~infinity0@occupy.ecodis.net) (Ping timeout: 240 seconds) |
| 02:33:48 | × | kmein quits (~weechat@user/kmein) (Client Quit) |
| 02:34:06 | → | kmein joins (~weechat@user/kmein) |
| 02:34:21 | → | ajb joins (~ajb@cupid.whatbox.ca) |
| 02:34:27 | → | infinity0 joins (~infinity0@occupy.ecodis.net) |
| 02:35:19 | × | kmein quits (~weechat@user/kmein) (Client Quit) |
| 02:35:37 | → | kmein joins (~weechat@user/kmein) |
| 02:36:43 | → | alx741 joins (~alx741@157.100.93.160) |
| 02:37:15 | × | waleee quits (~waleee@h-98-128-229-110.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 02:38:48 | × | kmein quits (~weechat@user/kmein) (Client Quit) |
| 02:38:57 | × | neurocyte0132889 quits (~neurocyte@user/neurocyte) (Ping timeout: 240 seconds) |
| 02:39:07 | → | kmein joins (~weechat@user/kmein) |
| 02:41:13 | × | octeep[m] quits (~octeepoct@2001:470:69fc:105::1:3dbf) (Quit: Client limit exceeded: 20000) |
| 02:43:54 | → | waleee joins (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
| 02:45:45 | × | xff0x quits (~xff0x@port-92-193-205-13.dynamic.as20676.net) (Ping timeout: 256 seconds) |
| 02:46:48 | → | Codaraxis_ joins (~Codaraxis@user/codaraxis) |
| 02:47:46 | → | xff0x joins (~xff0x@2001:1a81:527e:7f00:c95b:8db9:d638:e5ae) |
| 02:50:51 | × | Codaraxis quits (~Codaraxis@user/codaraxis) (Ping timeout: 256 seconds) |
| 02:54:36 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 02:58:36 | × | Movedtosridoneem quits (~sridmatri@2001:470:69fc:105::1c2) (Quit: Client limit exceeded: 20000) |
| 02:59:14 | → | n3rdy1 joins (~n3rdy1@2600:1700:4570:3480::41) |
| 03:07:42 | × | infinity0 quits (~infinity0@occupy.ecodis.net) (Remote host closed the connection) |
| 03:12:12 | × | perrierjouet quits (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Quit: WeeChat 3.4) |
| 03:12:12 | → | alx741 joins (~alx741@157.100.93.160) |
| 03:12:30 | → | infinity0 joins (~infinity0@occupy.ecodis.net) |
| 03:12:34 | → | yauhsien joins (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
| 03:19:27 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 03:23:07 | → | perrierjouet joins (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) |
| 03:23:32 | × | danso quits (~danso@2001:1970:52e7:d000:96b8:6dff:feb3:c009) (Ping timeout: 240 seconds) |
| 03:23:32 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 03:24:46 | → | danso joins (~danso@2001:1970:52e7:d000:96b8:6dff:feb3:c009) |
| 03:25:28 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 268 seconds) |
| 03:37:17 | × | danso quits (~danso@2001:1970:52e7:d000:96b8:6dff:feb3:c009) (Ping timeout: 240 seconds) |
| 03:39:16 | × | kupi quits (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 03:40:12 | → | alx741 joins (~alx741@157.100.93.160) |
| 03:44:16 | → | danso joins (~danso@d67-193-121-2.home3.cgocable.net) |
| 03:47:49 | × | waleee quits (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 240 seconds) |
| 03:47:56 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:47:56 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:47:56 | finn_elija | is now known as FinnElija |
| 03:52:39 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 03:53:17 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 03:56:01 | × | td_ quits (~td@muedsl-82-207-238-009.citykom.de) (Ping timeout: 256 seconds) |
| 03:57:30 | → | td_ joins (~td@94.134.91.217) |
| 04:07:39 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.4) |
| 04:08:34 | × | SummerSonw quits (~The_viole@203.77.49.232) (Quit: Leaving) |
| 04:08:50 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 04:10:13 | <InternetCitizen> | why is Text so much faster than [Char] ? |
| 04:10:23 | <InternetCitizen> | is it some sort of Array Char? |
| 04:10:25 | → | octeep[m] joins (~octeepoct@2001:470:69fc:105::1:3dbf) |
| 04:10:39 | → | SridharRatnakum4 joins (~sridmatri@2001:470:69fc:105::1c2) |
| 04:10:41 | → | alx741 joins (~alx741@157.100.93.160) |
| 04:14:57 | × | SummerSonw quits (~The_viole@203.77.49.232) (Ping timeout: 240 seconds) |
| 04:15:37 | × | yauhsien quits (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
| 04:18:19 | × | whatsupdoc quits (uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:18:21 | → | Morrow joins (~quassel@bzq-110-168-31-106.red.bezeqint.net) |
| 04:20:30 | <InternetCitizen> | it comes down to an Internal `!Array` where `data Array = ByteArray ByteArray#` |
| 04:21:08 | <InternetCitizen> | what do the ! and # mean? |
| 04:22:16 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 04:29:23 | → | mbuf joins (~Shakthi@122.162.67.169) |
| 04:29:25 | <EvanR> | strict Text is implemented as an array, while [Char] is a linked list |
| 04:29:31 | <EvanR> | of individual Chars |
| 04:30:02 | <EvanR> | ! in data types indicates a strict field |
| 04:30:21 | <EvanR> | # is found in primitives |
| 04:30:26 | → | deadmarshal joins (~deadmarsh@95.38.115.121) |
| 04:37:39 | × | dsrt^ quits (~dsrt@207.5.54.6) (Remote host closed the connection) |
| 04:40:16 | → | alx741 joins (~alx741@157.100.93.160) |
| 04:44:37 | × | n3rdy1 quits (~n3rdy1@2600:1700:4570:3480::41) (Ping timeout: 240 seconds) |
| 04:52:35 | <InternetCitizen> | EvanR: what does it mean for ByteArray to be a primitive? could I expect it to be a u8* in LLVM? |
| 04:54:15 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 04:58:55 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 05:00:26 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 05:01:20 | <catern> | what do you call a language which distinguishes pure and impure functions? (the obvious answer is "functional" but making such a distinction doesn't require you to have first-class functions) |
| 05:02:28 | → | alfonsox joins (~quassel@103.92.42.182) |
| 05:02:37 | × | mvk quits (~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds) |
| 05:07:55 | <maerwald[m]> | catern: huh? |
| 05:08:06 | <maerwald[m]> | That somehow makes no sense |
| 05:08:49 | <remexre> | catern: "effect typed" maybe? |
| 05:09:34 | <maerwald[m]> | 1. there are pure and non-pure functional languages, 2. Haskell does NOT distinguish between pure and impure functions (which is why unsafeperformIO is so dangerous) |
| 05:10:26 | × | phma quits (phma@2001:5b0:211f:d0f8:a0d5:904f:4002:7904) (Read error: Connection reset by peer) |
| 05:11:53 | → | phma joins (phma@2001:5b0:211f:42c8:a947:49ab:30cf:8035) |
| 05:12:14 | <int-e> | glguy: yeah, that's the kind of code I got, though it's more, uhm, monolithic (and handles the alternation between players differently): https://paste.tomsmeding.com/7eezQWz5 |
| 05:12:16 | <catern> | maerwald[m]: re 1, yes that's another great reason why "functional" is the wrong answer. re 2, it does if you ignore unsafePerformIO and friends |
| 05:12:26 | <int-e> | (slightly cleaned up from my previous paste) |
| 05:12:30 | <catern> | remexre: maybe but that's a little verbose... |
| 05:12:33 | <maerwald[m]> | catern: 2. No, it doesn't |
| 05:12:45 | <catern> | remexre: and you wouldn't usually say that about Haskell |
| 05:12:46 | <maerwald[m]> | Then you have a misconception of what purity is |
| 05:12:49 | → | alx741 joins (~alx741@181.199.42.79) |
| 05:12:51 | <int-e> | (still uncommented though) |
| 05:13:17 | <maerwald[m]> | all functions in Haskell are pure to the compiler |
| 05:13:38 | <maerwald[m]> | The compiler knows nothing about IO and it isn't treated special |
| 05:13:53 | <remexre> | catern: I wouldn't b/c haskell doesn't make that distinction; I would agree with maerwald; (a -> m b) is a pure function in the absence of shenanigans |
| 05:14:06 | <catern> | fine, fine |
| 05:14:21 | <catern> | what do you call a language which distinguishes pure and impure expressions? |
| 05:14:37 | <maerwald[m]> | I'm not sure such a language exists even |
| 05:14:43 | <remexre> | Koka does, doesn't it? |
| 05:14:53 | <catern> | (haskell clearly does...) |
| 05:14:58 | → | notzmv joins (~zmv@user/notzmv) |
| 05:15:51 | <maerwald[m]> | remexre: does the compiler know about purity and automatically distinguish that, regardless of types? |
| 05:16:02 | <remexre> | catern: is `Reader (\x -> x)` a pure or impure expression |
| 05:16:33 | <int-e> | glguy: oh and I didn't do anything clever (\live wins -> 27*live - wins) for the accounting the number of positions since the main point for me was asymptotic performance |
| 05:16:50 | <remexre> | maerwald[m]: I believe so |
| 05:17:19 | <maerwald[m]> | Even C compilers have a concept of pure functions, but you annotate them as such and the compiler will make no effort to prove it |
| 05:17:31 | <glguy> | int-e: I don't know if that was clever or not... I was torn between computing that directly and indirection as in my solution so taht I could have a simpler unfoldr generated list |
| 05:17:34 | <maerwald[m]> | So if you mess up, you get optimization dependent bugs |
| 05:18:02 | <remexre> | ig I should amend, "I believe so, but in the same way Rust lifetime analysis is separate from typechecking" |
| 05:18:12 | <glguy> | int-e: It's fun seeing the very similar structure in an almost completely different presentation :) |
| 05:18:24 | <glguy> | you're really enjoying pattern synonyms! |
| 05:18:25 | <catern> | remexre: impure, of course |
| 05:18:30 | <glguy> | guard patterns* |
| 05:18:33 | <int-e> | I really am |
| 05:18:45 | × | alx741 quits (~alx741@181.199.42.79) (Read error: Connection reset by peer) |
| 05:19:02 | <int-e> | a large part of the joy is that they're not recursive |
| 05:19:06 | <remexre> | catern: are datatype constructors pure functions? |
| 05:19:20 | <glguy> | int-e: yeah, I guess for non-recursive bindings they replace let |
| 05:19:29 | <glguy> | remexre: only the ones that are functions |
| 05:19:46 | → | theproffesor_ joins (~theproffe@2601:282:847f:8010::5fff) |
| 05:19:53 | <glguy> | True and False aren't functions and are datatype constructors |
| 05:19:55 | × | the_proffesor quits (~theproffe@user/theproffesor) (Remote host closed the connection) |
| 05:19:58 | <remexre> | ah, fair |
| 05:20:02 | <remexre> | I'll amend that too |
| 05:20:42 | <int-e> | glguy: but they don't work nicely with `where` so there is a downside when code becomes more complex |
| 05:21:13 | <remexre> | catern: if you agree that the Reader constructor is a pure function and the expression (\x -> x) is pure, `Reader (\x -> x)' has to be pure as well |
| 05:21:21 | <glguy> | int-e: I haven't decided if it's *better* but it is faster and I like the change. I updated day 18; exploding snailfish arithmetic; such that it does all the explodes in one "pass" walking up and down the tree, tracking where it is with zippers https://glguy.net/advent/sln_2021_18/src/Main.html#explode |
| 05:22:44 | → | lavaman joins (~lavaman@98.38.249.169) |
| 05:23:07 | × | sirlensalot quits (~sirlensal@ool-44c5f8c9.dyn.optonline.net) (Quit: sirlensalot) |
| 05:25:16 | <glguy> | now I'm wondering if the (Maybe Int, Tree, Maybe Int) version works just as well for the single pass; need to give that a stab next |
| 05:25:17 | <catern> | remexre: I don't think so; I can transform any impure program into a collection of pure components, but that doesn't make it pure |
| 05:25:59 | <remexre> | catern: the description of an impure program may be pure |
| 05:26:38 | <catern> | I disagree that there's a meaningful distinction between an impure program and its description |
| 05:27:02 | <remexre> | would you say that `"putStrLn \"hello\""' is a description of an impure program |
| 05:27:11 | <catern> | sure |
| 05:27:23 | <maerwald[m]> | putStrLn is a pure function |
| 05:27:27 | <remexre> | like, that being a string literal |
| 05:27:33 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 268 seconds) |
| 05:27:50 | <int-e> | glguy: it's a zipper! |
| 05:27:58 | <remexre> | maerwald[m]: pretend I wrote `"System.out.println(\"hello\")"' if you want :P |
| 05:28:07 | <maerwald[m]> | remexre: ? |
| 05:28:09 | → | nuh^ joins (~nuh@207.5.54.6) |
| 05:28:10 | <glguy> | pure/impure describe /functions/ |
| 05:28:22 | <remexre> | a string literal containing the source of a program describes the program |
| 05:28:40 | <remexre> | but I don't think there's a reasonable definition of impure that counts a string literal as impure |
| 05:29:01 | <glguy> | string literals aren't functions, so they can't be pure or impure |
| 05:29:12 | <remexre> | an expression could be impure, no? |
| 05:29:37 | <maerwald[m]> | https://www.semanticscholar.org/paper/What-is-a-Purely-Functional-Language-Sabry/63c46be541fa2f18022d00c3cf15eb5342b00b01 |
| 05:29:43 | <maerwald[m]> | Check that out |
| 05:30:14 | <maerwald[m]> | This discussion is semantically too vague |
| 05:31:10 | <otherwise> | is machine code pure or impure? |
| 05:31:20 | <remexre> | pdf link there gives me a cloudflare error 1020 >_> |
| 05:31:22 | <otherwise> | disregard, I don't even know what that question means |
| 05:31:23 | <catern> | remexre: oh - well, if you partner that with the type that the program evaluates to, yes, I'd say that's a description of an impure program |
| 05:31:34 | <remexre> | catern: why does the type matter? |
| 05:31:55 | <catern> | remexre: and to evalute that impure program to get its result, is an impure operation |
| 05:32:18 | <catern> | hence: it's an impure expression that gives you () |
| 05:32:20 | <remexre> | right, but the expression containing the _description itself_ is pure |
| 05:32:47 | <catern> | I mean, I agree with glguy, it's better to talk about pure/impure in terms of functions |
| 05:33:13 | <catern> | anyway, I don't think it's constructive to discuss whether Haskell distinguishes pure and impure functions |
| 05:33:41 | <maerwald[m]> | Try this link then https://www.cambridge.org/core/journals/journal-of-functional-programming/article/what-is-a-purely-functional-language/3A39D50DA48F628D17D9A768A1FA39C3 |
| 05:33:55 | <maerwald[m]> | catern: it doesn't distinguish them |
| 05:34:59 | <remexre> | I think you need some notion of an expression having an effect to talk about languages in general; in my mind, "an impure function" is shorthand for "a function f such that for some x, (f x) is an impure expression" |
| 05:36:15 | → | alx741 joins (~alx741@157.100.93.160) |
| 05:38:54 | <remexre> | maerwald[m]: I'm unconvinced por is a pure operator :P |
| 05:39:18 | <catern> | ultimately, I think any argument you could use to argue that Haskell doesn't have some kind of distinction between pure and impure, would also apply to any language with an effect system |
| 05:40:05 | <catern> | in languages with an effect system you can also pass around things which you can impurely evaluate to get some value |
| 05:40:25 | <otherwise> | catern, do you have a line of code in mind that would illuminate your case? |
| 05:41:09 | <maerwald[m]> | Purity is about equivalence of evaluation strategies, not about types or execution of a program. If changing the evaluation strategy doesn't change the semantics of your program, it's "pure". That's an oversimplification, but yeah |
| 05:42:20 | <catern> | then all languages with effect systems are pure, because effect handling is not part of the evaluation strategy |
| 05:42:31 | <catern> | er, rather, isn't changed if you change the evaluation, |
| 05:42:32 | <maerwald[m]> | Even effects systems are mostly orthogonal |
| 05:42:33 | <catern> | strategy |
| 05:43:40 | <maerwald[m]> | You don't need an effects system for your language to be pure. And the existence of one doesn't magically make your language pure |
| 05:44:40 | <catern> | okay so do you know of any language which has a (statically checked) distinction between pure and impure in any way? |
| 05:45:01 | <catern> | i'd say that "languages with an effect system" are a clear example of such a language |
| 05:45:06 | <catern> | (as is Haskell) |
| 05:45:41 | <maerwald[m]> | I'm giving up. I think you still have a misconception of purity. |
| 05:46:21 | <remexre> | catern: okay, I'll go with a modification of the above; does the `Monad ((->) r)' instance imply that `(\x -> x)' is an impure function |
| 05:46:30 | <remexre> | the existence of that instance* |
| 05:47:39 | <catern> | remexre: no, I suppose not |
| 05:48:52 | <remexre> | then since Reader is just a newtype around that, `Reader (\x -> x)' ought to also be pure |
| 05:49:57 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 05:49:57 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 05:50:56 | × | slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 05:51:57 | → | antony joins (~The_viole@203.77.49.232) |
| 05:55:33 | <maerwald[m]> | An example of a language that can distinguish between purity and impurity would e.g. be a language that allows global mutable variables, but has knowledge about where these are used in the entire callstack and then choose different evaluation strategies based on that knowledge. I don't even think that's a good thing, because it would make reasoning very hard. |
| 05:57:51 | × | vglfr quits (~vglfr@88.155.24.19) (Ping timeout: 256 seconds) |
| 06:04:26 | <catern> | remexre: sorry, what exactly is `Reader (\x -> x)'? is that just ask? |
| 06:04:31 | <remexre> | yeah |
| 06:05:02 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 06:07:04 | <catern> | okay, I grant that "pure" and "impure" are fuzzy concepts... it's hard to claim "something which is parameterized over some functions and a type" is always impure... it's possible that it's a detail of *what* concrete instance it's applied to, but then that would rather weaken my argument... |
| 06:07:53 | <catern> | I mean, I suppose a pure implementation for State is to just throw away the puts and return a constant for the gets |
| 06:07:53 | → | alx741 joins (~alx741@157.100.93.160) |
| 06:08:32 | <maerwald[m]> | purely functional isn't a fuzzy concept, but it's often used in a fuzzy way |
| 06:08:38 | <remexre> | I'd argue rather strongly that the existing implementation is pure too... |
| 06:10:17 | <catern> | remexre: that's true too |
| 06:11:30 | <catern> | but so is the implementation of Cont, and in some sense, so is the implementation of IO, if you run your program in a VM without access to external state/randomness |
| 06:11:49 | <c_wraith> | "pure" is a weird term to apply to types other than (->) |
| 06:12:05 | <c_wraith> | purity is a property of functions |
| 06:12:55 | <remexre> | c_wraith: if my language had a primitive expression (printHelloWorldAndYield42 : Nat), it would make sense to call that expression impure, no? |
| 06:13:50 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 06:13:50 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 06:13:50 | → | wroathe joins (~wroathe@user/wroathe) |
| 06:14:20 | <maerwald[m]> | c_wraith: anything that can be evaluated can be pure or impure |
| 06:14:20 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 06:14:52 | × | antony quits (~The_viole@203.77.49.232) (Quit: Leaving) |
| 06:16:00 | <remexre> | catern: if you were to implement the Haskell RTS in a pure language, I'd agree with that |
| 06:16:04 | <catern> | okay, so then what even is an effect? is callCC an effect? are put/get effects? how is an effect distinguished from just any random function that is an input to another function? |
| 06:17:52 | <c_wraith> | maerwald[m]: and in Haskell, only functions have non-trivial evaluation. Anything else is just a data constructor. |
| 06:17:59 | <remexre> | I feel like I've seen a proper definition somewhere, but my loose definition is, "something you can't implement via a definitional interpreter in the untyped lambda calculus" |
| 06:17:59 | <catern> | remexre: I don't that's necessary :) C is monadic, everything is monadic as oleg says https://okmij.org/ftp/Computation/monadic-shell.html#All%20i/o%20is%20monadic :) |
| 06:18:46 | <catern> | remexre: well, so are functions which use effects "impure"? |
| 06:19:36 | <remexre> | catern: remembering that e.g. `Reader (\x -> x)' is a pure description of an effect, not an impure expression itself; yes |
| 06:19:38 | <c_wraith> | catern: depends on if the effect is the result of calling the function or not. In haskell, only a very small number of functions like unsafePerformIO, unsafeInterleaveIO, unsafeInterleaveST, etc, are doing things that are impure |
| 06:19:57 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 06:20:22 | → | jco joins (~jco@90-228-194-139-no542.tbcn.telia.com) |
| 06:21:33 | <c_wraith> | in *most* cases, what's being done is a pure calculation that results in some sort of description of an effect. This is distinguishable from actually running the effect. |
| 06:22:32 | <maerwald[m]> | I tried to explain that an hour ago :) |
| 06:23:07 | <catern> | okay, sure, but I have to go back to: does a language with an effect system distinguish pure and impure functions? an effect system also lets me compose together impure functions to produce another impure function without actually "running the effect" |
| 06:23:15 | <c_wraith> | man, unsafeInterleaveST hits that awkward combination of really broken when misused and really helpful when used properly. |
| 06:24:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 06:24:07 | <remexre> | catern: I mean, I'd say `traceShowId . traceShowId' is a pure expression that yields an impure function |
| 06:24:45 | <remexre> | traceShowId being an impure function in Haskell |
| 06:25:09 | <catern> | Haskell lets me create descriptions of a big chain of effects, but so do many languages - heck, even C! "printf" is a description of a bunch of effects, if I write a function "print_hello" which calls printf, then print_hello is also just a description of some effects, it's not actually run until I type ./a.out in my terminal... |
| 06:25:45 | <c_wraith> | catern: a language like haskell *doesn't* distinguish between pure and impure functions. That's why impure functions are so dangerous. |
| 06:25:48 | <catern> | but I still think there is some difference between Haskell and C here, even though they both let me make functions which describe a bunch of effects! |
| 06:25:54 | <catern> | make values* |
| 06:26:40 | → | seer joins (~delicacie@2601:6c4:4080:3f80:452b:5b2:a00e:7e62) |
| 06:26:44 | <seer> | @[exa] |
| 06:26:44 | <lambdabot> | Unknown command, try @list |
| 06:26:47 | <maerwald[m]> | c_wraith: I also explained that an hour ago ^^ |
| 06:26:48 | <catern> | (although see the oleg link I just linked) |
| 06:26:53 | <seer> | can you help me out? |
| 06:26:56 | seer | is now known as Inst |
| 06:27:07 | <Inst> | I need to find a professor willing to supervise a course / seminar course I want to teach |
| 06:27:21 | <Inst> | what I'm trying to do is to bribe people with MMO gold equivalent of $4 |
| 06:27:35 | <Inst> | for non-programmers etc to learn Haskell |
| 06:27:40 | <remexre> | catern: I think that Oleg post isn't quite unconfusing enough |
| 06:27:46 | <Inst> | targeted courseload is 72-144 hours |
| 06:27:56 | <remexre> | I think it is valid to say (and possibly valid to interpret that post as saying), |
| 06:27:59 | <Inst> | since this is an online course |
| 06:28:03 | <Inst> | taught on Twitch.tv |
| 06:28:26 | ← | Omen parts (~Omen@2600:1702:2e30:1a40:8511:a2a3:f354:5a5e) (Leaving) |
| 06:28:41 | <remexre> | you can treat a string of bytes as a pure description of an impure program, and the string of bytes remains pure |
| 06:28:55 | <Inst> | instead of having grading, altohugh we'll have proper problem sets (which are divided into review of current lesson, spaced repetition review of previous lessons, extension of current lesson, and preview of future concepts) |
| 06:29:11 | <Inst> | we'll give a prize for best haskell program |
| 06:29:18 | <Inst> | would be $80 in MMO gold |
| 06:29:26 | <Inst> | $40 for second prize, $20 for third prize |
| 06:29:35 | <Inst> | ideal is that their stuff can be contributed to Hackage |
| 06:29:55 | <remexre> | and a reasonable followup might be, you could argue that an interpreter for the strings of bytes might not have to be impure, even if the language the string-of-bytes is describing is e.g. machine code |
| 06:30:01 | <Inst> | long-term, I want to extend that to steam and steam gift cards, with a $20 entry prize, and a $500 first prize, $250 second prize, and $125 third prize |
| 06:30:59 | <Inst> | interests: #1, scamming people into providing a good Windows API UI framework for Haskell |
| 06:31:14 | <Inst> | #2, producing a genericized Haskell course that professors can adapt to their needs |
| 06:31:37 | <remexre> | this argument could be made more concrete by thinking of the amd64 syscall instruction as your single effect added to http://wall.org/~lewis/2013/10/15/asm-monad.html |
| 06:31:45 | <Inst> | i ideally would like to produce "Accelerated Intro Computer Science in Haskell and C" |
| 06:31:48 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 06:31:50 | → | ensyde joins (~Omen@2600:1702:2e30:1a40:8511:a2a3:f354:5a5e) |
| 06:31:54 | <Inst> | which gives you data structures and algorithms baked in |
| 06:31:55 | <remexre> | and imagining an implementation of that effect that e.g. sets rax to -EAGAIN |
| 06:32:27 | → | alx741 joins (~alx741@157.100.93.160) |
| 06:32:58 | → | vglfr joins (~vglfr@88.155.6.191) |
| 06:33:02 | <Inst> | /s/in/with |
| 06:33:16 | <remexre> | (okay, I think more nuance is needed abt interrupts, but we could pretend for the sake of argument that we're interpreting in Maybe and synchronous interrupts result in our interpreter yielding Nothing) |
| 06:33:37 | <remexre> | er wait, that's not the right post |
| 06:34:16 | <c_wraith> | yeah, watch out for Oleg's site - everything is anchors into one giant page |
| 06:34:18 | <catern> | remexre: I dunno, so I think pure and impure is fuzzy, but I still think there's something inherently impure about, e.g., the IO monad even with a really simple implementation like always EAGAIN |
| 06:35:02 | <catern> | remexre: and I'm willing to bite the bullet on reader if that's necessary :) |
| 06:35:19 | <c_wraith> | catern: if you were to accept "Haskell doesn't treat pure and impure functions differently" as simple truth, would it require you to stop and rethink your starting point? |
| 06:36:42 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 06:36:42 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 06:36:42 | → | wroathe joins (~wroathe@user/wroathe) |
| 06:37:45 | <maerwald[m]> | xD |
| 06:39:27 | → | analognoise joins (~analognoi@185.216.74.46) |
| 06:41:29 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 06:48:15 | <catern> | okay, wait, what if there was a language where every function ended with return? every function is something like Foo -> IO Bar |
| 06:49:01 | <catern> | is there some concise way you would describe the difference between this language and Haskell? |
| 06:49:39 | <remexre> | does "everything" include (>>=)? or is bind a builtin to the language too? |
| 06:49:39 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 06:49:52 | <remexre> | and is it IO's return, or just "some" return |
| 06:50:28 | <maerwald[m]> | I have the feeling these type of questions don't lead anywhere |
| 06:52:56 | <catern> | remexre: yeah that was a poor description, let me just leave it at "every function has to return an IO T" and the programmer has to implement that appropriately |
| 06:53:51 | <remexre> | "the programmer has to implement that appropriately" -- in a separate metalanguage? |
| 06:54:20 | <catern> | remexre: no, by inserting appropriate calls to return and bind as appropriate |
| 06:55:21 | <remexre> | catern: can you give an example? |
| 06:55:39 | × | vglfr quits (~vglfr@88.155.6.191) (Ping timeout: 256 seconds) |
| 06:56:46 | → | asco2 joins (~asco2@c-73-202-117-7.hsd1.ca.comcast.net) |
| 06:57:26 | <catern> | add x y : Int -> Int -> IO Int = return (x + y) |
| 06:57:45 | <remexre> | er, an example of the implementation |
| 06:57:55 | <catern> | not sure what you mean |
| 06:58:02 | <catern> | implementation of what? |
| 06:58:11 | → | spaceseller joins (~spacesell@31.147.205.13) |
| 06:58:23 | <catern> | that was an example of the code a programmer would have to write |
| 06:58:29 | × | InternetCitizen quits (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) (Ping timeout: 256 seconds) |
| 06:58:40 | <catern> | the implementation... of the typechecker which requires every return type to be an IO t? |
| 06:58:41 | <remexre> | oh, in "the programmer has to implement that appropriately," was that =/= IO ? |
| 06:58:55 | <remexre> | well, currying gets in your way in your example :P |
| 06:59:07 | <catern> | ah |
| 07:00:00 | <remexre> | though, does that mean one can't write the identity function in that language? |
| 07:00:29 | <catern> | correct |
| 07:01:03 | <remexre> | can I take apart IO in the same way I can in Haskell? |
| 07:01:24 | <catern> | in what way do you mean? |
| 07:01:44 | <remexre> | like, IO in GHC is just a datatype |
| 07:03:13 | <remexre> | https://hackage.haskell.org/package/base-4.16.0.0/docs/GHC-IO.html#t:IO |
| 07:03:51 | <catern> | sure, you can take IO apart as much as you can in Haskell code that doesn't have access to the IO constructor |
| 07:04:17 | <remexre> | does unsafePerformIO exist, then? |
| 07:04:48 | <catern> | sure, I don't think unsafePerformIO harms the analgoy |
| 07:05:12 | <remexre> | okay, then I'd say that language allows impure expressions |
| 07:07:57 | → | alx741 joins (~alx741@157.100.93.160) |
| 07:08:01 | → | vglfr joins (~vglfr@88.155.6.191) |
| 07:08:28 | <catern> | er, so is that the distinction between that language and Haskell? IOLang allows impure expressions and Haskell doesn't? or if not, what's the difference between IOLang and Haskell? |
| 07:09:02 | <remexre> | haskell allows impure programming all day long, you just find yourself wrapping a ton of stuff in unsafePerformIO and having a terrible awful time because of laziness |
| 07:12:13 | × | vglfr quits (~vglfr@88.155.6.191) (Ping timeout: 240 seconds) |
| 07:12:31 | → | vglfr joins (~vglfr@88.155.6.191) |
| 07:12:48 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 07:13:08 | → | falafel joins (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
| 07:13:43 | → | yauhsien joins (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
| 07:15:14 | <maerwald[m]> | catern: we answered your question multiple times in the last 2 hours: 1. Haskell doesn't distinguish between pure and impure (everything is considered pure) and 2. you can write impure expressions, but the compiler won't know and you can pick up the pieces (that's why you need NOINLINE on global IORefs) |
| 07:16:17 | <int-e> | . o O ( making sure there's onle a single piece to pick up ) |
| 07:17:07 | <catern> | maerwald[m]: what's that a response to? I asked a specific question, what's the difference between IOLang which I just described, and Haskell? |
| 07:17:11 | × | vglfr quits (~vglfr@88.155.6.191) (Ping timeout: 256 seconds) |
| 07:17:48 | → | vglfr joins (~vglfr@88.155.6.191) |
| 07:17:55 | <maerwald[m]> | catern: "IOLang allows impure expressions and Haskell doesn't" |
| 07:18:13 | × | yauhsien quits (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
| 07:18:28 | <maerwald[m]> | Please read the paper by Amr Sabry I linked twice |
| 07:19:17 | × | SummerSonw quits (~The_viole@203.77.49.232) (Ping timeout: 240 seconds) |
| 07:20:18 | <remexre> | I kinda wanna write an ACME.Impure module now, that's a copy of System.IO but with unsafePerformIO composed onto everything |
| 07:24:56 | <int-e> | remexre: try https://hackage.haskell.org/package/bytestring-0.11.2.0/docs/Data-ByteString-Internal.html#v:accursedUnutterablePerformIO for extra foot-shooting power |
| 07:25:27 | × | burnsidesLlama quits (~burnsides@dhcp168-010.wadham.ox.ac.uk) (Remote host closed the connection) |
| 07:25:38 | <int-e> | (can you believe that this was called `inlinePerformIO` at some point... such an innocent name) |
| 07:25:52 | × | asco2 quits (~asco2@c-73-202-117-7.hsd1.ca.comcast.net) (Quit: Client closed) |
| 07:25:59 | → | burnsidesLlama joins (~burnsides@client-8-79.eduroam.oxuni.org.uk) |
| 07:26:35 | <catern> | remexre: just to be clear, what part if any was an answer to "what's the difference between IOLang which I just described, and Haskell?"? not that you're required to answer my questions, but if you did I didn't understand |
| 07:27:02 | <remexre> | there isn't a technical difference |
| 07:27:08 | <remexre> | the difference is a matter of convenience |
| 07:27:28 | <int-e> | no, it's so much worse than that |
| 07:27:54 | <int-e> | `IO a` imposes an order on effects |
| 07:28:19 | <remexre> | hm? unsafePerformIO removes it; I think IOLang is "macro-equivalent" to Haskell |
| 07:28:51 | <int-e> | (and from the glance I had, there's nothing in "IOLang" that relaxes that order) |
| 07:29:57 | × | burnsidesLlama quits (~burnsides@client-8-79.eduroam.oxuni.org.uk) (Ping timeout: 240 seconds) |
| 07:30:07 | <remexre> | int-e: unsafePerformIO relaxes it, dunnit? |
| 07:30:29 | → | alx741 joins (~alx741@157.100.93.160) |
| 07:30:32 | <int-e> | remexre: of course, horribly so |
| 07:30:48 | <remexre> | so that's the thing in IOLang that relaxes the order |
| 07:35:16 | <EvanR> | at some point the jargon for pure/impure functions escaped from functions and random stuff in haskell can be called pure and impure, pure expressions, pure values, pure data... |
| 07:36:26 | <EvanR> | I'm always suspicious about whether it makes sense xD |
| 07:37:08 | <int-e> | sometimes it makes sense through pure luck |
| 07:37:24 | <int-e> | (that's a real world phenomenon) |
| 07:37:39 | <EvanR> | oooooh |
| 07:38:33 | <remexre> | imo: pure expressions are the primitive concept (scroll up ~2hrs); a pure value is a WHNF value with pure subterms or a thunk of a pure expression; and pure data isn't pure/impure, it refers (afaik) to whether something is (forceable to) a tree of constructors or not |
| 07:38:33 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 07:40:07 | <EvanR> | even if some of that made sense I'm not sure how good it is, jargonwise |
| 07:40:39 | <EvanR> | why have a word for a WHNF value, that conflicts with established usage, when we already have that |
| 07:40:58 | <remexre> | uh the "or a thunk" part is relevant to that |
| 07:41:24 | <EvanR> | anyway |
| 07:51:13 | → | Jing joins (~hedgehog@2604:a840:3::1067) |
| 07:57:06 | → | alx741 joins (~alx741@157.100.93.160) |
| 07:57:16 | × | x88x88x quits (~x88x88x@2001:19f0:5:39a8:5400:3ff:feb6:73cb) (Remote host closed the connection) |
| 07:58:01 | → | x88x88x joins (~x88x88x@149.28.53.172) |
| 07:58:10 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 08:00:30 | → | nschoe joins (~quassel@178.251.84.79) |
| 08:01:47 | × | nschoe quits (~quassel@178.251.84.79) (Client Quit) |
| 08:02:53 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 08:04:17 | × | falafel quits (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Ping timeout: 240 seconds) |
| 08:04:19 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 08:10:48 | → | lavaman joins (~lavaman@98.38.249.169) |
| 08:11:00 | × | shriekingnoise quits (~shrieking@186.137.144.80) (Quit: Quit) |
| 08:15:19 | → | coolnickname joins (uid531864@user/coolnickname) |
| 08:16:13 | <otherwise> | > let test key xs = foldl (\acc (x,y)-> if key == x then Just y else acc) Nothing xs in test "foo" [("foo", "1234"), ("flub","4321"), ("bar","987"),("blurp","344")] |
| 08:16:14 | <lambdabot> | Just "1234" |
| 08:16:17 | <otherwise> | > let test key xs = foldl (\(x,y) acc-> if key == x then Just y else acc) xs Nothing in test "foo" [("foo", "1234"), ("flub","4321"), ("bar","987"),("blurp","344")] |
| 08:16:18 | <lambdabot> | error: |
| 08:16:18 | <lambdabot> | • Couldn't match expected type ‘(a1, a2)’ |
| 08:16:18 | <lambdabot> | with actual type ‘Maybe a2’ |
| 08:16:53 | <otherwise> | why does the second case fail? I switch (x,y) , acc, xs and Nothing, respectively |
| 08:17:40 | × | xff0x quits (~xff0x@2001:1a81:527e:7f00:c95b:8db9:d638:e5ae) (Remote host closed the connection) |
| 08:17:59 | → | xff0x joins (~xff0x@2001:1a81:527e:7f00:b856:ac3b:a520:4a41) |
| 08:20:34 | → | alx741 joins (~alx741@181.199.42.79) |
| 08:20:36 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 08:21:14 | → | max22- joins (~maxime@lfbn-ren-1-1026-62.w92-139.abo.wanadoo.fr) |
| 08:21:56 | × | foul_owl quits (~kerry@212.102.47.57) (Ping timeout: 252 seconds) |
| 08:22:14 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 08:22:24 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 08:22:27 | allbery_b | is now known as geekosaur |
| 08:26:11 | × | alx741 quits (~alx741@181.199.42.79) (Read error: Connection reset by peer) |
| 08:27:26 | → | foul_owl joins (~kerry@212.102.47.57) |
| 08:28:38 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:30:16 | × | alfonsox quits (~quassel@103.92.42.182) (Remote host closed the connection) |
| 08:30:40 | → | KvL joins (~KvL@user/KvL) |
| 08:39:39 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 08:39:41 | <otherwise> | okay I think i figured it out. it's in the type signature |
| 08:39:52 | → | ksqsf joins (~user@134.209.106.31) |
| 08:40:02 | × | analognoise quits (~analognoi@185.216.74.46) (Read error: Connection reset by peer) |
| 08:40:28 | <otherwise> | :t foldr |
| 08:40:29 | <lambdabot> | Foldable t => (a -> b -> b) -> b -> t a -> b |
| 08:42:51 | → | alx741 joins (~alx741@157.100.93.160) |
| 08:43:00 | <otherwise> | the a in (a -> b -> b) corresponds to the 't a', which is the last input to the foldr function, which needs to be a foldable (like a list) |
| 08:43:36 | <otherwise> | I'm just explaining things to myself here, dont mind me. |
| 08:48:46 | × | nuh^ quits (~nuh@207.5.54.6) (Remote host closed the connection) |
| 08:50:04 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 08:55:59 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 08:55:59 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 08:55:59 | → | wroathe joins (~wroathe@user/wroathe) |
| 08:56:51 | → | nhatanh02 joins (~satori@123.24.172.30) |
| 09:00:53 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 09:04:18 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:08:21 | → | alx741 joins (~alx741@157.100.93.160) |
| 09:08:22 | → | acidjnk joins (~acidjnk@p200300d0c7271e9910698cbf36694c68.dip0.t-ipconnect.de) |
| 09:11:39 | × | nhatanh02 quits (~satori@123.24.172.30) (Ping timeout: 256 seconds) |
| 09:13:20 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 09:17:42 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 09:17:42 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 09:17:45 | allbery_b | is now known as geekosaur |
| 09:18:57 | → | Gurkenglas joins (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) |
| 09:19:01 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 09:22:42 | <Nate[m]12> | does anyone know some good examples of accounting softwares with haskell? |
| 09:22:50 | → | nhatanh02 joins (~satori@123.24.172.30) |
| 09:22:59 | <Nate[m]12> | s/softwares/software/ |
| 09:24:07 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:26:26 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 09:30:16 | <tomsmeding> | Nate[m]12: not sure if it's precisely what you're looking for, but hledger exists |
| 09:30:39 | → | alx741 joins (~alx741@157.100.93.160) |
| 09:30:41 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 09:34:40 | <Nate[m]12> | tomsmeding: thanks, it looks like a personal accounting software, but I was looking for software that is distributed over multiple companies for verification purposes etc. |
| 09:34:56 | AlexNoo__ | is now known as AlexNoo |
| 09:35:00 | <Nate[m]12> | does cardano offer such services? |
| 09:35:05 | <tomsmeding> | I would find it unlikely that exists, to be honest :p |
| 09:37:43 | × | nhatanh02 quits (~satori@123.24.172.30) (Ping timeout: 256 seconds) |
| 09:40:08 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 09:40:31 | → | cosimone joins (~user@93-34-133-35.ip49.fastwebnet.it) |
| 09:43:57 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:44:43 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 09:45:09 | → | jgeerds joins (~jgeerds@55d4ac73.access.ecotel.net) |
| 09:45:54 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 09:47:17 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 09:48:08 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 09:50:17 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 240 seconds) |
| 09:51:26 | × | jco quits (~jco@90-228-194-139-no542.tbcn.telia.com) (Remote host closed the connection) |
| 09:51:37 | × | Inst quits (~delicacie@2601:6c4:4080:3f80:452b:5b2:a00e:7e62) (Ping timeout: 240 seconds) |
| 09:53:35 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 256 seconds) |
| 09:54:46 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 09:59:41 | × | max22- quits (~maxime@lfbn-ren-1-1026-62.w92-139.abo.wanadoo.fr) (Ping timeout: 250 seconds) |
| 10:04:03 | → | jinsun joins (~quassel@user/jinsun) |
| 10:04:47 | → | alx741 joins (~alx741@181.199.42.79) |
| 10:06:11 | → | chomwitt joins (~chomwitt@2a02:587:dc1e:c100:12c3:7bff:fe6d:d374) |
| 10:09:57 | × | vglfr quits (~vglfr@88.155.6.191) (Ping timeout: 240 seconds) |
| 10:12:39 | → | mvk joins (~mvk@2607:fea8:5cdd:f000::917a) |
| 10:16:57 | × | ensyde quits (~Omen@2600:1702:2e30:1a40:8511:a2a3:f354:5a5e) (Ping timeout: 240 seconds) |
| 10:20:28 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 10:21:28 | → | Tuplanolla joins (~Tuplanoll@91-159-69-90.elisa-laajakaista.fi) |
| 10:22:19 | × | alx741 quits (~alx741@181.199.42.79) (Read error: Connection reset by peer) |
| 10:25:43 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 10:27:25 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
| 10:27:55 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 10:30:38 | × | Gurkenglas quits (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Ping timeout: 252 seconds) |
| 10:35:15 | → | mastarija joins (~mastarija@2a05:4f46:e0e:5000:d11e:1641:cfb6:79c3) |
| 10:39:09 | → | alx741 joins (~alx741@157.100.93.160) |
| 10:42:17 | × | spaceseller quits (~spacesell@31.147.205.13) (Quit: Leaving) |
| 10:46:24 | × | ksqsf quits (~user@134.209.106.31) (Remote host closed the connection) |
| 10:46:57 | × | xff0x quits (~xff0x@2001:1a81:527e:7f00:b856:ac3b:a520:4a41) (Ping timeout: 240 seconds) |
| 10:48:11 | → | xff0x joins (~xff0x@2001:1a81:527e:7f00:c538:8d07:2658:ecf) |
| 10:48:53 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 10:49:50 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 10:53:19 | → | vglfr joins (~vglfr@88.155.12.39) |
| 10:53:30 | → | max22- joins (~maxime@2a01cb088335980042a847f93091dac4.ipv6.abo.wanadoo.fr) |
| 10:53:48 | → | DNH joins (~DNH@ip5f5abb04.dynamic.kabel-deutschland.de) |
| 10:54:44 | × | mastarija quits (~mastarija@2a05:4f46:e0e:5000:d11e:1641:cfb6:79c3) (Quit: Leaving) |
| 10:56:46 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 10:56:46 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 10:56:46 | → | wroathe joins (~wroathe@user/wroathe) |
| 10:59:39 | × | vglfr quits (~vglfr@88.155.12.39) (Read error: Connection reset by peer) |
| 11:00:17 | → | vglfr joins (~vglfr@88.155.12.39) |
| 11:01:47 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
| 11:03:41 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 11:07:35 | → | alx741 joins (~alx741@157.100.93.160) |
| 11:12:17 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 11:16:43 | × | DNH quits (~DNH@ip5f5abb04.dynamic.kabel-deutschland.de) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 11:21:24 | → | __monty__ joins (~toonn@user/toonn) |
| 11:24:14 | <otherwise> | i'm trying to compare runtime differences between two definitions of factorial, but it appears I need to force strict evaluation (not lazy) to maximize efficiency for one of the definitions. Only problem is, the syntax for applying BangPatterns is not working for me... |
| 11:25:08 | <int-e> | @where paste |
| 11:25:08 | <lambdabot> | Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com |
| 11:27:33 | <otherwise> | https://paste.tomsmeding.com/EWFX3Ar1 |
| 11:28:09 | <otherwise> | thanks, I put the cart in front of the horse, I didnt have a paste prepped |
| 11:28:45 | → | alx741 joins (~alx741@157.100.93.160) |
| 11:31:28 | <int-e> | otherwise: the last attempt looks correct; did you actually enable the extension? You need {-# LANGUAGE BangPatterns #-} or invoke ghc[i] with -XBangPatterns |
| 11:32:23 | <int-e> | ghc actually tried to be helpful and say "Did you forget to enable BangPatterns?" |
| 11:32:49 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 11:33:11 | <otherwise> | oh |
| 11:33:16 | <otherwise> | no I didnt do that |
| 11:33:32 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 11:33:38 | <otherwise> | I've never invoked anything, so I'm not how I would, honestly |
| 11:34:02 | × | acidjnk quits (~acidjnk@p200300d0c7271e9910698cbf36694c68.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 11:34:13 | <otherwise> | import Data.-XBangPatterns or something like that? |
| 11:34:23 | <int-e> | ? |
| 11:34:33 | <albet70> | why the fish operator >=> called Kleisli composition? |
| 11:34:50 | <albet70> | any special used? |
| 11:34:55 | <int-e> | otherwise: No, the LANGUAGE pragma is what you'd use in a source file. |
| 11:35:24 | <int-e> | otherwise: -XBangPatterns is a command line option for ghc or ghci; in ghci, you can also use :set -XBangPatterns |
| 11:35:32 | int-e | would recommend the pragma actually |
| 11:36:42 | <int-e> | LANGUAGE pragmas got at the very beginning of a module's source code, btw, even before the `module` keyword (if you have that) |
| 11:38:05 | <otherwise> | oh okay, nested in the {# #} ? |
| 11:39:50 | → | madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 11:40:07 | × | deadmarshal quits (~deadmarsh@95.38.115.121) (Ping timeout: 256 seconds) |
| 11:42:26 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 11:42:29 | <otherwise> | definitely not in the {# #}, okay I think I'm slowly weeding out the errors, thanks! :) |
| 11:42:32 | × | KvL quits (~KvL@user/KvL) (Quit: KvL) |
| 11:43:54 | → | KvL joins (~KvL@user/KvL) |
| 11:44:57 | <fendor[m]> | otherwise, you put it in {-# #-}, e.g. `{-# LANGUAGE BangPatterns #-}` |
| 11:45:10 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:46:18 | → | DNH joins (~DNH@2a02:8108:1100:16d8:7457:6675:c5ec:bb4b) |
| 11:46:55 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 11:47:25 | × | foul_owl quits (~kerry@212.102.47.57) (Ping timeout: 240 seconds) |
| 11:49:17 | <otherwise> | https://paste.tomsmeding.com/EfSiXa4b |
| 11:49:55 | → | alx741 joins (~alx741@157.100.93.160) |
| 11:50:19 | × | KvL quits (~KvL@user/KvL) (Ping timeout: 256 seconds) |
| 11:51:49 | <fendor[m]> | well, you have a typo |
| 11:52:17 | <fendor[m]> | `-#}` vs `#-}` |
| 11:52:36 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 11:53:47 | <otherwise> | Thats why the code was golden! |
| 11:53:51 | <otherwise> | haha |
| 11:54:01 | → | Rum joins (~bourbon@user/rum) |
| 11:54:10 | → | coot joins (~coot@89-64-85-93.dynamic.chello.pl) |
| 11:54:27 | × | synthmeat quits (~synthmeat@user/synthmeat) (Quit: WeeChat 3.0) |
| 11:55:12 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 11:55:13 | → | synthmeat joins (~synthmeat@user/synthmeat) |
| 11:56:50 | → | antony joins (~The_viole@203.77.49.232) |
| 11:57:37 | → | KvL joins (~KvL@user/KvL) |
| 11:57:46 | <otherwise> | thanks Int-e and fendor |
| 12:00:18 | → | ProfSimm joins (~ProfSimm@87.227.196.109) |
| 12:01:24 | → | foul_owl joins (~kerry@94.140.8.106) |
| 12:13:01 | × | antony quits (~The_viole@203.77.49.232) (Quit: Leaving) |
| 12:13:21 | → | antony joins (~The_viole@203.77.49.232) |
| 12:13:22 | → | alx741 joins (~alx741@157.100.93.160) |
| 12:13:23 | × | antony quits (~The_viole@203.77.49.232) (Remote host closed the connection) |
| 12:13:29 | × | SummerSonw quits (~The_viole@203.77.49.232) (Quit: Leaving) |
| 12:13:50 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 12:16:16 | × | SummerSonw quits (~The_viole@203.77.49.232) (Client Quit) |
| 12:16:34 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 12:16:51 | × | SummerSonw quits (~The_viole@203.77.49.232) (Client Quit) |
| 12:17:01 | × | Rum quits (~bourbon@user/rum) (Quit: WeeChat 3.4) |
| 12:17:07 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 12:17:34 | × | SummerSonw quits (~The_viole@203.77.49.232) (Client Quit) |
| 12:17:50 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 12:18:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 12:18:52 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 12:23:58 | × | coot quits (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
| 12:26:17 | × | ishutin quits (~ishutin@80-95-82-198.pool.digikabel.hu) (Ping timeout: 240 seconds) |
| 12:28:12 | → | ishutin joins (~ishutin@92-249-182-7.pool.digikabel.hu) |
| 12:31:04 | → | _ht_ joins (~quassel@37.120.218.158) |
| 12:31:12 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Ping timeout: 268 seconds) |
| 12:33:03 | × | xff0x quits (~xff0x@2001:1a81:527e:7f00:c538:8d07:2658:ecf) (Ping timeout: 268 seconds) |
| 12:33:22 | → | xff0x joins (~xff0x@2001:1a81:527e:7f00:128f:5c47:b7cd:f118) |
| 12:34:25 | → | curiousgay joins (~curiousga@77-120-141-90.kha.volia.net) |
| 12:35:25 | → | alx741 joins (~alx741@157.100.93.160) |
| 12:36:26 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 12:37:22 | → | deadmarshal joins (~deadmarsh@95.38.115.121) |
| 12:39:15 | × | Jing quits (~hedgehog@2604:a840:3::1067) (Remote host closed the connection) |
| 12:39:54 | → | Jing joins (~hedgehog@2604:a840:3::1067) |
| 12:40:46 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 12:44:13 | × | Kaiepi quits (~Kaiepi@216.208.243.198) (Ping timeout: 240 seconds) |
| 12:53:25 | → | Kaiepi joins (~Kaiepi@216.208.243.103) |
| 12:58:52 | → | alx741 joins (~alx741@157.100.93.160) |
| 12:59:30 | → | raehik joins (~raehik@2a00:23c6:4c83:a901:95bf:f7ec:7b7d:c21e) |
| 13:00:37 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 13:02:59 | × | max22- quits (~maxime@2a01cb088335980042a847f93091dac4.ipv6.abo.wanadoo.fr) (Ping timeout: 252 seconds) |
| 13:03:36 | × | KvL quits (~KvL@user/KvL) (Quit: KvL) |
| 13:03:45 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 13:03:45 | × | otherwise quits (~otherwise@c-73-221-44-172.hsd1.wa.comcast.net) () |
| 13:04:37 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 13:04:45 | → | coot joins (~coot@89-64-85-93.dynamic.chello.pl) |
| 13:13:32 | × | raehik quits (~raehik@2a00:23c6:4c83:a901:95bf:f7ec:7b7d:c21e) (Ping timeout: 240 seconds) |
| 13:16:20 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:19:00 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 13:19:00 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 13:19:00 | → | wroathe joins (~wroathe@user/wroathe) |
| 13:20:37 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 13:20:56 | → | alx741 joins (~alx741@157.100.93.160) |
| 13:23:10 | → | nhatanh02 joins (~satori@123.24.172.30) |
| 13:23:49 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 13:26:23 | → | CiaoSen joins (~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 13:27:47 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:33:30 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:33:44 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:33:51 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:34:05 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:34:13 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:34:20 | × | coot quits (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
| 13:34:27 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:34:34 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:34:47 | → | coot joins (~coot@89-64-85-93.dynamic.chello.pl) |
| 13:34:48 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:34:56 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:35:09 | → | spaceseller joins (~spacesell@31.147.205.13) |
| 13:35:10 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:35:17 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:35:23 | → | slowButPresent joins (~slowButPr@user/slowbutpresent) |
| 13:35:32 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:35:39 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:35:55 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:36:02 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:36:16 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:36:24 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:36:38 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:36:46 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:36:59 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:37:07 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:37:22 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:37:23 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 13:37:30 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:37:44 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:37:52 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:38:06 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:38:14 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:38:28 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:38:36 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:38:50 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:38:58 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:39:11 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:39:12 | → | InternetCitizen joins (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) |
| 13:39:19 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:39:33 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:39:41 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:39:55 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:40:03 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:40:16 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:40:24 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:40:38 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:40:46 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:40:59 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:41:07 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:41:22 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:41:29 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:41:44 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:41:51 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:42:05 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:42:13 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:42:28 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:42:36 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:42:50 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:42:57 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:43:12 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:43:20 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:43:34 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:43:42 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:43:56 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:44:04 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:44:18 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:44:26 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:44:40 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:44:47 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:45:02 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:45:10 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:45:24 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:45:31 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:45:45 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:45:53 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 13:52:20 | → | desantra joins (~skykanin@user/skykanin) |
| 13:52:52 | × | desantra quits (~skykanin@user/skykanin) (Client Quit) |
| 13:53:09 | → | zincy joins (~tom@2a00:23c8:970c:4801:5b6a:e81b:79dc:f684) |
| 13:54:22 | → | desantra joins (~skykanin@user/skykanin) |
| 13:55:31 | → | alx741 joins (~alx741@157.100.93.160) |
| 14:02:01 | → | shriekingnoise joins (~shrieking@186.137.144.80) |
| 14:02:17 | × | spaceseller quits (~spacesell@31.147.205.13) (Quit: Leaving) |
| 14:02:40 | → | spaceseller joins (~spacesell@31.147.205.13) |
| 14:05:13 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 14:05:20 | × | coot quits (~coot@89-64-85-93.dynamic.chello.pl) (Read error: Connection reset by peer) |
| 14:05:33 | → | coot joins (~coot@89-64-85-93.dynamic.chello.pl) |
| 14:10:20 | × | desantra quits (~skykanin@user/skykanin) (Quit: WeeChat 3.3) |
| 14:16:20 | → | lavaman joins (~lavaman@98.38.249.169) |
| 14:18:58 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.3) |
| 14:19:21 | × | azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Quit: ZNC - https://znc.in) |
| 14:19:49 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 14:20:37 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 14:23:21 | → | max22- joins (~maxime@2a01cb0883359800fd0e15f8c1058ba6.ipv6.abo.wanadoo.fr) |
| 14:24:03 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 14:24:10 | → | _73` joins (~user@pool-108-49-252-36.bstnma.fios.verizon.net) |
| 14:24:21 | × | _73` quits (~user@pool-108-49-252-36.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 14:25:37 | × | _73 quits (~user@pool-108-49-252-36.bstnma.fios.verizon.net) (Ping timeout: 240 seconds) |
| 14:25:57 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 14:27:44 | × | spaceseller quits (~spacesell@31.147.205.13) (Quit: Leaving) |
| 14:27:55 | → | waleee joins (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
| 14:36:19 | → | zebrag joins (~chris@user/zebrag) |
| 14:38:24 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 14:38:24 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 14:38:24 | → | wroathe joins (~wroathe@user/wroathe) |
| 14:42:24 | → | alx741 joins (~alx741@157.100.93.160) |
| 14:44:40 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 14:45:24 | → | kalxd[m]1 joins (~kalxdmatr@2001:470:69fc:105::1:576e) |
| 14:47:16 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 14:48:43 | × | cheater quits (~Username@user/cheater) (Ping timeout: 250 seconds) |
| 14:49:18 | → | cheater joins (~Username@user/cheater) |
| 14:49:23 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 14:51:16 | → | bollu joins (uid233390@id-233390.helmsley.irccloud.com) |
| 14:53:44 | <InternetCitizen> | How does haskell having a definition for every function `t0 -> ... -> tn -> (t0, ... tn)`? |
| 14:54:22 | <InternetCitizen> | i.e how does it define all the functions `(,), (,,), (,,,) ...`? |
| 14:54:54 | × | tafa quits (~tafa@user/tafa) (Quit: ZNC - https://znc.in) |
| 14:54:55 | <InternetCitizen> | I opened GHCi and typed 39 commas and got a bit scared tbh |
| 14:55:01 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 14:56:20 | <[exa]> | InternetCitizen: if you overdo it a bit you might get an error saying that maximum tuple size is 62 |
| 14:56:33 | × | mikoto-chan quits (~mikoto-ch@esm-84-240-99-143.netplaza.fi) (Quit: mikoto-chan) |
| 14:56:35 | → | tafa joins (~tafa@user/tafa) |
| 14:56:53 | <InternetCitizen> | hahaha but how does it work? does the parser generate a constructor on the fly? |
| 14:57:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 14:57:26 | <InternetCitizen> | or are all 63 of them put into scope of every haskell program |
| 14:57:35 | <[exa]> | not sure, the tuple handling is a bit special, but generating the constructor name on the fly during parsing would make sense to me |
| 14:57:45 | <[exa]> | ie not sure if there's even a better way |
| 14:58:45 | <[exa]> | OTOH you may have a look at instances of the (,,,,,,,,,)'s, the useful ones (Show,Read,Bounded,...) usually end at like 16-tuples |
| 14:59:07 | <[exa]> | IIRC these are defined manually in base |
| 15:01:47 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 15:02:20 | × | _ht_ quits (~quassel@37.120.218.158) (Ping timeout: 252 seconds) |
| 15:02:49 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 15:02:57 | <geekosaur> | the instances are manual, tuples themselves are wired-in |
| 15:04:56 | → | alx741 joins (~alx741@157.100.93.160) |
| 15:06:40 | <InternetCitizen> | I tried the same thing in Rust and I was able to make a 1000-element tuple ... sheesh! |
| 15:07:07 | × | coot quits (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
| 15:07:07 | <InternetCitizen> | at this point I don't think the madlads even put a limit |
| 15:07:15 | → | acidjnk joins (~acidjnk@p200300d0c7271e9910698cbf36694c68.dip0.t-ipconnect.de) |
| 15:07:43 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:08:06 | → | coot joins (~coot@89-64-85-93.dynamic.chello.pl) |
| 15:09:31 | <geekosaur> | I think ghc wouldn't have one except at some point they discovered the compiler dumped core with 63-tuples. I'm not sure anyone ever tested to see if it was fixed |
| 15:09:54 | <geekosaur> | mostly because we discourage tuples that big anyway |
| 15:10:30 | <geekosaur> | given how we do argument passing and the like, the main place to use tuples is as function return values, and a 1000-tuple there is kinda wtf |
| 15:11:11 | <geekosaur> | also at some point we start preferring ADTs/records so you can get values by name instead of hoping you counted right |
| 15:11:39 | <InternetCitizen> | I totally agree, anything larger than 2 looses any semantics for me |
| 15:11:47 | <InternetCitizen> | 5000 and counting |
| 15:12:21 | <InternetCitizen> | I'm inclinding to make a small program to see at which point does the rust compiler break |
| 15:12:32 | <InternetCitizen> | or if my memory will run out before |
| 15:13:22 | geekosaur | bets 32768 or some other power of 2 matching a native (sub)word size |
| 15:13:35 | <geekosaur> | could take a while if that's 2^63 |
| 15:13:41 | × | CiaoSen quits (~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 15:14:49 | <[exa]> | InternetCitizen: in rust it's limited by source filesize!!1 |
| 15:15:13 | <InternetCitizen> | how big is that? |
| 15:15:44 | <[exa]> | well, a lot |
| 15:16:09 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 15:16:56 | <InternetCitizen> | 500MB ... |
| 15:17:04 | <[exa]> | anyway tuples for rust are afaik basically the same as structs, I guess the real technical limit there is when LLVM breaks |
| 15:17:58 | <InternetCitizen> | "rustc_driver dll on Windows bundles the whole compiler and LLVM into one file" |
| 15:18:07 | <[exa]> | it might get pretty quick if they try to pass that stuff through stack |
| 15:18:33 | <[exa]> | now that's a library. :D |
| 15:19:13 | <InternetCitizen> | https://github.com/rust-lang/rustup/issues/2490 |
| 15:19:36 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 276 seconds) |
| 15:20:03 | <[exa]> | ;_; |
| 15:25:39 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 15:30:28 | <geekosaur> | nice to know we're not the only ones who have the "suck everything into a single strict ByteString" issue |
| 15:31:17 | × | kjak quits (~kjak@pool-108-45-56-21.washdc.fios.verizon.net) (Ping timeout: 268 seconds) |
| 15:31:38 | <Rembane> | Different types of strings are an issue everywhere imo, they just pop up in different ways. |
| 15:33:19 | <geekosaur> | that wasn't really the aspect I was reaching for |
| 15:33:30 | <geekosaur> | more the thought process that "of course it'll always fit" |
| 15:33:49 | × | SummerSonw quits (~The_viole@203.77.49.232) (Remote host closed the connection) |
| 15:34:26 | <Rembane> | Got it. I think I might've internalized a bit too much muttering about strings. |
| 15:34:31 | → | alx741 joins (~alx741@157.100.93.160) |
| 15:36:11 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 15:37:34 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) |
| 15:41:08 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 15:41:21 | → | shapr` joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 15:41:46 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 15:41:46 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 15:41:46 | → | wroathe joins (~wroathe@user/wroathe) |
| 15:42:31 | → | mikoto-chan joins (~mikoto-ch@esm-84-240-99-143.netplaza.fi) |
| 15:42:37 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 15:42:57 | × | madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 240 seconds) |
| 15:43:04 | → | _73 joins (~user@pool-108-49-252-36.bstnma.fios.verizon.net) |
| 15:46:17 | × | shapr` quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 15:46:17 | × | mvk quits (~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds) |
| 15:46:37 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 15:49:08 | → | neurocyte0132889 joins (~neurocyte@94.46.76.127) |
| 15:49:08 | × | neurocyte0132889 quits (~neurocyte@94.46.76.127) (Changing host) |
| 15:49:08 | → | neurocyte0132889 joins (~neurocyte@user/neurocyte) |
| 15:51:03 | × | coot quits (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
| 15:51:35 | → | coot joins (~coot@89-64-85-93.dynamic.chello.pl) |
| 15:54:50 | × | ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 15:59:05 | → | alx741 joins (~alx741@157.100.93.160) |
| 16:00:08 | × | utk quits (~utk@2001:470:69fc:105::1:2fe0) (Quit: You have been kicked for being idle) |
| 16:00:19 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 16:00:19 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 16:00:19 | → | wroathe joins (~wroathe@user/wroathe) |
| 16:04:09 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 16:04:50 | → | kmein joins (~weechat@user/kmein) |
| 16:05:25 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 16:05:32 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 16:09:05 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 16:09:05 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 16:09:57 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 16:13:16 | → | thevishy joins (~Nishant@2405:201:f005:c007:2dcc:1488:1871:6935) |
| 16:13:47 | → | gaff joins (~gaff@49.207.212.166) |
| 16:14:54 | <gaff> | in quickcheck, is it possible to put in multiple assertions in a property, a === b; c === d? |
| 16:16:13 | → | ProfSimm joins (~ProfSimm@87.227.196.109) |
| 16:17:08 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 16:17:58 | <gaff> | for example, prop_1 x y = x ===2; y === 3 |
| 16:23:12 | × | cosimone quits (~user@93-34-133-35.ip49.fastwebnet.it) (Remote host closed the connection) |
| 16:23:22 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:24:38 | → | cosimone joins (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) |
| 16:26:10 | → | alx741 joins (~alx741@157.100.93.160) |
| 16:29:35 | <lyxia> | @check \x y -> (x === 2) .&&. (y === 3) |
| 16:29:37 | <lambdabot> | *** Failed! Falsifiable (after 1 test): |
| 16:29:37 | <lambdabot> | 0 0 LHS 0 /= 2 |
| 16:30:57 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 16:33:37 | → | machined1od joins (~machinedg@24.105.81.50) |
| 16:33:45 | × | machined1od quits (~machinedg@24.105.81.50) (Client Quit) |
| 16:35:05 | → | raehik joins (~raehik@2a00:23c6:4c83:a901:95bf:f7ec:7b7d:c21e) |
| 16:37:36 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 276 seconds) |
| 16:38:25 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 16:38:25 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 16:38:25 | → | wroathe joins (~wroathe@user/wroathe) |
| 16:38:38 | × | mikoto-chan quits (~mikoto-ch@esm-84-240-99-143.netplaza.fi) (Read error: No route to host) |
| 16:39:14 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 16:42:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 16:42:19 | → | mikoto-chan joins (~mikoto-ch@esm-84-240-99-143.netplaza.fi) |
| 16:44:37 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 16:45:56 | → | rekahsoft joins (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) |
| 16:48:42 | → | alx741 joins (~alx741@157.100.93.160) |
| 16:53:04 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 16:54:06 | → | mastarija joins (~mastarija@2a05:4f46:e0e:5000:d11e:1641:cfb6:79c3) |
| 16:54:32 | × | raehik quits (~raehik@2a00:23c6:4c83:a901:95bf:f7ec:7b7d:c21e) (Ping timeout: 268 seconds) |
| 17:03:18 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) (Remote host closed the connection) |
| 17:03:39 | × | bollu quits (uid233390@id-233390.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:05:06 | × | coolnickname quits (uid531864@user/coolnickname) (Quit: Connection closed for inactivity) |
| 17:05:59 | → | shapr joins (~user@pool-108-28-144-11.washdc.fios.verizon.net) |
| 17:06:01 | <gaff> | lyxia: `&&` takes boolean, but `===` returns `Property`, so how does that work? |
| 17:06:54 | <monochrom> | .&&. is not && |
| 17:07:09 | <gaff> | ok |
| 17:08:27 | <gaff> | thanks |
| 17:09:10 | <gaff> | i suppose likewise there is something like .||. as well |
| 17:09:21 | → | lavaman joins (~lavaman@98.38.249.169) |
| 17:09:31 | <int-e> | :t (.||.) |
| 17:09:32 | <lambdabot> | (STestable prop2, STestable prop1) => prop1 -> prop2 -> Test.QuickCheck.Safe.SProperty |
| 17:09:43 | <gaff> | yeah |
| 17:09:48 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 17:09:58 | <monochrom> | In retrospect I'm a bit surprised that === was not named .==. |
| 17:10:05 | <gaff> | love quickcheck |
| 17:10:35 | <gaff> | but coming with properties is quite an art |
| 17:10:53 | <int-e> | :t (==>) |
| 17:10:54 | <lambdabot> | STestable prop => Bool -> prop -> Test.QuickCheck.Safe.SProperty |
| 17:11:02 | <int-e> | (that one has no dots either) |
| 17:11:11 | <gaff> | yeah |
| 17:11:13 | → | alx741 joins (~alx741@157.100.93.160) |
| 17:11:24 | <geekosaur> | proper testing is always an art |
| 17:12:12 | <int-e> | (You can ignore the `S` in `STestable`, there's no huge difference, except that `Testable`s embed IO and this doesn't) |
| 17:13:02 | → | machined1od joins (~machinedg@24.105.81.50) |
| 17:13:04 | <gaff> | geekosaur: no i mean coming up with properties that do not duplicate source code -- that's something tricky -- i didn't know about it until i read hughes' paper. |
| 17:13:28 | → | machined2od joins (~machinedg@24.105.81.50) |
| 17:13:37 | × | machined2od quits (~machinedg@24.105.81.50) (Client Quit) |
| 17:13:41 | × | machined1od quits (~machinedg@24.105.81.50) (Client Quit) |
| 17:13:45 | × | machinedgod quits (~machinedg@24.105.81.50) (Quit: leaving) |
| 17:13:53 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 17:14:05 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 17:14:05 | <monochrom> | Oh there is still some value in properties that duplicate source code. It's called "white-box testing" and "path coverage" in some circles. >:) |
| 17:14:27 | monochrom | disbelieve in those, that's right. |
| 17:16:15 | <gaff> | i love the idea of random test data generation ... it is amazing what bugs you can catch |
| 17:16:15 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 17:16:39 | → | sirlensalot joins (~sirlensal@ool-44c5f8c9.dyn.optonline.net) |
| 17:16:48 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:17:15 | <gaff> | and quickcheck design -- those guys can really do some great stuff with types |
| 17:17:41 | <gaff> | thanks |
| 17:17:48 | × | gaff quits (~gaff@49.207.212.166) () |
| 17:20:27 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) |
| 17:21:05 | → | machined1od joins (~machinedg@24.105.81.50) |
| 17:21:19 | × | machinedgod quits (~machinedg@24.105.81.50) (Quit: leaving) |
| 17:21:40 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 17:23:05 | × | mbuf quits (~Shakthi@122.162.67.169) (Quit: Leaving) |
| 17:25:22 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) (Ping timeout: 268 seconds) |
| 17:27:25 | × | Morrow quits (~quassel@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 240 seconds) |
| 17:28:06 | → | Morrow joins (~quassel@bzq-110-168-31-106.red.bezeqint.net) |
| 17:29:53 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 17:29:53 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 17:29:53 | → | wroathe joins (~wroathe@user/wroathe) |
| 17:30:29 | → | econo joins (uid147250@user/econo) |
| 17:31:37 | × | vglfr quits (~vglfr@88.155.12.39) (Ping timeout: 240 seconds) |
| 17:34:40 | → | alx741 joins (~alx741@157.100.93.160) |
| 17:34:55 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
| 17:35:14 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 17:35:24 | → | cheater joins (~Username@user/cheater) |
| 17:37:20 | × | DNH quits (~DNH@2a02:8108:1100:16d8:7457:6675:c5ec:bb4b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 17:38:32 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) |
| 17:39:19 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 17:47:26 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 17:48:41 | → | DNH joins (~DNH@2a02:8108:1100:16d8:7457:6675:c5ec:bb4b) |
| 17:51:19 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:51:51 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:52:29 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 17:56:02 | × | acidjnk quits (~acidjnk@p200300d0c7271e9910698cbf36694c68.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 17:57:01 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) (Ping timeout: 250 seconds) |
| 17:57:11 | → | alx741 joins (~alx741@157.100.93.160) |
| 17:59:54 | → | dignissimus joins (~dignissim@88-104-68-62.dynamic.dsl.as9105.com) |
| 18:00:01 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) |
| 18:02:00 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 18:03:28 | × | neurocyte0132889 quits (~neurocyte@user/neurocyte) (Quit: The Lounge - https://thelounge.chat) |
| 18:04:04 | <dignissimus> | Can I use record syntac with GADTs? If so, have I made a mistake here? https://paste.tomsmeding.com/aeKbFFLr |
| 18:05:55 | <geekosaur> | I think the syntax is: data Foo where {fields} -> Constructor |
| 18:06:15 | <monochrom> | Heh, the correct syntax is e.g. LambdaExpression :: { lambdaVariable :: Variable, ... } -> Expression |
| 18:06:28 | → | coot_ joins (~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) |
| 18:07:05 | <dignissimus> | Thank you! |
| 18:07:09 | × | coot quits (~coot@89-64-85-93.dynamic.chello.pl) (Ping timeout: 256 seconds) |
| 18:07:57 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 18:11:01 | → | n3rdy1 joins (~n3rdy1@2600:1700:4570:3480::41) |
| 18:11:55 | → | zmt01 joins (~zmt00@user/zmt00) |
| 18:11:57 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 240 seconds) |
| 18:15:42 | → | spaceseller_ joins (~spacesell@31.147.205.13) |
| 18:18:07 | → | alx741 joins (~alx741@157.100.93.160) |
| 18:18:34 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 18:22:35 | → | neurocyte0132889 joins (~neurocyte@94.46.76.127) |
| 18:22:35 | × | neurocyte0132889 quits (~neurocyte@94.46.76.127) (Changing host) |
| 18:22:35 | → | neurocyte0132889 joins (~neurocyte@user/neurocyte) |
| 18:22:56 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:22:57 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 18:23:15 | × | spaceseller_ quits (~spacesell@31.147.205.13) (Quit: Leaving) |
| 18:24:37 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 18:25:18 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 18:25:47 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 18:27:42 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 18:30:02 | → | whatsupdoc joins (uid509081@id-509081.hampstead.irccloud.com) |
| 18:33:52 | → | tomku joins (~tomku@user/tomku) |
| 18:37:56 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 18:38:20 | × | thevishy quits (~Nishant@2405:201:f005:c007:2dcc:1488:1871:6935) (Quit: Leaving) |
| 18:40:39 | → | alx741 joins (~alx741@157.100.93.160) |
| 18:41:03 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 18:41:03 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 18:41:03 | → | wroathe joins (~wroathe@user/wroathe) |
| 18:42:34 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:44:03 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 18:44:58 | × | johnw quits (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
| 18:46:30 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 18:48:41 | → | learner-monad joins (~ehanneken@user/learner-monad) |
| 18:48:59 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 18:51:47 | → | yauhsien joins (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
| 18:53:30 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 18:54:46 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
| 18:57:35 | × | yauhsien quits (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Ping timeout: 256 seconds) |
| 18:58:09 | → | coolnickname joins (uid531864@user/coolnickname) |
| 19:00:23 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:02:43 | → | alx741 joins (~alx741@157.100.93.160) |
| 19:04:02 | × | max22- quits (~maxime@2a01cb0883359800fd0e15f8c1058ba6.ipv6.abo.wanadoo.fr) (Ping timeout: 268 seconds) |
| 19:04:49 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 250 seconds) |
| 19:05:49 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 19:08:13 | × | mikoto-chan quits (~mikoto-ch@esm-84-240-99-143.netplaza.fi) (Read error: No route to host) |
| 19:09:55 | → | mikoto-chan joins (~mikoto-ch@esm-84-240-99-143.netplaza.fi) |
| 19:11:43 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 19:11:43 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 19:11:43 | → | wroathe joins (~wroathe@user/wroathe) |
| 19:14:47 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 19:15:21 | → | ensyde joins (~ensyde@2600:1702:2e30:1a40:d506:18a6:e0ef:8a3a) |
| 19:15:53 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
| 19:16:00 | × | mikoto-chan quits (~mikoto-ch@esm-84-240-99-143.netplaza.fi) (Read error: No route to host) |
| 19:18:00 | → | mikoto-chan joins (~mikoto-ch@esm-84-240-99-143.netplaza.fi) |
| 19:19:31 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 19:19:55 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 19:20:45 | <dignissimus> | I have `data Entails a b = Entails a b`, I have `type (:-) = Entails` which works fine but `(:-) = Entails` doesn't work as a synonym for the constructor, is it possible to do what I want to do? |
| 19:20:52 | → | travv0 joins (sid293381@user/travv0) |
| 19:21:57 | <tomsmeding> | dignissimus: what about `data a :- b = a :- b`? |
| 19:23:07 | <tomsmeding> | but if you don't want that: `(:-) = Entails` doesn't work for the same reason that `Something = Entails` doesn't work; you want to define a variable, but variables must be lowercase. And "uppercase symbols" in Haskell are symbols starting with : -- except for (:) itself, that is |
| 19:23:35 | <tomsmeding> | but if you want to define a "fake constructor", you can use pattern synonyms :) |
| 19:24:20 | <tomsmeding> | (low-tech alternative: try |- ) |
| 19:26:07 | <dignissimus> | tomsmeding: Thank you! |
| 19:26:19 | → | madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 19:26:34 | <dignissimus> | I'll have to look into pattern synonyms, I just searched it but it wasn't making intuitive sense |
| 19:26:57 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 19:27:01 | <dignissimus> | I think I like `data a :- b = a :- b` with `type Entails = (:-)` and `entails = (:-)` |
| 19:27:42 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 19:31:32 | → | zer0bitz joins (~zer0bitz@194.34.133.91) |
| 19:32:52 | × | _73 quits (~user@pool-108-49-252-36.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 19:33:40 | <tomsmeding> | dignissimus: pattern (:-) :: a -> b -> Entails a b ; pattern (:-) = Entails |
| 19:33:54 | <tomsmeding> | but preferably understand what they do first :) |
| 19:34:00 | <tomsmeding> | I like your suggestion as well, more idiomatic |
| 19:34:10 | <tomsmeding> | (in a way) |
| 19:37:01 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 240 seconds) |
| 19:37:21 | tomsmeding | is still amused that Haskell has a concept of an uppercase symbol |
| 19:38:00 | → | alx741 joins (~alx741@157.100.93.160) |
| 19:39:31 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 19:39:50 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 19:40:05 | × | nhatanh02 quits (~satori@123.24.172.30) (Ping timeout: 256 seconds) |
| 19:40:14 | → | yauhsien joins (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
| 19:42:57 | <Henson> | for those interested in a follow up from yesterday's conversation, changing "unsafe" to "safe" fixed my problem. I thought that term applied to the kind of function that was being called, and not the method by which Haskell called the functions. I thought all of my functions were "unsafe" because they were in IO, not that Haskell was using an "unsafe" method of calling them. |
| 19:42:57 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 19:43:36 | <geekosaur> | yeh, I had that confusion at first as well. wish there were a better way to get that across |
| 19:44:02 | <EvanR> | using an IO type or not is how the "is IO" is expressed in the ffi |
| 19:44:14 | <geekosaur> | ironically it's almost the opposite: functions that do no IO, blocking, or memory allocation can be called "unsafe" for the most part |
| 19:44:30 | <EvanR> | if you don't put IO, you're promising the other end of this ffi call is pure |
| 19:44:46 | <geekosaur> | I think you always have to put IO |
| 19:44:55 | <EvanR> | for ffi bindings? no |
| 19:45:02 | × | yauhsien quits (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
| 19:45:02 | <geekosaur> | you're just allows to use unsafeLocalState around the call if it isn't actually in IO |
| 19:45:08 | <geekosaur> | *allowed |
| 19:45:19 | <EvanR> | i.e. the C math library (if you're careful) can be not IO |
| 19:51:09 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 19:51:38 | × | InternetCitizen quits (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) (Ping timeout: 252 seconds) |
| 19:51:49 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Client Quit) |
| 19:51:58 | → | max22- joins (~maxime@2a01cb08833598003c7cbbeb6c92ab00.ipv6.abo.wanadoo.fr) |
| 19:52:02 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 19:54:13 | → | yauhsien joins (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
| 19:55:08 | → | lavaman joins (~lavaman@98.38.249.169) |
| 19:59:17 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 19:59:20 | → | wroathe joins (~wroathe@user/wroathe) |
| 20:00:01 | <dignissimus> | Which is preferred? `sort ctx _ = ...` or `sort ctx = const $ ...`? |
| 20:00:29 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 20:00:29 | <dignissimus> | As an example: sort ctx = const $ ctx :- Judgement (TypeExpression (Kind KindType)) TypeOfKin |
| 20:01:26 | → | alx741 joins (~alx741@157.100.93.160) |
| 20:03:36 | → | Feuermagier_ joins (~Feuermagi@84.17.49.78) |
| 20:05:01 | × | juhp quits (~juhp@128.106.188.82) (Ping timeout: 240 seconds) |
| 20:05:47 | <hpc> | what is that extra parameter normally? |
| 20:05:57 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Ping timeout: 240 seconds) |
| 20:05:57 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 20:06:20 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 20:06:21 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.3) |
| 20:06:25 | <dignissimus> | hpc: List of "entailments" |
| 20:06:25 | <tomsmeding> | why make a distinction between the first and second parameter? |
| 20:06:45 | <dignissimus> | tomsmeding: What do you mean by that? |
| 20:06:49 | <EvanR> | the one with const $ is longer for no reason |
| 20:06:52 | <hpc> | tomsmeding: it could be like lens where you want to think of the partially applied function as a full object in and of itself |
| 20:06:57 | → | juhp joins (~juhp@128.106.188.82) |
| 20:07:02 | → | epolanski joins (uid312403@id-312403.helmsley.irccloud.com) |
| 20:07:09 | <hpc> | when in doubt i would definitely go with sort ctx _ though |
| 20:07:27 | <tomsmeding> | dignissimus: why would you even consider writing one with a normal argument ("ctx") and one with a pointfree function ("const") -- not saying it's not a good idea, just asking what the difference is |
| 20:08:14 | <EvanR> | maybe the sort is the second case in a list of equations |
| 20:10:37 | × | Vajb quits (~Vajb@nabiicwveotvxswi5-2.v6.elisa-mobile.fi) (Ping timeout: 268 seconds) |
| 20:10:46 | → | Vajb joins (~Vajb@2001:999:230:a44e:bc17:5155:7945:add1) |
| 20:11:14 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 20:11:35 | <dignissimus> | tomsmeding: I don't think there's a specific reason. I have `sort :: InferenceRule` and `type InferenceRule = Context -> [Entailment] -> Entailment` |
| 20:11:52 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:11:58 | <dignissimus> | These are the rules https://i.imgur.com/EfeOygF.png |
| 20:12:18 | <tomsmeding> | dignissimus: then I'd just go with sort ctx _ = |
| 20:12:27 | <dignissimus> | Thank you everyone |
| 20:12:34 | <dignissimus> | When would const be preferred? |
| 20:12:37 | <tomsmeding> | that, or sort = \ctx _ -> ..., if you feel like they shouldn't be proper arguments |
| 20:13:23 | <tomsmeding> | if there was a meaningful difference between the first and the second argument, like if it was 'sort :: A -> Rule' where 'type Rule = B -> C', then perhaps const -- but even then I'd probably just go with 'sort ctx _ =' |
| 20:13:35 | <tomsmeding> | or even 'sort ctx = \_ -> ...' :) |
| 20:14:27 | <EvanR> | const can make passing arguments to a higher order function more convenient, similar to partialling, flip, etc |
| 20:14:47 | <EvanR> | or section involving $ |
| 20:17:06 | <EvanR> | e.g. you wrote sort ctx = assuming 1 arg, then later when something wants a 2 arg function you pass (const sort) |
| 20:18:39 | × | yauhsien quits (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 20:19:29 | → | yauhsien joins (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
| 20:19:57 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 240 seconds) |
| 20:20:08 | × | hughjfchen[m] quits (~hughjfche@2001:470:69fc:105::c29d) (Quit: Client limit exceeded: 20000) |
| 20:22:37 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 20:23:58 | → | alx741 joins (~alx741@181.199.42.79) |
| 20:24:49 | × | yauhsien quits (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Ping timeout: 268 seconds) |
| 20:27:03 | × | alx741 quits (~alx741@181.199.42.79) (Read error: Connection reset by peer) |
| 20:28:08 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 20:28:08 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 20:28:11 | allbery_b | is now known as geekosaur |
| 20:29:06 | × | euandreh quits (~euandreh@191.181.59.160) (Ping timeout: 245 seconds) |
| 20:29:13 | → | otherwise joins (~otherwise@2601:602:880:90f0:9dc:9663:8c4e:291b) |
| 20:29:59 | → | InternetCitizen joins (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) |
| 20:31:18 | <otherwise> | in ghci I can :set +s to show time spent during an evaluation. is there a way to add this a main.hs so that this information is also returned when running ./main (outside of ghci)? |
| 20:31:31 | → | hughjfchen[m] joins (~hughjfche@2001:470:69fc:105::c29d) |
| 20:31:37 | <EvanR> | try -s |
| 20:31:39 | <monochrom> | No. |
| 20:31:41 | <EvanR> | +RTS -s |
| 20:31:54 | <monochrom> | Err I guess that works. |
| 20:32:36 | → | mvk joins (~mvk@2607:fea8:5cdd:f000::917a) |
| 20:34:20 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 20:34:20 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 20:34:20 | → | wroathe joins (~wroathe@user/wroathe) |
| 20:35:13 | <otherwise> | EvanR where do I put +RTS -s ? |
| 20:35:30 | <EvanR> | when you run ./main |
| 20:36:32 | <EvanR> | command line arguments |
| 20:37:15 | <otherwise> | hmm okay |
| 20:40:17 | → | burnsidesLlama joins (~burnsides@dhcp168-010.wadham.ox.ac.uk) |
| 20:41:48 | → | jeetelongname joins (~jeet@88-111-159-26.dynamic.dsl.as9105.com) |
| 20:42:34 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 20:44:13 | → | alx741 joins (~alx741@157.100.93.160) |
| 20:44:30 | <otherwise> | omg it worked! cool, thanks EvanR |
| 20:44:37 | × | madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 240 seconds) |
| 20:45:09 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 20:45:55 | <EvanR> | also -S gives you a running dump of GC stats |
| 20:46:18 | <EvanR> | which could be interesting for a long-running program |
| 20:46:39 | <otherwise> | so is +RTS -s haskell specific command? also, is there a resource online for me to read more about adding commands to the end of ./main. in general? |
| 20:46:50 | <EvanR> | yes |
| 20:47:33 | <EvanR> | https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/runtime_control.html |
| 20:48:49 | <geekosaur> | you can also provide user-specified options not handled by the RTS; those are available to the program via https://downloads.haskell.org/ghc/latest/docs/html/libraries/base-4.16.0.0/System-Environment.html#v:getArgs |
| 20:49:05 | × | coot_ quits (~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) (Quit: coot_) |
| 20:49:29 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 20:49:47 | × | dignissimus quits (~dignissim@88-104-68-62.dynamic.dsl.as9105.com) (Ping timeout: 256 seconds) |
| 20:49:47 | <otherwise> | okay, i need to get better at navigating online GHC documentation, it seems like all my questions are answered there. However it is kind of a catch-22, because I often don't have the technical language to even ask the question properly, so that makes navigating GHC documentation more difficult at this point in my learning curve... |
| 20:50:14 | <EvanR> | just reading the whole manual is a thing |
| 20:50:18 | → | madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 20:50:34 | <EvanR> | that I haven't done, but back in the day it helped |
| 20:50:51 | <geekosaur> | …skipping over parts that don't make sense at first, like some of the fancy type foo |
| 20:51:29 | → | dignissimus joins (~dignissim@88-104-68-62.dynamic.dsl.as9105.com) |
| 20:57:27 | → | pavonia joins (~user@user/siracusa) |
| 21:01:51 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 21:07:53 | → | alx741 joins (~alx741@157.100.93.160) |
| 21:08:21 | <EvanR> | wow lazy Writer is very lazy... and strict Writer is not very strict |
| 21:09:04 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 21:09:35 | <monochrom> | strict State is not very strict either. |
| 21:10:00 | → | falafel joins (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
| 21:11:15 | <EvanR> | as long as the monoid is lazy enough should work |
| 21:11:19 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 21:12:17 | × | dignissimus quits (~dignissim@88-104-68-62.dynamic.dsl.as9105.com) (Ping timeout: 268 seconds) |
| 21:12:27 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 21:13:28 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 21:14:17 | × | mvk quits (~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds) |
| 21:14:51 | <EvanR> | the process of getting the results from runWriter is reminding me of the break/span thing which had surprising performance |
| 21:16:14 | <EvanR> | the result is a pair whose computational fate of components is inextricably linked |
| 21:19:28 | <EvanR> | did don knuth say way back when the only way to predict performance is to consider everything to be bits and bytes and machine code instructions xD |
| 21:19:35 | × | kaph quits (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
| 21:19:53 | <EvanR> | how to haskell |
| 21:19:58 | <geekosaur> | even that doens't work these days thanks to caching and such |
| 21:21:11 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 21:22:50 | → | kaph joins (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
| 21:24:14 | <c_wraith> | back when racing the beam was a thing, you had to be deterministic. |
| 21:24:33 | <c_wraith> | those days are long past |
| 21:25:01 | <jackdk> | we have CPS WriterT now, but you need the unreleased mtl-2.3 to get a MonadWriter instance for it |
| 21:26:14 | × | doyougnu quits (~doyougnu@c-73-25-202-122.hsd1.or.comcast.net) (Ping timeout: 252 seconds) |
| 21:28:34 | × | falafel quits (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Remote host closed the connection) |
| 21:28:52 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 21:28:52 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 21:28:52 | → | wroathe joins (~wroathe@user/wroathe) |
| 21:28:57 | → | falafel joins (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
| 21:29:59 | <qrpnxz> | iterators are just lists, laziness is super power |
| 21:30:47 | × | zer0bitz quits (~zer0bitz@194.34.133.91) (Ping timeout: 268 seconds) |
| 21:31:19 | → | alx741 joins (~alx741@157.100.93.160) |
| 21:32:02 | → | johnw joins (~johnw@2607:f6f0:3004:1:c8b4:50ff:fef8:6bf0) |
| 21:32:48 | → | falafel_ joins (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
| 21:33:13 | <EvanR> | how we see ourselves: iron man, how everyone else sees us: the cosplay tron dude from programming language battle grid |
| 21:33:18 | → | uam joins (uid360535@id-360535.hampstead.irccloud.com) |
| 21:33:25 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 21:35:37 | × | falafel quits (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Ping timeout: 240 seconds) |
| 21:36:05 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 21:37:16 | → | acidjnk joins (~acidjnk@pd9e0bdc0.dip0.t-ipconnect.de) |
| 21:37:37 | × | falafel_ quits (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Ping timeout: 240 seconds) |
| 21:38:17 | <qrpnxz> | lol |
| 21:38:58 | <qrpnxz> | I'm going to be doing file manupulation for the first time in haskell, and i was surprised how much there is in System.IO, hopefully enough. |
| 21:39:43 | <EvanR> | see also Data.ByteString I/O section |
| 21:40:30 | <qrpnxz> | ty |
| 21:40:37 | → | dignissimus joins (~dignissim@88-104-68-62.dynamic.dsl.as9105.com) |
| 21:42:07 | → | mvk joins (~mvk@2607:fea8:5cdd:f000::917a) |
| 21:42:59 | <EvanR> | aaand Control.Exception since file manipulation communicates some stuff by throwing |
| 21:43:21 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 21:43:38 | <EvanR> | i.e. file not found |
| 21:43:46 | <qrpnxz> | ohhh, good heads up |
| 21:44:02 | <dsal> | qrpnxz: what kinds of files? I don't end up using system.io very much. |
| 21:44:10 | → | euandreh joins (~euandreh@2804:14c:33:9fe5:203e:45d6:8d1a:1058) |
| 21:45:43 | <qrpnxz> | I want to port a audio metadata editor from C, so audio files. Common case it will read very few bytes, if possible overwrite as much, worse case rewrite the metadata and copy the rest of the file. |
| 21:46:07 | <dsal> | Ah, so actual low level stuff. :) |
| 21:46:22 | <qrpnxz> | yeah pretty low level for the overwrite case |
| 21:47:23 | <qrpnxz> | and i'd like to build some of the structures by hand as well, what's idiomatic serialization in Haskell? Should I use Show or is there something more "efficient"? |
| 21:47:34 | <dsal> | Definitely not show. |
| 21:47:41 | <qrpnxz> | right |
| 21:47:55 | × | coolnickname quits (uid531864@user/coolnickname) (Quit: Connection closed for inactivity) |
| 21:48:14 | <dsal> | But it depends on the structure. I did mqtt "by hand" with a class that's I probably named "ByteMe" or something which makes a ByteStream out of a thing. |
| 21:48:57 | <qrpnxz> | yeah, something like that was the plan if there wasn't anything else |
| 21:49:10 | <geekosaur> | depends on how you want to serialize stuff. there are libraries for things like protobuf, json, yaml, bson, toml, etc.; there are libraries for Haskell-specific serialization with type information (binary, cereal), etc. |
| 21:49:35 | <dsal> | If you want to encode your data into mqtt packets, I've got something that will do that. |
| 21:49:35 | <geekosaur> | if you need to serialize for direct consumption by C/FFI, there's the Storable class |
| 21:50:44 | <EvanR> | if there's no library for your metadata format already I'm going to guess use `binary' package |
| 21:53:11 | → | falafel_ joins (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
| 21:53:25 | <qrpnxz> | "binary" looks like what I want, thank you all |
| 21:53:51 | → | alx741 joins (~alx741@157.100.93.160) |
| 21:54:41 | → | Gurkenglas joins (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) |
| 21:57:03 | × | Kaiepi quits (~Kaiepi@216.208.243.103) (Read error: Connection reset by peer) |
| 21:57:41 | → | falafel__ joins (~falafel@cpe-76-168-195-162.socal.res.rr.com) |
| 21:58:22 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 21:58:53 | → | CiaoSen joins (~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 21:58:57 | × | deadmarshal quits (~deadmarsh@95.38.115.121) (Ping timeout: 240 seconds) |
| 22:00:16 | <qrpnxz> | storable also note worthy thanks |
| 22:00:37 | × | falafel_ quits (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Ping timeout: 240 seconds) |
| 22:01:00 | → | SummerSonw joins (~The_viole@203.77.49.232) |
| 22:01:57 | × | falafel__ quits (~falafel@cpe-76-168-195-162.socal.res.rr.com) (Ping timeout: 240 seconds) |
| 22:03:12 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 22:04:50 | <dignissimus> | Could somebody check the style of my code? https://paste.tomsmeding.com/BBtrf7nI |
| 22:05:43 | → | Guest13 joins (~Guest13@p200300c8973682c385b00e33b8703e1f.dip0.t-ipconnect.de) |
| 22:05:47 | × | Guest13 quits (~Guest13@p200300c8973682c385b00e33b8703e1f.dip0.t-ipconnect.de) (Client Quit) |
| 22:06:09 | <dignissimus> | I've just figured out how I want to go about doing things, I want to make sure the code can be read easily or if I've done something weird |
| 22:07:56 | <EvanR> | I can read it xD |
| 22:08:06 | <dignissimus> | Yay! |
| 22:08:27 | <dignissimus> | I think I'm slowly getting the hang of haskell |
| 22:09:21 | <glguy> | dignissimus: I'd switch to using derived Eq instances when you can, and not providing Eq instances when they are incomplete |
| 22:09:44 | <glguy> | In some cases with GADTs you can derive them using StandaloneDeriving when you couldn't have derived them the normal way |
| 22:10:54 | <glguy> | If you need a custom Eq instance for a very special reason it should have comment explaining the reason |
| 22:11:11 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) (Remote host closed the connection) |
| 22:12:56 | <dignissimus> | glguy: Thank you! I'm a bit confused about StandaloneDeriving, after searching I've understood that it's a pragma that allows me to write deriving statements on their own, but I don't understand much else |
| 22:13:16 | <glguy> | in the case of your file, it's not needed |
| 22:13:40 | <glguy> | (you aren't using any GADTs) |
| 22:14:16 | <geekosaur> | it's sometimes useful when you need an instance that the original author didn't derive for you, but only in executables (otherwise, well, orphan instances are a nasty trap for the unsuspecting) |
| 22:14:41 | <geekosaur> | and otherwise useful because they can derive things for GADTs when normal deriving can't, as glguy said |
| 22:15:26 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:15:50 | <geekosaur> | in general I'd consider the first use a small and the second use risky because in most cases where normal deriving won't work, there's good reason it won't and not even a manually written instance will work |
| 22:16:22 | → | alx741 joins (~alx741@157.100.93.160) |
| 22:16:43 | <glguy> | It's not that dire, sometimes the deriver just needs some help with the type indexes |
| 22:16:55 | <glguy> | you don't get a bad instance out of it |
| 22:18:02 | <glguy> | easy example: https://glguy.net/advent/sln_2021_22/src/Main.html#Box |
| 22:20:06 | <geekosaur> | right, I'm mostly thinking of the GADTs that hide existentials that can never be proven Eq |
| 22:20:25 | <dignissimus> | glguy: With GADTs, I initially used the GADT pragma because I wanted to encode type information expression with the `Expression` type, I then realised I couldn't do this. Now, if I remove the GADT pragma, I'm told SimpleType is an illegal GADT declaration, how come? (I can't tell why it can't be done without the extension) |
| 22:20:54 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 22:20:55 | <glguy> | dignissimus: You can use the GADTSyntax extension if you want to use that syntax without any of the extensions that GADTs bring along |
| 22:21:32 | <dignissimus> | Thank you! That worked |
| 22:22:29 | × | madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Quit: Lost terminal) |
| 22:24:50 | <geekosaur> | (my main complaint about the cases I'm thinking of is that ghc will happily derive something that can't work and then vomit it up at you as if it was your fault) |
| 22:24:50 | × | cheater quits (~Username@user/cheater) (Ping timeout: 260 seconds) |
| 22:25:41 | <geekosaur> | it does at least say "while typechecking a derived Eq instance" or some such, but otherwise leaves you wondering where tf that code came from |
| 22:28:20 | → | cheater joins (~Username@user/cheater) |
| 22:30:20 | → | coot joins (~coot@89-64-85-93.dynamic.chello.pl) |
| 22:30:39 | <ProfSimm> | Could Haskell effectively model a neural network? |
| 22:32:13 | <geekosaur> | there's at least one although I note it's a bit out of date: https://hackage.haskell.org/package/neural |
| 22:32:26 | <geekosaur> | wouldn't be surprised if there are others |
| 22:35:24 | → | notzmv joins (~zmv@user/notzmv) |
| 22:36:34 | → | Midjak joins (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) |
| 22:37:13 | → | Everything joins (~Everythin@37.115.210.35) |
| 22:37:41 | → | Midjak2 joins (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) |
| 22:38:15 | × | Midjak2 quits (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) (Client Quit) |
| 22:38:15 | × | Midjak quits (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) (Client Quit) |
| 22:38:54 | → | alx741 joins (~alx741@157.100.93.160) |
| 22:39:30 | × | max22- quits (~maxime@2a01cb08833598003c7cbbeb6c92ab00.ipv6.abo.wanadoo.fr) (Quit: Leaving) |
| 22:41:33 | × | DNH quits (~DNH@2a02:8108:1100:16d8:7457:6675:c5ec:bb4b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 22:41:55 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 22:42:01 | × | Katarushisu quits (~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net) (Quit: The Lounge - https://thelounge.chat) |
| 22:42:38 | × | coot quits (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
| 22:43:12 | → | Katarushisu joins (~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net) |
| 22:43:22 | → | Midjak joins (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) |
| 22:48:14 | <dignissimus> | https://github.com/dignissimus/Halt/ Thus begins my ambitious project XD |
| 22:48:42 | <dignissimus> | I don't really see it going anywhere, agda and idris already exist and they're very good |
| 22:49:11 | → | vglfr joins (~vglfr@88.155.60.141) |
| 22:49:11 | <dignissimus> | But I'll be very happy when I've made it, I'd like to see algorithms become first class data types |
| 22:49:19 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 22:49:19 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 22:49:19 | → | wroathe joins (~wroathe@user/wroathe) |
| 22:51:18 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 22:51:45 | → | Codaraxis__ joins (~Codaraxis@user/codaraxis) |
| 22:52:25 | → | DNH joins (~DNH@2a02:8108:1100:16d8:7457:6675:c5ec:bb4b) |
| 22:55:53 | × | Codaraxis_ quits (~Codaraxis@user/codaraxis) (Ping timeout: 268 seconds) |
| 22:57:05 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 22:57:05 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 22:57:09 | allbery_b | is now known as geekosaur |
| 23:06:25 | × | ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 23:08:02 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 23:09:26 | → | alx741 joins (~alx741@157.100.93.160) |
| 23:11:21 | → | python476 joins (~user@88.160.31.174) |
| 23:15:09 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 23:16:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 23:16:22 | → | doyougnu joins (~doyougnu@c-73-25-202-122.hsd1.or.comcast.net) |
| 23:17:52 | → | acidjnk_new joins (~acidjnk@p200300d0c7271e9411aaafeb7bff4a7a.dip0.t-ipconnect.de) |
| 23:18:17 | × | chomwitt quits (~chomwitt@2a02:587:dc1e:c100:12c3:7bff:fe6d:d374) (Remote host closed the connection) |
| 23:29:25 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 23:29:36 | <InternetCitizen> | dignissimus: seems very interesting, never even heard of this, I though there was no way to deal with the halting problem, could you show me some code snippets? |
| 23:31:29 | → | alx741 joins (~alx741@157.100.93.160) |
| 23:34:02 | × | cosimone quits (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Ping timeout: 240 seconds) |
| 23:35:10 | × | otherwise quits (~otherwise@2601:602:880:90f0:9dc:9663:8c4e:291b) () |
| 23:35:42 | → | otherwise joins (~otherwise@2601:602:880:90f0:9dc:9663:8c4e:291b) |
| 23:36:47 | <dignissimus> | InternetCitizen: The language won't be turing complete, so I'll be able to make it so termination is decidable |
| 23:37:16 | <pfurla-matrix> | yeah, Turing incomplete languages are a thing |
| 23:37:22 | <dignissimus> | For example, you wouldn't be able to define the collatz function without a proof it terminates |
| 23:37:30 | <EvanR> | really, you can decide yes terminates, or not does not? xD |
| 23:37:43 | <EvanR> | haven't seen that one |
| 23:38:33 | <EvanR> | usually it's yes terminates or not sure, reject it |
| 23:39:20 | × | mastarija quits (~mastarija@2a05:4f46:e0e:5000:d11e:1641:cfb6:79c3) (Quit: Leaving) |
| 23:42:50 | <dignissimus> | InternetCitizen: Haven't written the parser yet and I still don't know what it'll look like exactly, but here are some doodles I made a while ago, it looks similar to haskell but I'm looking into adding imperative syntax too https://paste.tomsmeding.com/Eoh9qSzC |
| 23:43:21 | <dignissimus> | EvanR: I'm too lazy to write termination checking, you must supply your own proof! :D |
| 23:43:36 | <EvanR> | oof |
| 23:44:01 | <EvanR> | well depending on the language that might not be so bad |
| 23:44:42 | <EvanR> | e.g. imagine if the only thing you could do is map and fold finite structures using total primitives |
| 23:44:48 | <geekosaur> | that's fairly common, actually |
| 23:45:23 | <geekosaur> | the providing your own proof, that is |
| 23:45:56 | × | alx741 quits (~alx741@157.100.93.160) (Read error: Connection reset by peer) |
| 23:47:01 | × | Jing quits (~hedgehog@2604:a840:3::1067) (Remote host closed the connection) |
| 23:47:40 | → | Jing joins (~hedgehog@2604:a840:3::1067) |
| 23:48:13 | × | acidjnk_new quits (~acidjnk@p200300d0c7271e9411aaafeb7bff4a7a.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 23:48:27 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 23:48:37 | × | acidjnk quits (~acidjnk@pd9e0bdc0.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 23:52:47 | <glguy> | int-e: you around, I want to share a cool thign about day 22 |
| 23:54:57 | × | python476 quits (~user@88.160.31.174) (Ping timeout: 240 seconds) |
| 23:57:12 | × | DNH quits (~DNH@2a02:8108:1100:16d8:7457:6675:c5ec:bb4b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 23:57:40 | → | DNH joins (~DNH@2a02:8108:1100:16d8:7457:6675:c5ec:bb4b) |
| 23:58:34 | <glguy> | int-e: OK, for when you get back, a day 22 solution using inclusion-exclusion principle that's nearly as fast as the subtraction solution (30ms vs 45ms); by keeping the seen regions in a map I cut down on a lot of duplication in the list of inclusions and exclusions: https://glguy.net/advent/sln_2021_22/src/Main.html#solveInEx |
All times are in UTC on 2021-12-30.