Logs on 2023-03-01 (liberachat/#haskell)
| 00:00:35 | <ph88> | trying to model it with inspiration from this post https://stackoverflow.com/a/28696299/1833322 |
| 00:02:30 | <ph88> | i think i'm going to throw this code away .. it looks so ugly to making all these names for the data constructors :( |
| 00:04:35 | × | acidjnk_new quits (~acidjnk@p200300d6e715c4929ccd0d51d52c8268.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 00:06:21 | × | xff0x quits (~xff0x@178.255.149.135) (Ping timeout: 255 seconds) |
| 00:06:33 | × | forell quits (~forell@user/forell) (Ping timeout: 252 seconds) |
| 00:07:21 | <geekosaur> | kinda sorry I asked; type level in haskell drives me bonkers. maybe when we have actual dependent haskell… |
| 00:07:50 | → | mauke_ joins (~mauke@user/mauke) |
| 00:08:26 | → | xff0x joins (~xff0x@ai081074.d.east.v6connect.net) |
| 00:09:06 | <mon_aaraj> | i love dependent types! i love idris and agda a lot... but i kind of feel like adding them to haskell is too much, no? |
| 00:09:15 | × | mauke quits (~mauke@user/mauke) (Ping timeout: 248 seconds) |
| 00:09:15 | mauke_ | is now known as mauke |
| 00:10:08 | <mon_aaraj> | the GHC team seems to be biting off more than they can chew already, and I think the language is awesome in all honestly -- we just need huge clean ups or rewrites of the code and some more optimizations |
| 00:10:13 | <ph88> | geekosaur, no worries, thanks for offering help anyway |
| 00:10:31 | <ph88> | mon_aaraj, what do you think of my paste ? is it doable ? |
| 00:10:34 | <hpc> | mon_aaraj: some say haskell has gone too far, but i say it hasn't gone too far enough |
| 00:10:48 | → | forell joins (~forell@user/forell) |
| 00:11:09 | <mon_aaraj> | hpc: haha! you may be right |
| 00:11:36 | <c_wraith> | There are some things that just aren't practical in current Haskell and would be way better with just a couple dependent features. Just having Pi types would allow type classes to vary on values, for instance. |
| 00:11:42 | <mon_aaraj> | i just wish GHC gets way more funding (especially tooling, cabal and ghcup) and more working hands on it (especially the compiler for this) |
| 00:12:40 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 00:13:02 | <c_wraith> | You can sort of fake classes that vary on values using reflection, but reflection is a horrible hack with unsafeCoerce at the core. Not using it makes things much more dependable |
| 00:14:18 | × | Tuplanolla quits (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:14:27 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-212.fiber.dynamic.sonic.net) (Ping timeout: 255 seconds) |
| 00:16:01 | <mon_aaraj> | also -- what's the benefit of encoding all of this in the type system? you can do the type level stuff in the value level rather easily |
| 00:16:37 | <ph88> | c_wraith, what do you think of package singletons ? |
| 00:17:13 | <c_wraith> | ph88: it has some shocking holes in it, like... Float and Double |
| 00:17:20 | <ph88> | hpc, maybe liquid haskell is something you would like to try |
| 00:17:38 | <hpc> | maybe |
| 00:17:59 | <c_wraith> | mon_aaraj: you get to use pre-existing tools like foldMap if you have a Monoid instance available. |
| 00:18:00 | <ph88> | c_wraith, what is missing with float and double ? |
| 00:18:09 | <c_wraith> | ph88: you can't promote them to the type level |
| 00:18:37 | <ph88> | ah ye |
| 00:19:02 | <mon_aaraj> | c_wraith: Ah, sorry. I didn't mean as in response to you, in response to ph88's source code. |
| 00:19:23 | <c_wraith> | Oh, hah. no problem. :) |
| 00:19:29 | <mon_aaraj> | In reality I think it's just not useful to do this at the type level at all. But I'm not really sure why one would do it in the first place |
| 00:19:48 | <mon_aaraj> | * In reality I think it's just not useful to implement this specific thing at the type level at all. But I'm not really sure why one would do it in the first place |
| 00:19:55 | <ph88> | mon_aaraj, i thought it was nice to have type level guarantees .. if only it would work .. |
| 00:20:26 | <ph88> | mon_aaraj, check this presentation for background https://www.lambdadays.org/static/upload/media/1519637389130819oskarwickstromfinitestatemachines_.pdf |
| 00:20:29 | <c_wraith> | ph88: I think you've identified the problem. It would be nice... if it worked. :) |
| 00:20:56 | <ph88> | c_wraith, i am still blaiming it on my own ignorance than compiler limitations :p |
| 00:21:15 | <mon_aaraj> | Meh, doing this at the type level won't really guarantee much for you. It's a lot of work for almost no benefit. You'll still get guarantees from the type system if you implement it at the value level too. |
| 00:21:42 | <mon_aaraj> | You very much _can_ do it, but you shouldn't. Maybe I should find the "you've spent so long thinking about if you could, you've never stopped to think if you should" meme, but I'm too lazy. |
| 00:23:58 | <ph88> | ok i give up |
| 00:25:09 | × | mrcsno quits (~mrcsno@71.69.152.220) (Ping timeout: 255 seconds) |
| 00:27:46 | <hpc> | sometimes instead of making sure you write correct code, you should write correct code instead? |
| 00:34:56 | × | stackdroid18 quits (14094@de1.hashbang.sh) (Quit: hasta la vista... tchau!) |
| 00:36:47 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 00:46:33 | × | zeenk quits (~zeenk@2a02:2f04:a20d:f900::7fe) (Quit: Konversation terminated!) |
| 00:49:16 | × | dextaa quits (~DV@user/dextaa) (Quit: Ping timeout (120 seconds)) |
| 00:52:35 | × | ph88 quits (~ph88@ip5b426553.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 00:54:00 | → | dextaa joins (~DV@user/dextaa) |
| 00:59:16 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 01:02:06 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 01:03:10 | → | califax joins (~califax@user/califx) |
| 01:04:32 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 01:04:32 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 01:04:32 | → | wroathe joins (~wroathe@user/wroathe) |
| 01:05:07 | <mauke> | https://github.com/mauke/mini-mine/blob/main/app/Main.hs I made a small, but unfortunately not tiny, game |
| 01:05:27 | <mauke> | (it's 15 lines, not 10) |
| 01:09:58 | → | thegeekinside joins (~thegeekin@189.180.66.126) |
| 01:10:47 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:13:32 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 01:15:49 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 01:16:27 | × | dextaa quits (~DV@user/dextaa) (Ping timeout: 260 seconds) |
| 01:16:54 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:18:47 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 264 seconds) |
| 01:20:31 | → | dextaa joins (~DV@user/dextaa) |
| 01:22:20 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) |
| 01:26:35 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) (Ping timeout: 248 seconds) |
| 01:30:26 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-212.fiber.dynamic.sonic.net) |
| 01:37:57 | <sm> | nice! might fit in the next jam |
| 01:42:07 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-212.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 01:43:16 | <mauke> | I only started like 5 hours before the deadline, and predictably ran out of time :-) |
| 01:45:44 | × | dextaa quits (~DV@user/dextaa) (Quit: Ping timeout (120 seconds)) |
| 01:48:59 | <sm> | 10 lines can soak up a lot of hours :) |
| 01:50:04 | <davean> | More than 15 lines can! ;) |
| 01:50:12 | → | dextaa joins (~DV@user/dextaa) |
| 01:52:59 | × | thegeekinside quits (~thegeekin@189.180.66.126) (Ping timeout: 264 seconds) |
| 01:53:52 | → | thegeekinside joins (~thegeekin@189.141.115.134) |
| 02:06:15 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 256 seconds) |
| 02:07:10 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Ping timeout: 246 seconds) |
| 02:07:23 | → | kritzefitz joins (~kritzefit@debian/kritzefitz) |
| 02:07:51 | × | xff0x quits (~xff0x@ai081074.d.east.v6connect.net) (Ping timeout: 255 seconds) |
| 02:08:29 | × | czy quits (~user@host-140-25.ilcub310.champaign.il.us.clients.pavlovmedia.net) (Quit: ERC 5.4.1 (IRC client for GNU Emacs 30.0.50)) |
| 02:08:45 | <ddellacosta> | so I am reading about async exceptions and bound threads, and how a thread may not respond if a FFI call is being made. The workaround I'm reading is to spawn the FFI call in an async itself. However, this doesn't actually end the process/FFI call--is there any way to explicitly do that somehow? |
| 02:08:47 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:08:53 | → | czy joins (~user@host-140-25.ilcub310.champaign.il.us.clients.pavlovmedia.net) |
| 02:09:32 | <davean> | No, its not a seperate PROCESS |
| 02:10:21 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Remote host closed the connection) |
| 02:10:21 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-212.fiber.dynamic.sonic.net) |
| 02:10:41 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 02:11:42 | <ddellacosta> | sorry I meant thread instead of process, in the case that you spawn a separate async in the manner I described |
| 02:19:17 | → | pavonia joins (~user@user/siracusa) |
| 02:20:54 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 02:20:56 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 02:22:15 | Lord_of_Life_ | is now known as Lord_of_Life |
| 02:26:22 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 02:29:54 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 02:32:11 | × | Square quits (~Square4@user/square) (Ping timeout: 248 seconds) |
| 02:34:32 | → | dsrt^ joins (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) |
| 02:44:27 | → | opticblast1 joins (~Thunderbi@172.58.85.161) |
| 02:45:39 | × | opticblast quits (~Thunderbi@172.58.82.191) (Ping timeout: 255 seconds) |
| 02:45:40 | opticblast1 | is now known as opticblast |
| 02:47:20 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:55:23 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 264 seconds) |
| 02:57:15 | × | thegeekinside quits (~thegeekin@189.141.115.134) (Ping timeout: 256 seconds) |
| 03:15:10 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 03:18:32 | × | jero98772 quits (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) (Remote host closed the connection) |
| 03:24:33 | → | Everything joins (~Everythin@46.185.124.65) |
| 03:25:00 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 03:25:56 | → | gastus joins (~gastus@185.6.123.208) |
| 03:29:20 | × | gastus_ quits (~gastus@185.6.123.141) (Ping timeout: 268 seconds) |
| 03:30:39 | × | ft quits (~ft@p3e9bc443.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 03:31:53 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) |
| 03:32:34 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 03:35:35 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:35:35 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:35:35 | finn_elija | is now known as FinnElija |
| 03:36:02 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 03:38:09 | × | td_ quits (~td@i5387093D.versanet.de) (Ping timeout: 246 seconds) |
| 03:40:05 | → | td_ joins (~td@i53870923.versanet.de) |
| 03:40:25 | × | slack1256 quits (~slack1256@186.11.13.167) (Remote host closed the connection) |
| 03:41:28 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-212.fiber.dynamic.sonic.net) (Quit: segfaultfizzbuzz) |
| 03:46:28 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 03:48:47 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 264 seconds) |
| 03:58:47 | → | razetime joins (~Thunderbi@117.193.3.64) |
| 04:00:13 | × | shailangsa quits (~shailangs@host165-120-169-78.range165-120.btcentralplus.com) (Ping timeout: 246 seconds) |
| 04:14:21 | × | m5zs7k quits (aquares@web10.mydevil.net) (Ping timeout: 268 seconds) |
| 04:16:20 | → | m5zs7k joins (aquares@web10.mydevil.net) |
| 04:18:40 | × | razetime quits (~Thunderbi@117.193.3.64) (Ping timeout: 252 seconds) |
| 04:21:53 | × | dsrt^ quits (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) (Ping timeout: 246 seconds) |
| 04:22:39 | × | m5zs7k quits (aquares@web10.mydevil.net) (Ping timeout: 260 seconds) |
| 04:25:32 | → | dsrt^ joins (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) |
| 04:25:53 | → | mbuf joins (~Shakthi@49.204.115.87) |
| 04:26:12 | → | jinsun__ joins (~jinsun@user/jinsun) |
| 04:26:12 | × | jinsun quits (~jinsun@user/jinsun) (Killed (platinum.libera.chat (Nickname regained by services))) |
| 04:26:12 | jinsun__ | is now known as jinsun |
| 04:29:19 | × | jle` quits (~jle`@cpe-23-240-75-236.socal.res.rr.com) (Ping timeout: 248 seconds) |
| 04:29:56 | → | m5zs7k joins (aquares@web10.mydevil.net) |
| 04:31:14 | → | jle` joins (~jle`@cpe-23-240-75-236.socal.res.rr.com) |
| 04:33:36 | × | opticblast quits (~Thunderbi@172.58.85.161) (Quit: opticblast) |
| 04:33:49 | → | opticblast joins (~Thunderbi@172.58.82.223) |
| 04:34:43 | × | bliminse_ quits (~bliminse@user/bliminse) (Ping timeout: 256 seconds) |
| 04:35:51 | × | m5zs7k quits (aquares@web10.mydevil.net) (Ping timeout: 256 seconds) |
| 04:36:23 | → | bliminse joins (~bliminse@user/bliminse) |
| 04:38:02 | × | opticblast quits (~Thunderbi@172.58.82.223) (Ping timeout: 255 seconds) |
| 04:38:28 | → | m5zs7k joins (aquares@web10.mydevil.net) |
| 04:39:09 | → | mrcsno joins (~mrcsno@71.69.152.220) |
| 04:41:34 | → | shailangsa_ joins (~shailangs@host165-120-169-78.range165-120.btcentralplus.com) |
| 04:41:37 | × | czy quits (~user@host-140-25.ilcub310.champaign.il.us.clients.pavlovmedia.net) (Read error: Connection reset by peer) |
| 04:42:43 | → | Feuermagier_ joins (~Feuermagi@user/feuermagier) |
| 04:45:14 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Ping timeout: 255 seconds) |
| 04:47:09 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 04:56:34 | × | Vajb quits (~Vajb@2001:999:230:f561:4ee8:ad7f:13ff:9959) (Read error: Connection reset by peer) |
| 04:56:45 | <Axman6> | ddellacosta: I would strongly recommend reading Simon Marlow's Parallel and Concurrent Haskell, there's really no better resource for understanding how exceptions and threading play with each other. |
| 04:56:51 | <Axman6> | @where pcph |
| 04:56:51 | <lambdabot> | "Parallel and Concurrent Programming in Haskell" by Simon Marlow in 2013 at <http://community.haskell.org/~simonmar/pcph/>,<http://chimera.labs.oreilly.com/books/1230000000929/>,<https://web.archive. |
| 04:56:51 | <lambdabot> | org/web/20180117194842/http://chimera.labs.oreilly.com/books/1230000000929>,<https://www.oreilly.com/library/view/parallel-and-concurrent/9781449335939/> |
| 04:56:59 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) |
| 05:02:09 | × | kupi quits (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 05:03:10 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 05:04:04 | × | Feuermagier_ quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 05:04:47 | → | Vajb joins (~Vajb@2001:999:230:f561:4ee8:ad7f:13ff:9959) |
| 05:08:40 | × | polyphem_ quits (~rod@2a02:810d:840:8754:224e:f6ff:fe5e:bc17) (Ping timeout: 252 seconds) |
| 05:09:54 | → | opticblast joins (~Thunderbi@172.58.85.161) |
| 05:10:20 | → | razetime joins (~Thunderbi@117.193.3.64) |
| 05:11:21 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 255 seconds) |
| 05:13:11 | × | johnw quits (~johnw@2600:1700:cf00:db0:90d9:7fcd:a65c:d4b3) (Quit: ZNC - http://znc.in) |
| 05:13:11 | × | jwiegley quits (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
| 05:16:44 | → | cyphase joins (~cyphase@user/cyphase) |
| 05:17:12 | × | ddellacosta quits (~ddellacos@143.244.47.85) (Ping timeout: 246 seconds) |
| 05:35:34 | → | harveypwca joins (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
| 05:37:09 | × | Adran quits (~adran@botters/adran) (Quit: Este é o fim.) |
| 05:39:06 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 05:39:23 | → | califax joins (~califax@user/califx) |
| 05:39:26 | → | ddellacosta joins (~ddellacos@146.70.166.10) |
| 05:40:26 | → | xkuru joins (~xkuru@user/xkuru) |
| 05:45:01 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 05:45:16 | <ddellacosta> | Axman6: that was actually the book I was referencing when I asked the question, chapter 15, the section "Asychronous Exceptions and Foreign Calls." That is where I found the suggestion to make FFI calls using async, but I didn't see anything past that to understand if I can actually some how kill an FFI call somehow. I guess it just passes the same characteristics (not responding to async |
| 05:45:18 | <ddellacosta> | exceptions) on to the new thread that is running the FFI call. I'm probably missing something though. |
| 05:45:54 | → | Adran joins (adran@botters/adran) |
| 05:48:25 | <Axman6> | Well, what does it mean to kill an FFI call in the middle of running? It seems to me like it's more likely to be dangerous than not |
| 05:48:58 | → | JimL joins (~quassel@89-162-26-217.fiber.signal.no) |
| 05:49:25 | <ddellacosta> | I'm trying to run a Lua script in a fairly constrainted context, in multiple concurrent threads as needed, and I want those to be easily interruptible |
| 05:49:39 | × | JimL quits (~quassel@89-162-26-217.fiber.signal.no) (Client Quit) |
| 05:50:01 | <ddellacosta> | but I think I'm going to handle it by ensuring the scripts follow a given format, and try to bypass the problem |
| 05:50:03 | → | JimL joins (~quassel@89-162-26-217.fiber.signal.no) |
| 05:51:16 | → | trev joins (~trev@user/trev) |
| 06:05:48 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 06:07:46 | <Axman6> | Well, it's been a long time since I've read it, so can't really help any more than that, sorry =) |
| 06:10:31 | → | kupi joins (uid212005@id-212005.hampstead.irccloud.com) |
| 06:19:51 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 06:20:17 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 06:31:06 | × | razetime quits (~Thunderbi@117.193.3.64) (Ping timeout: 255 seconds) |
| 06:32:41 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:33:30 | → | johnw joins (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
| 06:34:00 | → | jwiegley joins (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
| 06:38:05 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 06:46:01 | → | michalz joins (~michalz@185.246.207.203) |
| 06:46:50 | <Inst> | what's wrong with tossing {-# INLINE funname #-} everywhere? |
| 06:47:17 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
| 06:47:20 | <Jade[m]1> | it blows up quickly if a function is used in a lot of places I'd assume |
| 06:50:20 | <Inst> | define blows up? |
| 06:51:25 | <Axman6> | i can make code larger, which might make it execute slower. generally small functions should be inlined (and GHC should do that automatically). I'm sure there's a lot of documentation in the GHC manual you can read |
| 06:52:38 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 06:56:07 | <Inst> | yeah, i saw it, i'm just worried because afaik splitting files up into modules stops the inliner from working normally |
| 06:57:11 | × | opticblast quits (~Thunderbi@172.58.85.161) (Quit: opticblast) |
| 06:57:26 | → | opticblast joins (~Thunderbi@172.58.83.235) |
| 06:57:46 | <Inst> | also re: programming is hard, Haskell just doesn't hide it from you, from monochrom: my eyes literally glaze over when I find a file of source code that's over 100-150 lines |
| 06:57:54 | <Inst> | Haskell at least lets me organize everything into neat, separate packages |
| 06:57:59 | <Inst> | erm, neat, separate modules |
| 07:01:14 | <Inst> | i think Haskell, is somehow an easier language than everything else i've been exposed to |
| 07:03:54 | → | theproffesor joins (~theproffe@2601:282:8880:20::351b) |
| 07:03:54 | × | theproffesor quits (~theproffe@2601:282:8880:20::351b) (Changing host) |
| 07:03:54 | → | theproffesor joins (~theproffe@user/theproffesor) |
| 07:06:51 | × | shriekingnoise_ quits (~shrieking@186.137.175.87) (Ping timeout: 248 seconds) |
| 07:08:15 | × | harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
| 07:09:42 | × | Inst quits (~Inst@2601:6c4:4081:54f0:f532:ca97:ac1f:c1cd) (Ping timeout: 255 seconds) |
| 07:10:14 | → | Inst joins (~Inst@2601:6c4:4081:54f0:7069:999c:7e48:ff3b) |
| 07:30:23 | × | opticblast quits (~Thunderbi@172.58.83.235) (Ping timeout: 256 seconds) |
| 07:30:34 | × | lagash_ quits (lagash@lagash.shelltalk.net) (Ping timeout: 246 seconds) |
| 07:31:40 | → | lagash_ joins (lagash@lagash.shelltalk.net) |
| 07:33:55 | × | johnw quits (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
| 07:34:16 | → | johnw joins (~johnw@2600:1700:cf00:db0:a85a:aa58:c54c:551d) |
| 07:36:37 | × | mjrosenb quits (~mjrosenb@pool-96-232-177-77.nycmny.fios.verizon.net) (Ping timeout: 268 seconds) |
| 07:37:09 | → | mjrosenb joins (~mjrosenb@pool-96-232-177-77.nycmny.fios.verizon.net) |
| 07:38:56 | → | kenran joins (~user@user/kenran) |
| 07:43:38 | → | gurkenglas joins (~gurkengla@dynamic-046-114-179-219.46.114.pool.telefonica.de) |
| 07:48:39 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 07:50:17 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 255 seconds) |
| 07:52:31 | → | gmg joins (~user@user/gehmehgeh) |
| 07:53:56 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 07:54:17 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 07:56:03 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:1fc4:7ac2:9c57:911) |
| 07:57:21 | → | ft joins (~ft@p3e9bc443.dip0.t-ipconnect.de) |
| 08:02:13 | → | kenran` joins (~user@user/kenran) |
| 08:04:14 | → | zephyr__ joins (~irfan@106.214.197.187) |
| 08:04:22 | × | kenran quits (~user@user/kenran) (Ping timeout: 268 seconds) |
| 08:12:50 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:20:26 | → | MajorBiscuit joins (~MajorBisc@c-001-028-045.client.tudelft.eduvpn.nl) |
| 08:28:48 | × | ft quits (~ft@p3e9bc443.dip0.t-ipconnect.de) (Quit: leaving) |
| 08:29:41 | → | akegalj joins (~akegalj@93-137-60-213.adsl.net.t-com.hr) |
| 08:35:01 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) (Remote host closed the connection) |
| 08:37:19 | → | acidjnk_new joins (~acidjnk@p200300d6e715c4099ccd0d51d52c8268.dip0.t-ipconnect.de) |
| 08:40:35 | × | lagash_ quits (lagash@lagash.shelltalk.net) (Ping timeout: 255 seconds) |
| 08:44:12 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 08:46:59 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 255 seconds) |
| 08:49:01 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 08:50:57 | × | MajorBiscuit quits (~MajorBisc@c-001-028-045.client.tudelft.eduvpn.nl) (Ping timeout: 255 seconds) |
| 08:55:26 | → | MajorBiscuit joins (~MajorBisc@2001:1c00:2408:a400:67e:5371:52a7:9b9a) |
| 08:56:59 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 08:57:10 | → | lagash joins (lagash@2605:6400:20:b4:9c76:1538:3398:ce71) |
| 09:03:04 | → | the_proffesor joins (~theproffe@2601:282:8880:20:bb29:952e:2032:246f) |
| 09:03:04 | × | the_proffesor quits (~theproffe@2601:282:8880:20:bb29:952e:2032:246f) (Changing host) |
| 09:03:04 | → | the_proffesor joins (~theproffe@user/theproffesor) |
| 09:03:09 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 09:07:02 | → | nschoe joins (~q@141.101.51.197) |
| 09:07:23 | × | theproffesor quits (~theproffe@user/theproffesor) (Ping timeout: 248 seconds) |
| 09:10:18 | × | kupi quits (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:12:52 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:15:38 | → | chele joins (~chele@user/chele) |
| 09:19:38 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 09:21:04 | × | remexre quits (~remexre@user/remexre) (Read error: Connection reset by peer) |
| 09:21:15 | → | remexre joins (~remexre@user/remexre) |
| 09:21:42 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 09:22:08 | → | califax joins (~califax@user/califx) |
| 09:23:59 | → | fserucas joins (~fserucas@2001:818:e376:a400:fb92:70c1:dd88:c7d7) |
| 09:24:00 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.8) |
| 09:24:27 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 248 seconds) |
| 09:26:36 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 09:34:19 | × | wagle quits (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 09:34:50 | → | wagle joins (~wagle@quassel.wagle.io) |
| 09:35:33 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) |
| 09:36:28 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 09:39:41 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) (Ping timeout: 246 seconds) |
| 09:42:34 | <cheater> | hi |
| 09:42:50 | <zephyr__> | hello |
| 09:43:44 | <cheater> | how could i modify the method echo'echo in instance Echo'server_ MyEchoServer so that it increments a TVar without forgetting it between calls? echo'echo is IO () but I just don't know how I would initialize / pass a TVar into this https://hackage.haskell.org/package/capnp-0.17.0.0/docs/Capnp-Tutorial.html#g:1 |
| 09:47:31 | <cheater> | what do i do, stuff the TVar in an IORef or something? |
| 09:48:37 | <mauke> | that's a tutorial link |
| 09:48:53 | <cheater> | yes, it is |
| 09:49:00 | <cheater> | what are you trying to say |
| 09:49:01 | × | phma quits (phma@2001:5b0:215a:9618:c34:315f:ca7c:13ac) (Read error: Connection reset by peer) |
| 09:49:21 | <mauke> | how do you pass variables into tutorials |
| 09:49:33 | <zephyr__> | cheater: you'd need to pass the `TVar` reference as an argument. |
| 09:49:55 | → | phma joins (phma@2001:5b0:211f:30c8:d195:4c3:ddc4:3351) |
| 09:50:22 | <cheater> | pass it how? look how the server is started inside of main - there's no call to the actual function echo'ech |
| 09:50:28 | <cheater> | echo'echo |
| 09:50:59 | <mauke> | there are 10 mains on that page |
| 09:51:04 | [exa] | can't help it but echo'echo sounds too much like 'allo'allo and I like it for servers |
| 09:51:06 | <mauke> | where are we? |
| 09:51:11 | <cheater> | getBootstrap = \sup -> Just . toClient <$> export @Echo sup MyEchoServer |
| 09:51:22 | × | MajorBiscuit quits (~MajorBisc@2001:1c00:2408:a400:67e:5371:52a7:9b9a) (Ping timeout: 252 seconds) |
| 09:51:28 | <cheater> | mauke: read again what i said. i mention the function name. |
| 09:51:38 | <zephyr__> | cheater: maybe have a global `TVar`, then. |
| 09:51:46 | <mauke> | ah, under RPC: https://hackage.haskell.org/package/capnp-0.17.0.0/docs/Capnp-Tutorial.html#g:10 |
| 09:51:47 | <cheater> | how do you have a global TVar? |
| 09:53:31 | → | MajorBiscuit joins (~MajorBisc@c-001-028-045.client.tudelft.eduvpn.nl) |
| 09:55:08 | <mauke> | I haven't seen this library before, but my first instinct would be to embed it in the MyEchoServer type. no idea if that's sensible |
| 09:55:36 | <cheater> | i don't think it is |
| 09:57:29 | <cheater> | idk how |
| 09:57:32 | <cheater> | how would you do that mauke |
| 09:59:13 | <mauke> | https://github.com/zenhack/haskell-capnp/blob/master/examples/lib/Examples/Rpc/CalculatorServer.hs#L49-L60 |
| 09:59:26 | <mauke> | like this example, which stores a function |
| 09:59:34 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Remote host closed the connection) |
| 10:00:12 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 10:01:17 | <zephyr__> | cheater: does this work? |
| 10:01:19 | <zephyr__> | cheater: https://paste.tomsmeding.com/ZZV87ly7 |
| 10:01:50 | → | CiaoSen joins (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 10:02:13 | <gurkenglas> | Recommend a repository of strange/arcane uses of Haskell's type system? |
| 10:02:21 | <int-e> | zephyr__: add {-# NOINLINE t #-} and it probably works |
| 10:02:26 | → | teo joins (~teo@user/teo) |
| 10:02:40 | <zephyr__> | int-e: yeah, thanks |
| 10:02:51 | <cheater> | why NOINLINE? |
| 10:03:11 | <int-e> | cheater: imagine what the code looks like if both uses of t get inlined |
| 10:03:14 | <zephyr__> | cheater: you don't want to create a new TVar again and again, i think |
| 10:03:27 | <cheater> | oh yeah |
| 10:03:33 | <cheater> | mauke: i'm still reading your link |
| 10:03:48 | → | razetime joins (~Thunderbi@117.193.3.64) |
| 10:03:58 | <zephyr__> | cheater: you might not be comfortable with unsafePerformIO but it's a global TVar so you don't need to pass an argument to echo'echo |
| 10:04:14 | <cheater> | i'm comfortable ish |
| 10:04:44 | <mauke> | but echo'echo already takes an argument of user-defined type, so you can pass in whatever you like, no? |
| 10:05:12 | <zephyr__> | isn't echo'echo just `IO ()`, cheater? |
| 10:05:36 | <cheater> | mauke: it does? idk that it does |
| 10:05:38 | <zephyr__> | sorry, if there's a possibility to pass arguments, then that's the better solution. |
| 10:05:44 | <cheater> | zephyr__: yes, it's IO () |
| 10:05:46 | <zephyr__> | i believe |
| 10:06:53 | <mauke> | cheater: the first argument |
| 10:06:54 | <cheater> | class (Echo'server_ s_) where { ... echo'echo :: s_ -> (GH.MethodHandler Echo'echo'params Echo'echo'results); echo'echo _ = GH.methodUnimplemented } |
| 10:07:02 | <mauke> | s_ |
| 10:07:06 | <mauke> | that's your type |
| 10:07:22 | <cheater> | it also has an un-implementation |
| 10:07:26 | × | koz quits (~koz@121.99.240.58) (Ping timeout: 255 seconds) |
| 10:07:55 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 256 seconds) |
| 10:08:17 | <cheater> | so in my instance, it looks like this: |
| 10:08:39 | <cheater> | instance Echo'server_ MyEchoServer where { echo'echo MyEchoServer ... } |
| 10:08:45 | <cheater> | sorry i meant |
| 10:08:48 | <cheater> | instance Echo'server_ MyEchoServer where { echo'echo MyEchoServer = ... } |
| 10:09:00 | <cheater> | so yeah that's the constructor being passed |
| 10:09:10 | <cheater> | so i could put stuff inside the data definition i guess? like you said? |
| 10:09:22 | <cheater> | currently it's data MyEchoServer = MyEchoServer |
| 10:09:32 | <mauke> | yeah |
| 10:09:40 | <cheater> | but i could make it like data MyEchoServer = MyEchoServer { counter :: TVar Integer } |
| 10:09:59 | <cheater> | and then in the main function instead of saying |
| 10:09:59 | <cheater> | , getBootstrap = \sup -> Just . toClient <$> export @Echo sup MyEchoServer |
| 10:10:30 | <cheater> | i could say , getBootstrap = \sup -> Just . toClient <$> export @Echo sup (MyEchoServer myTvar ) |
| 10:10:36 | <mauke> | right, that's what I was thinking of |
| 10:10:41 | <cheater> | gotcha |
| 10:10:51 | <cheater> | i could try that. saves us a global reference |
| 10:11:24 | <zephyr__> | sure, thanks mauke |
| 10:11:30 | <cheater> | see for some reason when i was looking at that getBootstrap line i thought that MyEchoServer was a syntactic reference to the type, not to the constructor |
| 10:11:35 | <gurkenglas> | int-e: how can I find more exercises like the (forall x. x a -> x b -> x c) -> Either (forall x. x a -> x c) (forall x. x b -> x c) one I came up with recently? |
| 10:11:47 | <cheater> | we need like a third case that's between lower case and upper case |
| 10:12:23 | <cheater> | that's what will bring on the year of the Haskell desktop |
| 10:15:57 | <int-e> | gurkenglas: I don't know, I found the last one by being on #haskell and reading one of your messages. |
| 10:16:09 | × | mud quits (~mud@user/kadoban) (Remote host closed the connection) |
| 10:16:14 | → | koz joins (~koz@121.99.240.58) |
| 10:16:35 | → | mud joins (~mud@user/kadoban) |
| 10:20:02 | <Inst> | god, I love Haskell |
| 10:20:12 | <cheater> | nice |
| 10:20:17 | <Inst> | I have no freaking clue what I'm doing, just copy-pasting code from an old project |
| 10:21:05 | <Inst> | got an 8x speed-up |
| 10:21:22 | <Inst> | just by doing a trivial refactor to exploit mapconcurrently because I can't figure out how to get Eval monad to work properly |
| 10:23:01 | <Inst> | that said, i'm doing old and crappy parallel code, i sprung a space leak ;_; |
| 10:23:35 | <Inst> | https://cdn.discordapp.com/attachments/968989726633779215/1080435068591407165/image.png |
| 10:24:16 | <Inst> | 85% spark conversion rate, hahahaha |
| 10:24:18 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 10:24:22 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 10:25:33 | <Inst> | crap no, i'm out of memory. ffff |
| 10:25:39 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 10:27:56 | <int-e> | Wow, that's a 15% spark fizzle rate. Lots of duds... |
| 10:28:19 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 10:29:19 | <int-e> | Oh, why are some of them getting GC'd? Are you `par`-ing values that you don't need? |
| 10:29:29 | <Inst> | ;_; |
| 10:29:36 | <Inst> | i was told this was good! |
| 10:30:25 | <int-e> | And I missed that there's an actual "dud" statistic, I wonder what the ghc folks think a dud is. |
| 10:30:51 | <Inst> | "when rpar is applied to an expression that is already evaluated, this is considered a dud and the rpar is ignored" |
| 10:31:40 | <Inst> | ugh, it's probably the overuse of state |
| 10:31:53 | <int-e> | `par` is good if the value will be needed and computing it isn't instantaneous; there's some overhead in managing sparks. Basically they're added to a queue and idle threads look for items on that queue to evaluate. |
| 10:32:14 | → | ubert1 joins (~Thunderbi@2a02:8109:abc0:6434:64ad:38c9:a22a:dbbb) |
| 10:32:47 | <Inst> | halp |
| 10:32:59 | <Inst> | recompile with all the puts in StateT strict made strict? |
| 10:33:00 | <Inst> | https://media.discordapp.net/attachments/968989726633779215/1080437435760128040/image.png |
| 10:36:24 | → | shryke joins (~shryke@2a00:4b00:13c:cc:b27b:25ff:fe18:efd) |
| 10:36:37 | → | Midjak joins (~Midjak@82.66.147.146) |
| 10:37:37 | <int-e> | Inst: If you suspect that a non-strict state is the culprit (plausible), there's Control.Monad.State.Strict |
| 10:39:15 | <Inst> | I'm already on Control.Monad.State.Strict! ugh!!!! |
| 10:39:27 | <Inst> | import Control.Monad.Trans.State.Strict (StateT, gets, get, put) |
| 10:40:00 | <int-e> | Well, then a non-strict state isn't your issue. It might still be a non-strict component of your state if it's a record. |
| 10:40:23 | <int-e> | This kind of thing is impossible to figure out without code. |
| 10:40:58 | → | king_gs joins (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) |
| 10:42:20 | <Inst> | unfortunately, the code isn't really readable |
| 10:42:45 | <Inst> | https://paste.tomsmeding.com/PzLh1rkF |
| 10:43:39 | <Inst> | i'm blaming mapConcurrently |
| 10:43:49 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 10:44:12 | <Inst> | tbh might be better to redo and try again, but with Vector instead of List |
| 10:47:24 | <Inst> | still leaking with vector and bang patterns slapped over most of the place, but acceptable rate, roughly 100kb per second this time |
| 10:47:32 | × | razetime quits (~Thunderbi@117.193.3.64) (Remote host closed the connection) |
| 10:49:56 | × | xkuru quits (~xkuru@user/xkuru) (Quit: Unvirtualizing) |
| 10:50:48 | → | xkuru joins (~xkuru@user/xkuru) |
| 10:51:22 | × | xkuru quits (~xkuru@user/xkuru) (Remote host closed the connection) |
| 10:51:32 | × | fnurglewitz quits (uid263868@id-263868.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:51:54 | → | xkuru joins (~xkuru@user/xkuru) |
| 10:52:34 | × | xkuru quits (~xkuru@user/xkuru) (Remote host closed the connection) |
| 10:52:47 | <tomsmeding> | possibly relevant: https://www.well-typed.com/blog/2020/09/nothunks/ |
| 10:52:58 | → | xkuru joins (~xkuru@user/xkuru) |
| 10:56:14 | × | xkuru quits (~xkuru@user/xkuru) (Read error: Connection reset by peer) |
| 10:56:43 | × | tubogram44 quits (~tubogram@user/tubogram) (Quit: Ping timeout (120 seconds)) |
| 10:57:01 | <kuribas> | meh, I was discussing how we could leverage stream fusion to get well performing time series computations at the fraction of the cost and with lower error rate than doing it in java, and all I get is that I am "an evangelist", and that I shouldn't look down on java programmers. |
| 10:57:01 | → | tubogram44 joins (~tubogram@user/tubogram) |
| 10:57:15 | × | acidjnk_new quits (~acidjnk@p200300d6e715c4099ccd0d51d52c8268.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 10:57:20 | <kuribas> | How I claiming that one programming language is better suited for a problem than another "looking down"? |
| 10:57:37 | <kuribas> | Then couldn't we write everything in assembly language? |
| 10:58:13 | <tomsmeding> | kuribas: would it be possible to put stream fusion rules in a java streaming library |
| 10:58:32 | <kuribas> | tomsmeding: at the expense of a lot of complexity, maybe... |
| 10:58:37 | <tomsmeding> | yes |
| 10:58:42 | <tomsmeding> | but reusable complexity, possibly |
| 10:58:56 | → | cfricke joins (~cfricke@user/cfricke) |
| 10:59:00 | <kuribas> | something was done by Oleg I remember... |
| 10:59:38 | <kuribas> | But java streams doesn't have the same performance as haskell stream fusion IIRC. |
| 10:59:55 | <kuribas> | I should do a study, benchmarking a solution in java, haskell, and clojure. |
| 11:00:00 | <kuribas> | And present it. |
| 11:00:33 | × | akegalj quits (~akegalj@93-137-60-213.adsl.net.t-com.hr) (Quit: leaving) |
| 11:01:26 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Remote host closed the connection) |
| 11:01:50 | <hellwolf[m]> | When push comes to the shove, would you prefer the 2-3x performance or elegant and maintainable code? |
| 11:01:51 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 11:01:54 | <hellwolf[m]> | (Just curious) |
| 11:02:04 | <kuribas> | hellwolf[m]: me, or the company? |
| 11:02:14 | <hellwolf[m]> | * (Yes, loaded question, I am just curious) |
| 11:02:22 | <kuribas> | Of course I prefer maintainable over 2-3x performance. |
| 11:02:40 | <hellwolf[m]> | how about you and your own company |
| 11:03:20 | <kuribas> | I can write a super optimized SIMD version in 20x the time I write the haskell. |
| 11:03:24 | <kuribas> | With twice the bugs. |
| 11:03:36 | <kuribas> | And segmentation faults as added bonus. |
| 11:03:43 | <kuribas> | hellwolf[m]: I am an employee |
| 11:04:14 | <gurkenglas> | int-e: I guessed as much, I had just hoped from your initial confidence against is solubility and eventual elegance of solution that you might have seen similar situations elsewhere :D |
| 11:04:53 | <gurkenglas> | If I were asked this, the best I could point the asker at is to read edward kmett's Kan extensions module |
| 11:06:59 | <gurkenglas> | (which I say with the ulterior motive of showing that I'm desperate enough to look even for answers that matches my question that little) |
| 11:07:00 | <hellwolf[m]> | I am asking everyone... |
| 11:07:00 | <hellwolf[m]> | And in the case of edward kmett code: `read ~= be shocked about|be awed at|be confused of|in perpetual denial with` |
| 11:07:27 | × | V quits (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 11:07:54 | × | jinsl- quits (~jinsl@2408:8207:2558:e50:211:32ff:fec8:6aea) (Quit: ZNC - https://znc.in) |
| 11:08:05 | → | jinsl joins (~jinsl@2408:8207:2558:e50:211:32ff:fec8:6aea) |
| 11:08:12 | → | xff0x joins (~xff0x@ai081074.d.east.v6connect.net) |
| 11:08:12 | <kuribas> | hellwolf[m]: just get a PHD in category theory, problem solved! |
| 11:08:54 | → | V joins (~v@ircpuzzles/2022/april/winner/V) |
| 11:09:01 | <hellwolf[m]> | How to decompose the meaning of a word in a human uttered sentence? Use Yoneda lemma and enumerate all the iso-emotions evoked by the word. |
| 11:09:22 | <kuribas> | ask chatGPT? |
| 11:09:26 | <hellwolf[m]> | kuribas: Got it. See you in 20 years! |
| 11:11:09 | <gurkenglas> | hellwolf[m]: elegant! the time for 2-3x performance is when you have all of 1. you're working on the core loop of the code 2. you're actually bottlenecked on compute 3. you can't throw 25% of coder salary at the compute problem to make it go away |
| 11:11:49 | <gurkenglas> | hellwolf[m]: scratch the iso, yoneda is oriented |
| 11:12:23 | <kuribas> | This, it should be demonstrated that the 2x gain by not using stream fusion is actually having a benifit on the system, like it isn't swamped by IO. |
| 11:12:55 | <cheater> | make zephyr__ putting stuff in the record worked thanks |
| 11:13:07 | <cheater> | mauke |
| 11:13:14 | <cheater> | sorry :) :) |
| 11:13:18 | → | acidjnk_new joins (~acidjnk@p200300d6e715c409795fa7f63fedb700.dip0.t-ipconnect.de) |
| 11:13:45 | <hellwolf[m]> | > One observer described the solution as “cute but not extensible” (para-phrasing);... (full message at <https://libera.ems.host/_matrix/media/v3/download/libera.chat/2c96a99ecae09a7e1833c20a6dcd7481d0f5e45d>) |
| 11:13:46 | <lambdabot> | <hint>:1:40: error: lexical error at character 'c' |
| 11:15:24 | <gurkenglas> | Is there a searchable or downloadable version of https://ircbrowse.tomsmeding.com/browse/lchaskell ? |
| 11:16:49 | <gurkenglas> | oh, https://github.com/tomsmeding/ircbrowse says how to set up the db |
| 11:18:38 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 11:19:01 | <mon_aaraj> | the gitlab milestone page for ghc 9.6 says it's gonna be released today (or was it yesterday?), is it in any way accurate? |
| 11:21:31 | × | king_gs quits (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) (Remote host closed the connection) |
| 11:21:51 | → | king_gs joins (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) |
| 11:22:42 | <merijn> | Maybe? :p |
| 11:23:08 | <tomsmeding> | gurkenglas: I still need to add search to that :p |
| 11:23:37 | → | Guest11 joins (~Guest11@c83-251-160-169.bredband.tele2.se) |
| 11:23:46 | <tomsmeding> | setting it up locally kinda works, instructions might be kinda outdated (I revived the project from a semi-forgotten state) |
| 11:23:55 | <Guest11> | I'm so freaking confused, are there any haskell libraries that implements FRP correctly or not? |
| 11:24:08 | <merijn> | Guest11: Define "implement", "FRP", and "correctly" :) |
| 11:24:17 | <Guest11> | Right, that's where I have been |
| 11:24:19 | <Guest11> | lol |
| 11:24:41 | <Guest11> | So according to Eliott, there's a clear meaning, but no library is true to it? |
| 11:24:50 | <Guest11> | Elliott* |
| 11:24:51 | <merijn> | Guest11: That sounds likely |
| 11:25:07 | <Jade[m]1> | what is FRP |
| 11:25:25 | <Guest11> | Google it, there are *loads* of explanations |
| 11:25:33 | <merijn> | Guest11: Essentially, FRP is a semantics, that is "a description of what something means" without definition of *how to achieve that* |
| 11:26:17 | <Guest11> | So am I to give up until there is a correct one, or what? I'm semi-new to haskell, but is interested in the subject of FRP. |
| 11:26:28 | <merijn> | Guest11: So if you look at Conal's papers he gives you the semantics of Behaviour, Event, etc. but "implementing those semantics in a way that doesn't suck" is an exercise for the reader (well, stuff like Push-Pull FRP talks a bit about how to implement things) |
| 11:27:30 | <merijn> | Guest11: Well, there's basically 2 axes to look at "how far does this library deviate from the semantics described?" and "how poorly does it perform?" and atm there seems to be a trade-off between those two (i.e. more correct versions suffer performance issues due to time leaks) |
| 11:27:41 | <Guest11> | I mean, I really want to get some hands on experience on anything. FRP seems like a really interesting rabbit hole. Will you please just give me some direction, as you seem experienced? |
| 11:28:02 | <merijn> | tbh, I haven't touched FRP in nearly a decade, so I don't really know what's new atm |
| 11:28:40 | <merijn> | Thinking about it, something like FRP for FPGA's could be cool :> |
| 11:29:13 | <hellwolf[m]> | I can't stop myself to plug this, I have an alternative FRP application, applied to money/payment :) Actually the production system (which is before I discover it is basically FRP applied to money) is live. |
| 11:29:34 | <Guest11> | i was JUST thinking about applying FRP to money/payments. Interesting! |
| 11:29:48 | <hellwolf[m]> | We processed 80M$ (well, "money") cumulatively so far. |
| 11:30:05 | <Guest11> | What do you mean by "alternative"? |
| 11:30:29 | <hellwolf[m]> | It is not an application that is mentioned anywhere, including on Wikipedia |
| 11:30:54 | → | __monty__ joins (~toonn@user/toonn) |
| 11:30:59 | <hellwolf[m]> | "not commonly", I should say, I have done quite a bit of digging |
| 11:31:54 | <Guest11> | Sounds mysterious. I just want hop on a journey with haskell so I can get experienced, should I just shoot my shot at, say, Yampa? |
| 11:32:31 | <hellwolf[m]> | It's actually wide open, I just haven't found my audience about its FRP angle yet :) |
| 11:32:51 | <hellwolf[m]> | https://github.com/superfluid-finance/protocol-monorepo/tree/semantic-money/packages/spec-haskell/pkgs/semantic-money |
| 11:32:54 | <jackdk> | Guest11: http://joeyh.name/blog/entry/my_haskell_controlled_offgrid_fridge/ is something I remember from the past |
| 11:34:04 | <Guest11> | That was an interesting read! |
| 11:34:13 | <hellwolf[m]> | Live system is at : app.superfluid.finance/ |
| 11:34:13 | <hellwolf[m]> | Enough of my shameless plug, happy to be DM-ed if you want to discuss more |
| 11:34:15 | × | MasseR46 quits (thelounge@2001:bc8:47a0:1521::1) (Quit: The Lounge - https://thelounge.chat) |
| 11:34:23 | <dminuoso_> | merijn: From everything I have seen, FRP certainly seems cool on an idealistic level, but its far from practical. While I can see if you have a team of dedicated specialist you can build things with reflex, I think it sets for an extremely high bar. |
| 11:34:35 | <Guest11> | Massive! I'll take a look! hellwolf[m] |
| 11:34:55 | → | MasseR46 joins (thelounge@2001:bc8:47a0:1521::1) |
| 11:35:38 | <jackdk> | dminuoso_: ISTM that a lot of it is "how do I organise code?" because there's comparatively little folklore. (On top of the abstractions being somehow both simple and hard to grok) |
| 11:40:46 | → | mmhat joins (~mmh@p200300f1c7046216ee086bfffe095315.dip0.t-ipconnect.de) |
| 11:42:08 | × | mmhat quits (~mmh@p200300f1c7046216ee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 11:43:16 | × | king_gs quits (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) (Remote host closed the connection) |
| 11:43:36 | → | king_gs joins (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) |
| 11:44:31 | <gurkenglas> | Is there a free theorem generator that golfs its output by skipping type signatures that could be rederived from context? |
| 11:48:04 | <gurkenglas> | Once one has seen enough examples of free theorems, is it obvious what the free theorem for any given type would be? |
| 11:48:57 | <mon_aaraj> | I love FRP. It's genuinely one of the most interesting pieces of engineering I've seen on haskell |
| 11:49:32 | <Guest11> | Which library have you preferred, and why? |
| 11:49:32 | <Axman6> | does reflex count as FRP? |
| 11:49:47 | <Guest11> | That's kind of my question, does any library cohere to true FRP? |
| 11:49:56 | <gurkenglas> | I can imagine that they end up "you can thread a function through each usage of a free variable before or after" and then one can prove a precise phrasing of "therefore free theorems are useless" |
| 11:49:58 | <Axman6> | almost certainly not |
| 11:50:10 | <hellwolf[m]> | Would love to learn more about: what is true FRP? |
| 11:50:17 | <cheater> | i thought there was some front end stuff that did frp |
| 11:50:41 | <Guest11> | I'm 8 months into Haskell, I don't believe I'm qualified to answer any questions at all yet lol |
| 11:50:46 | <gurkenglas> | but i'd like to know precisely what kind of useless, or equivalently precisely what class of statements they can express |
| 11:50:52 | <mon_aaraj> | Axman6: Yep. |
| 11:51:10 | <Guest11> | How do you guys @ people? |
| 11:51:10 | <mon_aaraj> | Guest11: dunai, and I don't think there's any competition |
| 11:51:21 | <gurkenglas> | s/free variable/bound variable/ :( |
| 11:51:22 | <Guest11> | Oh really, interesting! |
| 11:51:29 | <mon_aaraj> | er, I'm not on IRC - I'm replying to messages on Matrix. |
| 11:52:14 | <mon_aaraj> | hellwolf[m]: You should read conal's blog, conal's stackoverflow, and look up "denotative continuous time programming" |
| 11:52:44 | <mon_aaraj> | Guest11: Never the less, you can just type their username and they should be notified. |
| 11:52:45 | <Inst> | wait, curious |
| 11:52:48 | <Axman6> | Guest11: you just say their name, usually suffixed with : if it's the beginning of the message |
| 11:52:56 | <Axman6> | see ^ |
| 11:52:57 | <Inst> | can you store a function in an IORef? |
| 11:53:02 | <Axman6> | yes |
| 11:53:09 | <Inst> | does that do anything, or is it worthless? |
| 11:53:09 | <Guest11> | Axman6: Test |
| 11:53:09 | <hellwolf[m]> | I read the original paper, hugely inspired by it. And hence realized what I have been doing is FRP but for different domain |
| 11:53:17 | <Axman6> | pass |
| 11:53:22 | <hellwolf[m]> | But what is true frp... |
| 11:53:43 | <mon_aaraj> | by the words of conal -- denotative continuous time programming |
| 11:53:47 | <mon_aaraj> | shortened to DCTP |
| 11:53:49 | <Axman6> | Hmm, conal isn't in here at the moment, I wonder when he was around last |
| 11:54:00 | <Inst> | i'm having a big issue with a memory leak, probably related to a specific function, in part because quite a few of its arguments are truly enormous entities |
| 11:54:22 | <mon_aaraj> | I wasn't quoting him from this Matrix room, just from texts I've seen him write online |
| 11:55:17 | <Guest11> | See this thread, in which Conal says which libraries should be considered true FRP, lol: https://twitter.com/conal/status/532683685003141120 |
| 11:55:19 | <hellwolf[m]> | maybe an example of an implementation that violates that definition would be more concrete for the discussion |
| 11:55:26 | <Axman6> | I mean he used to be in the IRC channel fairly regularly |
| 11:56:51 | <merijn> | He still shows up occasionally |
| 11:57:20 | <hellwolf[m]> | ah, yes, "not even wrong" is the key phrase |
| 11:57:49 | <hellwolf[m]> | I think Conal moved to Agda camp and wanting the denotational spec entirely in Agda :) |
| 11:58:11 | <Axman6> | Inst: there's nothing special about IORefs, they don't force evaluation or anything, they are literally a pointer to a heap object |
| 11:58:16 | <hellwolf[m]> | I have been trying to catch up but... |
| 11:58:21 | <Axman6> | which could be a thunk |
| 11:58:40 | <Inst> | thanks |
| 11:58:47 | <Inst> | sigh, i can't get the profiler to work either |
| 12:02:03 | ← | zephyr__ parts (~irfan@106.214.197.187) () |
| 12:03:00 | <Inst> | probably cabal clean, but giving it a shot |
| 12:03:09 | <Inst> | under the current performance situation |
| 12:03:09 | <mon_aaraj> | <hellwolf[m]> "I think Conal moved to Agda camp..." <- That would make sense. |
| 12:04:02 | <Inst> | http://conal.net/cv.pdf |
| 12:04:03 | <Inst> | huh |
| 12:04:11 | <Inst> | looks like he got shook out with Tikhon at Target? |
| 12:04:12 | <hellwolf[m]> | mon_aaraj: It does, it just means many folks like me need more time to catch up with the state of the art |
| 12:05:50 | <hellwolf[m]> | https://github.com/conal/Collaboration |
| 12:05:50 | <hellwolf[m]> | I have been through a few sessions of his. It's worth it and recommend everyone to contact him if you are up for a shaking up of your belief system too :) |
| 12:06:28 | <Guest11> | Wait, just like that? |
| 12:06:52 | <gurkenglas> | it seems silly that the parametricity theorem talks about relations rather than functions. what prevents us from saying it in terms of functions? |
| 12:08:05 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:1fc4:7ac2:9c57:911) (Ping timeout: 246 seconds) |
| 12:11:07 | <Inst> | there we go, cabal configure --enable-profiling, then rebuild |
| 12:12:27 | <hellwolf[m]> | there is only categories, objects and morphisms. Function is rather a special type of morphism built on top of a category, e.g. Husk. |
| 12:13:24 | <Axman6> | the podcast he did a few months ago was excellent |
| 12:13:42 | <Axman6> | Hask is just a Husk of a category |
| 12:13:51 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 12:14:27 | <hellwolf[m]> | Only Agda people cares about the bottoms now :) Haskellers have submitted to them. |
| 12:15:37 | <Axman6> | https://www.typetheoryforall.com/2022/05/09/17-The-Lost-Elegance-of-Computation-(Conal-Elliott).html#1fe23b61 |
| 12:15:58 | → | infinity0 joins (~infinity0@pwned.gg) |
| 12:26:58 | → | bontaq joins (~user@ool-45779fe5.dyn.optonline.net) |
| 12:35:12 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 12:35:19 | <gurkenglas> | hellwolf[m]: shiny! i've emailed the guy, i do have this CT insight I'd like to formalize. |
| 12:35:37 | <gurkenglas> | how long can I expect to wait for the first session? |
| 12:36:55 | <hellwolf[m]> | In my experience, fairly quickly :) |
| 12:37:04 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 12:37:31 | <gurkenglas> | are we talking minutes or hours or days :P |
| 12:39:28 | <hellwolf[m]> | I don't know, but I just found out he's been working on this: https://github.com/conal/felix |
| 12:39:29 | <hellwolf[m]> | We could stalk his work while waiting. |
| 12:40:06 | <gurkenglas> | pfft looks like if this were paid, he should be paying me |
| 12:40:24 | <hellwolf[m]> | heh, no no, I don't think so. |
| 12:41:09 | × | swistak quits (~swistak@185.21.216.141) (Quit: bye bye) |
| 12:41:21 | × | king_gs quits (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) (Ping timeout: 255 seconds) |
| 12:42:29 | × | melonai quits (~mel@rnrd.eu) (Quit: ZNC 1.8.2 - https://znc.in) |
| 12:42:45 | → | melonai joins (~mel@rnrd.eu) |
| 12:42:57 | → | lyle joins (~lyle@104.246.145.237) |
| 12:43:43 | × | mud quits (~mud@user/kadoban) (Remote host closed the connection) |
| 12:43:43 | × | Cheery quits (~cheery@server-239-7.tentacle.cloud) (Ping timeout: 268 seconds) |
| 12:43:44 | × | tureba quits (~tureba@tureba.org) (Ping timeout: 268 seconds) |
| 12:43:58 | × | simpleauthority quits (~simpleaut@user/simpleauthority) (Quit: ZNC 1.8.2 - https://znc.in) |
| 12:44:09 | → | mud joins (~mud@user/kadoban) |
| 12:44:13 | → | Cheery joins (~cheery@server-239-7.tentacle.cloud) |
| 12:44:27 | → | simpleauthority joins (~simpleaut@user/simpleauthority) |
| 12:44:57 | × | gurkenglas quits (~gurkengla@dynamic-046-114-179-219.46.114.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 12:45:52 | → | gurkenglas joins (~gurkengla@dynamic-046-114-179-219.46.114.pool.telefonica.de) |
| 12:45:57 | → | swistak joins (~swistak@185.21.216.141) |
| 12:46:39 | → | Logio joins (em@kapsi.fi) |
| 12:46:45 | → | stefan-__ joins (~cri@42dots.de) |
| 12:47:47 | → | codolio joins (~dolio@130.44.134.54) |
| 12:47:48 | → | user___ joins (~user@162.255.84.96) |
| 12:48:08 | → | ystael_ joins (~ystael@user/ystael) |
| 12:51:40 | → | califax_ joins (~califax@user/califx) |
| 12:51:41 | × | tired quits (~tired@user/tired) (Ping timeout: 256 seconds) |
| 12:51:47 | × | califax quits (~califax@user/califx) (Ping timeout: 255 seconds) |
| 12:51:55 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 260 seconds) |
| 12:52:32 | × | xerox quits (~edi@user/edi) (Ping timeout: 246 seconds) |
| 12:52:34 | → | tired joins (~tired@user/tired) |
| 12:52:53 | × | kosmikus quits (~kosmikus@nullzig.kosmikus.org) (Ping timeout: 246 seconds) |
| 12:52:59 | califax_ | is now known as califax |
| 12:53:06 | → | kosmikus joins (~kosmikus@nullzig.kosmikus.org) |
| 12:53:08 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 255 seconds) |
| 12:53:16 | × | Guest11 quits (~Guest11@c83-251-160-169.bredband.tele2.se) (Quit: Client closed) |
| 12:53:30 | → | xerox joins (~edi@user/edi) |
| 12:55:09 | → | gmg joins (~user@user/gehmehgeh) |
| 12:55:51 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 255 seconds) |
| 12:56:13 | × | CiaoSen quits (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 12:56:16 | × | cfricke quits (~cfricke@user/cfricke) (*.net *.split) |
| 12:56:16 | × | wagle quits (~wagle@quassel.wagle.io) (*.net *.split) |
| 12:56:16 | × | biberu quits (~biberu@user/biberu) (*.net *.split) |
| 12:56:16 | × | manwithluck quits (~manwithlu@hoeven.dossingday.ml) (*.net *.split) |
| 12:56:16 | × | meejah quits (~meejah@rutas.meejah.ca) (*.net *.split) |
| 12:56:16 | × | ystael quits (~ystael@user/ystael) (*.net *.split) |
| 12:56:16 | × | ubert quits (~Thunderbi@p548c9fde.dip0.t-ipconnect.de) (*.net *.split) |
| 12:56:16 | × | kimiamania quits (~65804703@user/kimiamania) (*.net *.split) |
| 12:56:16 | × | matthews quits (~matthews@gentoo/developer/matthew) (*.net *.split) |
| 12:56:16 | × | dolio quits (~dolio@130.44.134.54) (*.net *.split) |
| 12:56:16 | × | simeon quits (~pi@143.231.7.51.dyn.plus.net) (*.net *.split) |
| 12:56:16 | × | Vq quits (~vq@90-227-195-41-no77.tbcn.telia.com) (*.net *.split) |
| 12:56:16 | × | APic quits (apic@apic.name) (*.net *.split) |
| 12:56:16 | × | user2 quits (~user@162.255.84.96) (*.net *.split) |
| 12:56:16 | × | noteness_ quits (~noteness@user/noteness) (*.net *.split) |
| 12:56:16 | × | energizer quits (~energizer@user/energizer) (*.net *.split) |
| 12:56:16 | × | heath1 quits (~heath@user/heath) (*.net *.split) |
| 12:56:16 | × | noctux1 quits (Zx24REiiwW@user/noctux) (*.net *.split) |
| 12:56:16 | × | aforemny quits (~aforemny@static.248.158.34.188.clients.your-server.de) (*.net *.split) |
| 12:56:16 | × | AWizzArd quits (~code@user/awizzard) (*.net *.split) |
| 12:56:16 | × | Logio_ quits (em@kapsi.fi) (*.net *.split) |
| 12:56:16 | × | kaol quits (~kaol@94-237-42-30.nl-ams1.upcloud.host) (*.net *.split) |
| 12:56:16 | × | cjay quits (cjay@nerdbox.nerd2nerd.org) (*.net *.split) |
| 12:56:16 | × | dfordvm quits (~dfordivam@tk2-219-19469.vs.sakura.ne.jp) (*.net *.split) |
| 12:56:16 | × | laman2 quits (~laman@rego.ai) (*.net *.split) |
| 12:56:16 | × | hammond__ quits (proscan@gateway02.insomnia247.nl) (*.net *.split) |
| 12:56:16 | × | thaumavorio_ quits (~thaumavor@thaumavor.io) (*.net *.split) |
| 12:56:16 | × | dminuoso_ quits (~dminuoso@user/dminuoso) (*.net *.split) |
| 12:56:16 | × | guygastineau quits (~guygastin@137.184.131.156) (*.net *.split) |
| 12:56:16 | × | tstat_ quits (~tstat@user/tstat) (*.net *.split) |
| 12:56:16 | × | davl_ quits (~davl@207.154.228.18) (*.net *.split) |
| 12:56:16 | × | shachaf quits (~shachaf@user/shachaf) (*.net *.split) |
| 12:56:16 | × | robbert-vdh quits (~robbert@robbertvanderhelm.nl) (*.net *.split) |
| 12:56:17 | × | jakalx quits (~jakalx@base.jakalx.net) (*.net *.split) |
| 12:56:17 | × | ario quits (~ario@159.65.220.102) (*.net *.split) |
| 12:56:17 | × | raoul quits (~raoul@95.179.203.88) (*.net *.split) |
| 12:56:17 | × | ralu1 quits (~ralu@static.211.245.203.116.clients.your-server.de) (*.net *.split) |
| 12:56:17 | × | ridcully_ quits (~ridcully@p508acd69.dip0.t-ipconnect.de) (*.net *.split) |
| 12:56:17 | × | defanor quits (~defanor@tart.uberspace.net) (*.net *.split) |
| 12:56:17 | × | chymera quits (~chymera@ns1000526.ip-51-81-46.us) (*.net *.split) |
| 12:56:17 | × | hank_ quits (~hank@45-33-24-80.ip.linodeusercontent.com) (*.net *.split) |
| 12:56:17 | × | mesaoptimizer quits (apotheosis@user/PapuaHardyNet) (*.net *.split) |
| 12:56:17 | × | lambdap237 quits (~lambdap@static.167.190.119.168.clients.your-server.de) (*.net *.split) |
| 12:56:17 | × | DigitalKiwi quits (~kiwi@137.184.156.191) (*.net *.split) |
| 12:56:17 | × | nicole quits (ilbelkyr@libera/staff/ilbelkyr) (*.net *.split) |
| 12:56:17 | × | stefan-_ quits (~cri@42dots.de) (*.net *.split) |
| 12:56:17 | × | auri quits (~auri@fsf/member/auri) (*.net *.split) |
| 12:56:17 | × | hexology quits (~hexology@user/hexology) (*.net *.split) |
| 12:56:17 | ubert1 | is now known as ubert |
| 12:56:35 | → | APic joins (apic@apic.name) |
| 12:56:40 | → | kimiamania joins (~65804703@user/kimiamania) |
| 12:56:41 | → | tureba joins (~tureba@tureba.org) |
| 12:56:42 | → | hexology joins (~hexology@user/hexology) |
| 12:56:50 | → | energizer joins (~energizer@user/energizer) |
| 12:57:08 | → | chymera joins (~chymera@ns1000526.ip-51-81-46.us) |
| 12:57:20 | → | manwithluck joins (~manwithlu@hoeven.dossingday.ml) |
| 12:57:39 | → | cfricke joins (~cfricke@user/cfricke) |
| 12:57:40 | stefan-__ | is now known as stefan-_ |
| 13:00:37 | → | noteness joins (~noteness@user/noteness) |
| 13:00:43 | ubert | is now known as 078AALVPE |
| 13:00:49 | → | auri joins (~auri@static.46.108.40.188.clients.your-server.de) |
| 13:00:49 | → | wagle joins (~wagle@quassel.wagle.io) |
| 13:00:49 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 13:00:49 | → | biberu joins (~biberu@user/biberu) |
| 13:00:49 | → | meejah joins (~meejah@rutas.meejah.ca) |
| 13:00:49 | → | ubert joins (~Thunderbi@p548c9fde.dip0.t-ipconnect.de) |
| 13:00:49 | → | matthews joins (~matthews@gentoo/developer/matthew) |
| 13:00:49 | → | simeon joins (~pi@143.231.7.51.dyn.plus.net) |
| 13:00:49 | → | Vq joins (~vq@90-227-195-41-no77.tbcn.telia.com) |
| 13:00:49 | → | heath1 joins (~heath@user/heath) |
| 13:00:49 | → | noctux1 joins (Zx24REiiwW@user/noctux) |
| 13:00:49 | → | aforemny joins (~aforemny@static.248.158.34.188.clients.your-server.de) |
| 13:00:49 | → | AWizzArd joins (~code@user/awizzard) |
| 13:00:49 | → | kaol joins (~kaol@94-237-42-30.nl-ams1.upcloud.host) |
| 13:00:49 | → | cjay joins (cjay@nerdbox.nerd2nerd.org) |
| 13:00:49 | → | dfordvm joins (~dfordivam@tk2-219-19469.vs.sakura.ne.jp) |
| 13:00:49 | → | laman2 joins (~laman@rego.ai) |
| 13:00:49 | → | hammond__ joins (proscan@gateway02.insomnia247.nl) |
| 13:00:49 | → | thaumavorio_ joins (~thaumavor@thaumavor.io) |
| 13:00:49 | → | dminuoso_ joins (~dminuoso@user/dminuoso) |
| 13:00:49 | → | guygastineau joins (~guygastin@137.184.131.156) |
| 13:00:49 | → | tstat_ joins (~tstat@user/tstat) |
| 13:00:49 | → | davl_ joins (~davl@207.154.228.18) |
| 13:00:49 | → | shachaf joins (~shachaf@user/shachaf) |
| 13:00:49 | → | robbert-vdh joins (~robbert@robbertvanderhelm.nl) |
| 13:00:49 | → | ario joins (~ario@159.65.220.102) |
| 13:00:49 | → | raoul joins (~raoul@95.179.203.88) |
| 13:00:49 | → | ralu1 joins (~ralu@static.211.245.203.116.clients.your-server.de) |
| 13:00:49 | → | ridcully_ joins (~ridcully@p508acd69.dip0.t-ipconnect.de) |
| 13:00:49 | → | defanor joins (~defanor@tart.uberspace.net) |
| 13:00:49 | → | hank_ joins (~hank@45-33-24-80.ip.linodeusercontent.com) |
| 13:00:49 | → | mesaoptimizer joins (apotheosis@user/PapuaHardyNet) |
| 13:00:49 | → | lambdap237 joins (~lambdap@static.167.190.119.168.clients.your-server.de) |
| 13:00:49 | → | DigitalKiwi joins (~kiwi@137.184.156.191) |
| 13:00:49 | → | nicole joins (ilbelkyr@libera/staff/ilbelkyr) |
| 13:01:00 | → | Guest11 joins (~Guest11@c83-251-160-169.bredband.tele2.se) |
| 13:01:16 | × | swistak quits (~swistak@185.21.216.141) (Quit: bye bye) |
| 13:01:51 | <Guest11> | So, just to conclude things, would FRP be an interesting rabbit hole to develop myself as a Haskell programmer? |
| 13:02:46 | <mon_aaraj> | I suppose. Though be warned, FRP is kind of magical at first. |
| 13:03:45 | × | whatsupdoc quits (uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:04:05 | <Guest11> | mon_aaraj: Magical as in things-get-done-and-I-don't-know-why? |
| 13:04:23 | <mon_aaraj> | Pretty much. |
| 13:04:39 | × | kraftwerk28 quits (~kraftwerk@178.62.210.83) (Remote host closed the connection) |
| 13:04:53 | <Guest11> | I see. That's fine I suppose. Thank you! |
| 13:05:14 | <gurkenglas> | mon_aaraj, "you get things done" or "things are happening"? |
| 13:05:39 | <mon_aaraj> | it's more like "my code is working and i have no clue how or why it does" |
| 13:05:50 | → | kraftwerk28 joins (~kraftwerk@178.62.210.83) |
| 13:06:10 | <gurkenglas> | did the hypothetical person write what came to mind or manipulate copypasted snippets :P |
| 13:06:49 | <mon_aaraj> | the hypothetical person checked the documentation and followed the types |
| 13:07:40 | <mon_aaraj> | when one matches the types up, more often than not i've experienced that stuff will start working. it's just one needs to see what is happening when the stuff is working and why it worked |
| 13:09:24 | <mon_aaraj> | I think for me, I came upon FRP before really even having a proper knowledge of Haskell. After reading Haskell From First Principles I then opened up Yampa in a REPL and just matched the types of some functions. It felt really nice to get stuff working even though I didn't have a single clue what i was doing. |
| 13:09:46 | <kuribas> | Guest11: IMO it's one the rabit holes that actually have practical uses. |
| 13:10:10 | <kuribas> | Guest11: unlike most of category theory. |
| 13:10:51 | <gurkenglas> | noice. can one bring this to its natural conclusion - put half one's code in terms of a type that one suspects has one natural inhabitant even though one couldn't write it, the compiler agrees and doesn't ask for an implementation? |
| 13:11:11 | <Guest11> | kuribas: I had a suspicion of that. Great! I'm digging in! |
| 13:12:23 | <mon_aaraj> | gurkenglas: That's kind of already implemented in wingman. It's used more frequently in Idris and Agda -- stuff like that's called "conversations with the compiler", I like that form of interactive programming. |
| 13:14:24 | × | Guest11 quits (~Guest11@c83-251-160-169.bredband.tele2.se) (Quit: Client closed) |
| 13:14:33 | × | dsrt^ quits (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 13:15:36 | → | king_gs joins (~Thunderbi@187.201.41.239) |
| 13:16:23 | × | MajorBiscuit quits (~MajorBisc@c-001-028-045.client.tudelft.eduvpn.nl) (Ping timeout: 264 seconds) |
| 13:16:41 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:16:59 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 13:17:23 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 13:17:53 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 255 seconds) |
| 13:18:06 | → | MajorBiscuit joins (~MajorBisc@2001:1c00:2408:a400:67e:5371:52a7:9b9a) |
| 13:18:31 | → | swistak joins (~swistak@185.21.216.141) |
| 13:19:31 | <kuribas> | using type holes in haskell is also pretty common. |
| 13:19:40 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 13:20:02 | <kuribas> | we just need an AI that fill in holes |
| 13:20:44 | <gurkenglas> | mon_aaraj: *checks out wingman* aww, that looks like it only does the basic things, as opposed to like https://paste.tomsmeding.com/6GRAZ33t |
| 13:21:18 | <mon_aaraj> | Yep... It's also not working for GHC 9.2 |
| 13:21:26 | × | swistak quits (~swistak@185.21.216.141) (Client Quit) |
| 13:21:40 | <mon_aaraj> | Those along with some other reasons are why I use Agda and Idris a good number of times. |
| 13:21:46 | → | swistak joins (~swistak@185.21.216.141) |
| 13:22:03 | <gurkenglas> | kuribas: Copilot is basically this, HLS should add plumbing to give it type signature context |
| 13:22:30 | <kuribas> | yeah, except that it doesn't check the type, or does it? |
| 13:22:33 | <gurkenglas> | (by the time they're done with the plumbing Copilot should be good enough to work with Haskell...) |
| 13:22:47 | <Axman6> | does that code even make any sense? I'm struggling to see how (forall x. x a -> x c) would ever be useful |
| 13:22:56 | <kuribas> | There was an interesting demo in idris where it filled in continuation monad code, based on the type. |
| 13:23:04 | <merijn> | @quote didn't.you.write.it |
| 13:23:04 | <lambdabot> | No quotes match. BOB says: You seem to have forgotten your passwd, enter another! |
| 13:23:06 | <merijn> | aww |
| 13:23:07 | <kuribas> | Sadly not implemented in the latest idris. |
| 13:23:09 | <gurkenglas> | Axman6: (forall x. x a -> x b) witnesses a=b |
| 13:23:13 | <mon_aaraj> | kuribas: Eh. AI can be and usually is wrong, especially with dependent types. Good Type systems can't. |
| 13:23:31 | <kuribas> | mon_aaraj: that's why we need to mix AI and types :) |
| 13:23:32 | <gurkenglas> | mon_aaraj: just get 10 completions and pick the one that compiles :shrug: |
| 13:24:03 | <Axman6> | I understand those words but don't understand how it does that |
| 13:24:17 | <mon_aaraj> | kuribas: I don't really think that'll work out as well as you think it will |
| 13:24:21 | <merijn> | @quote Didn't.you.write.that |
| 13:24:21 | <lambdabot> | autrijus says: * autrijus stares at type Eval x = forall r. ContT r (ReaderT x IO) (ReaderT x IO x) and feels very lost <shapr> Didn't you write that code? <autrijus> yeah. and it works <autrijus> I |
| 13:24:21 | <lambdabot> | just don't know what it means. |
| 13:24:29 | <merijn> | That was the quote I was thinking off ;) |
| 13:24:42 | <gurkenglas> | fine, make the AI write comments too. |
| 13:24:50 | × | swistak quits (~swistak@185.21.216.141) (Client Quit) |
| 13:25:07 | <kuribas> | mon_aaraj: that's what research is for, isn't it? |
| 13:25:11 | <mon_aaraj> | an AI like, let's say ChatGPT, would just output the most statistically plausible word soup when you give it a prompt. Same thing for Copilot. There's no logic checking at all. |
| 13:25:21 | <Axman6> | is lambdabot's quote dictionary available anywhere? I'd hate for it to disappear |
| 13:25:27 | × | euandreh quits (~Thunderbi@189.6.18.7) (Quit: euandreh) |
| 13:25:34 | <gurkenglas> | mon_aaraj: guess what i do |
| 13:25:37 | <mon_aaraj> | The difference is that for Copilot in very popular languages, the most statistically plausible word soup is usually correct |
| 13:25:44 | <merijn> | Axman6: Whoever hosts it |
| 13:25:52 | <kuribas> | mon_aaraj: I managed ChatGPT to give me a correct implementation of safeTail. |
| 13:25:55 | <merijn> | Axman6: I have a (by now fairly old) copy of it |
| 13:26:13 | <kuribas> | mon_aaraj: it did typecheck. |
| 13:26:17 | <Axman6> | @quote Axman6 |
| 13:26:17 | <lambdabot> | Axman6 says: -ddump-occur-anal <- another terrible name... |
| 13:26:32 | <Axman6> | well, that one certainly is old... |
| 13:26:41 | <merijn> | A lot of them are :p |
| 13:26:43 | <merijn> | @quote merijn |
| 13:26:43 | <lambdabot> | merijn says: after a week you can delete 80% of your code and replace it with whatever edwardk wrote that day ;-) |
| 13:26:51 | <merijn> | Still relevant :p |
| 13:27:04 | <Axman6> | very |
| 13:27:27 | <gurkenglas> | Axman6: (forall x. x a -> x b) doesn't give whoever implements it enough information about x to let them do anything except return the value they have that partially matches the expected type and hope that it completely matches |
| 13:27:31 | <Axman6> | I remember doing exactly that with jackdk once, replaced 5-6 lines of State code with a single lens operator |
| 13:27:50 | <kuribas> | mon_aaraj: https://gist.github.com/kuribas/eada8c691e93e2b519dfb21959d9806e |
| 13:27:50 | <Axman6> | gurkenglas: yeah, right, I can see that now. neat |
| 13:28:16 | <kuribas> | mon_aaraj: but maybe it just got it from somewhere in its database. |
| 13:28:30 | <kuribas> | mon_aaraj: I should try it with a completely new usecase. |
| 13:29:46 | <mon_aaraj> | I've never said it could never be right. I just said it doesn't check if it's right, and it just sends the most plausible output. People can get ChatGPT to do something eventually... but it gets harder and harder the more detailed you want to be and the more obscure your field is -- i.e., dependent types. |
| 13:29:48 | <mon_aaraj> | kuribas: Recursion would be funny. |
| 13:30:14 | <kuribas> | idk, it didn't take that many tries... |
| 13:30:27 | <jackdk> | Axman6: lens continues to do that in my code, fwiw |
| 13:30:31 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:22c2:703e:85c8:b082) |
| 13:30:51 | <kuribas> | "it doesn't check if it's right" <= how could it? It doesn't have a builtin idris interpreter. |
| 13:31:55 | <mon_aaraj> | Doesn't have a built-in logic interpreter, either -- which is the main issue. |
| 13:32:16 | <merijn> | mon_aaraj: to be fair, most people are missing that too :p |
| 13:32:40 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 13:32:43 | → | swistak joins (~swistak@185.21.216.141) |
| 13:33:03 | <kuribas> | hehe, this. Why do people expect a LLM to be magick that could just program out of nowhere? People can't do that either. |
| 13:35:35 | × | MajorBiscuit quits (~MajorBisc@2001:1c00:2408:a400:67e:5371:52a7:9b9a) (Ping timeout: 264 seconds) |
| 13:35:36 | <gurkenglas> | this doesn't rule out that the LLM can replace me |
| 13:35:39 | × | swistak quits (~swistak@185.21.216.141) (Client Quit) |
| 13:36:43 | <kuribas> | depends on what you do in your day job ... |
| 13:37:21 | → | MajorBiscuit joins (~MajorBisc@c-001-028-045.client.tudelft.eduvpn.nl) |
| 13:37:30 | <gurkenglas> | *almost* "make LLMs replace people", wouldn't that be a fun answer |
| 13:38:32 | → | swistak joins (~swistak@185.21.216.141) |
| 13:38:39 | <kuribas> | most of what a programmer does is not churning out code, it's gathering requirements, acquiring domain logic, etc... |
| 13:39:10 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) |
| 13:39:20 | <gurkenglas> | 1. is that most of what edward kmett does? 2. sure it can do that |
| 13:40:11 | <gurkenglas> | (we don't *really* need another hundred of us. another hundred of edward kmett, on the other hand, would be handy) |
| 13:41:53 | <kuribas> | gurkenglas: I don't think edward kmett "acquires domain logic". He probably absorbs it by osmosis. |
| 13:42:05 | <gurkenglas> | domain logic acquires him. |
| 13:42:26 | → | vglfr joins (~vglfr@145.224.100.76) |
| 13:42:28 | <kuribas> | right :) |
| 13:43:49 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) (Ping timeout: 256 seconds) |
| 13:43:51 | × | king_gs quits (~Thunderbi@187.201.41.239) (Read error: Connection reset by peer) |
| 13:43:55 | <sclv> | gurkenglas: parametricity is about one to many relationships between types. those types may be function types! |
| 13:44:47 | → | king_gs joins (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) |
| 13:45:49 | <mon_aaraj> | <kuribas> "hehe, this. Why do people..." <- I didn't complain about that because people can do that, i complained about that because they can't do what type systems do. |
| 13:48:35 | <gurkenglas> | sclv: functions form a subset of relations. does retricting the parametricity theorem to relations that are functions actually weaken it? |
| 13:49:22 | <sclv> | think about why we talk about equality in terms of a relation |
| 13:50:11 | <sclv> | hard to be meaningfully reflexive without being trivial otherwise, no? |
| 13:50:43 | <gurkenglas> | equivalence relations can be expressed using equality and functions to equivalence classes, do you have another example? |
| 13:51:45 | <gurkenglas> | (or if what i just said does not suffice to refute your point, we can stay here) |
| 13:53:23 | <sclv> | i think that alternate expression may work for an equiv relation — if you restrict both sides to equiv classes, then you have a function between them. |
| 13:53:43 | <sclv> | but in my mind thats just a clunkier way of expressing the same thing |
| 13:54:11 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 264 seconds) |
| 13:54:14 | <gurkenglas> | Can you give some corollary of parametricity that i wouldn't want to route through functional language? |
| 13:54:31 | <sclv> | a logical relation is a fattened equiv relation expressed in a certain way. you can re-express it in another equiv way |
| 13:55:02 | <sclv> | like all relations are boolean valued binary functions of a certain form, and you can do that too |
| 13:55:55 | × | Vajb quits (~Vajb@2001:999:230:f561:4ee8:ad7f:13ff:9959) (Ping timeout: 248 seconds) |
| 13:55:57 | <gurkenglas> | I prefer to think of a relation as the set of pairs equipped with two projections to avert boolean blindness |
| 13:56:29 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.8) |
| 13:56:46 | → | Vajb joins (~Vajb@2001:999:68c:7f92:37da:222a:b35b:af4d) |
| 13:57:01 | <gurkenglas> | hmm, if we drop the requirement that every pair appear at most once, we might get a neat categorical phrasing of parametricity |
| 13:57:28 | <gurkenglas> | quick, what's the proof of the parametricity theorem |
| 13:57:52 | <kuribas> | mon_aaraj: my experimentation shows that they can. Sort of ... |
| 13:58:22 | <gurkenglas> | (or, to be fair. what... is the *precise statement* of the parametricity theorem??) |
| 13:59:06 | <ncf> | for t : T, (t, t) ∈ [T] where [T] is a binary relation built by induction on T |
| 13:59:28 | → | systemhalted joins (~systemhal@130.51.137.77) |
| 13:59:48 | → | zer0bitz_ joins (~zer0bitz@2001:2003:f443:d600:fc46:678f:19c6:5892) |
| 13:59:53 | → | anatta_ joins (~AdiIRC@h-155-4-132-216.NA.cust.bahnhof.se) |
| 14:00:01 | → | codaraxis___ joins (~codaraxis@user/codaraxis) |
| 14:00:31 | → | rodental joins (~rodental@38.146.5.222) |
| 14:01:05 | × | systemhalted quits (~systemhal@130.51.137.77) (Remote host closed the connection) |
| 14:02:34 | × | anatta quits (~AdiIRC@h-155-4-132-216.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 14:02:40 | anatta_ | is now known as anatta |
| 14:02:55 | × | zer0bitz quits (~zer0bitz@2001:2003:f443:d600:9d80:2d1f:b124:730) (Ping timeout: 246 seconds) |
| 14:02:55 | × | codaraxis__ quits (~codaraxis@user/codaraxis) (Ping timeout: 246 seconds) |
| 14:02:57 | × | Ghostpatsch quits (~Profpatsc@static.88-198-193-255.clients.your-server.de) (Quit: WeeChat 3.7.1) |
| 14:03:24 | <gurkenglas> | ncf: [T] is some particular such relation, yes? is [T] polymorphic in T :)? |
| 14:04:19 | <ncf> | you start with [Bool], [Nat] etc being just equality and then build up |
| 14:04:51 | <ncf> | something like (f, f') ∈ [A → B] iff ∀ (a, a') ∈ [A], (f a, f' a') ∈ [B] |
| 14:05:09 | <ncf> | and the interpretation of forall leads you to quantify over relations |
| 14:05:25 | <gurkenglas> | okay, so it's the smallest reflexive relation |
| 14:06:11 | <ncf> | no, that would be equality |
| 14:06:27 | <gurkenglas> | oh. name some related pair that isn't equal? |
| 14:07:04 | <ncf> | hang on |
| 14:09:15 | <gurkenglas> | (oh, my :03 line was under the impression that you meant T=Type, not T∈Type) |
| 14:11:11 | <ncf> | right so the point is that this is a kind of equality *across types* |
| 14:11:41 | <gurkenglas> | whuh? i didn't expect to read that last line |
| 14:12:51 | → | coot joins (~coot@213.134.171.3) |
| 14:12:53 | <ncf> | e.g. for any binary relation R between A and B, you can say that id_A and id_B are related by the relation R → R |
| 14:13:26 | <ncf> | it's a variation on equality, if you will |
| 14:13:55 | <ncf> | indeed the way it's implemented in cubical agda is with a second interval type (the first one being used to implement "equality" (paths)) with slightly different semantics |
| 14:14:34 | <gurkenglas> | let me rephrase. for every two types A,B, you're defining a subset of (A,B)? |
| 14:15:21 | <gurkenglas> | And you're defining it by "induction on Type", which means that it's the least family of relations that satisfies some listed properties |
| 14:16:26 | <gurkenglas> | Presumably the subset of (Int,Int) is the diagonal, and the subset of (Int,Bool) is the empty subset |
| 14:16:56 | <gurkenglas> | What is the subset of (Int,[Int])? |
| 14:16:58 | <ncf> | no, you're defining an interpretation of types as binary relations |
| 14:17:14 | <ncf> | Int is interpreted as the equality relation ⊂ Int × Int |
| 14:17:38 | <gurkenglas> | how does "interpret" differ from "mapped to"? |
| 14:17:42 | <ncf> | → is interpreted as an operator that takes two relations between A × B and A' × B' and outputs a relation between (A → A') × (B → B') |
| 14:19:27 | <ncf> | the point is that this construction does not give you an arbitrary relation Int × Bool. it gives you, for each type T, a relation T × T, but this relation is built from operators that operate on heterogeneous relations |
| 14:19:39 | <ncf> | and the heterogeneity plays a role, as you'd expect, in the interpretation of forall. |
| 14:19:51 | <ncf> | at this point i encourage you to read wadler's paper, it's quite easy to read |
| 14:20:16 | <gurkenglas> | I bounced off it! I came here to ask why it's written in terms of relations. |
| 14:20:18 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 14:20:39 | → | Guest2820 joins (~Guest28@HFA62-0-131-117.bb.netvision.net.il) |
| 14:21:02 | <ncf> | because there's no reason not to, but you can replace every instance of "relation" with "function" if that's easier |
| 14:21:16 | <ncf> | as for whether the version restricted to function is less general, i don't know; i suspect so |
| 14:21:20 | <ncf> | functions* |
| 14:22:01 | <gurkenglas> | ah no wadler's is the *second* link on wikipedia, i bounced off the first link https://people.mpi-sws.org/~dreyer/tor/papers/reynolds.pdf |
| 14:22:15 | <ncf> | that's a lot harder to read! |
| 14:24:32 | → | thegeekinside joins (~thegeekin@189.141.115.134) |
| 14:25:34 | → | ph88 joins (~ph88@ip5b426553.dynamic.kabel-deutschland.de) |
| 14:26:00 | <ph88> | is there some extension to allow this? data Foo = Bar {hello :: Int} | Qux {hello :: String} why is it now allowed ? |
| 14:26:06 | × | king_gs quits (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) (Remote host closed the connection) |
| 14:26:26 | → | king_gs joins (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) |
| 14:26:44 | <geekosaur> | ph88, because `hello` is also a function Foo -> (what?) |
| 14:27:21 | <geekosaur> | the `NoFieldSelectors` extension might permit it, but then you have to figure out how to extract `hello` |
| 14:27:37 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 14:27:41 | <gurkenglas> | ncf: you're telling me to read https://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2-tcs.pdf yes? |
| 14:28:07 | <ncf> | gurkenglas: no, i'm talking about the canonical "Theorems for free!" paper |
| 14:28:13 | <ncf> | https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf |
| 14:29:21 | <ph88> | geekosaur, if it would be this data Foo = Bar {hello :: Int} | Qux {bye :: String} would `hello 2` make Bar ? don't really get how that is a function |
| 14:30:08 | <geekosaur> | if `foo :: Foo`, `hello foo` is the value held in the `Bar` alternative or else a runtime error |
| 14:30:35 | <geekosaur> | (if it's a `Qux` instead of a `Bar`) |
| 14:31:47 | <geekosaur> | but if you have `data Foo = Bar {hello :: Int} | Quz {hello :: String}` then for `foo :: Foo`, `hello foo` has no single type; it could be Int or String. which is not permitted |
| 14:31:52 | <ph88> | oh ok understood .. i've only this before when i didn't have a sum type |
| 14:34:00 | → | systemhalted joins (~systemhal@130.51.137.77) |
| 14:35:04 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 14:35:05 | × | king_gs quits (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) (Ping timeout: 246 seconds) |
| 14:39:04 | × | systemhalted quits (~systemhal@130.51.137.77) (Remote host closed the connection) |
| 14:39:11 | × | MajorBiscuit quits (~MajorBisc@c-001-028-045.client.tudelft.eduvpn.nl) (Ping timeout: 264 seconds) |
| 14:39:37 | <ncf> | gurkenglas: btw i may have misled you with <ncf> you can replace every instance of "relation" with "function" if that's easier |
| 14:39:57 | <ncf> | you can't actually do that; the constructions involved don't preserve functionality |
| 14:40:08 | × | gurkenglas quits (~gurkengla@dynamic-046-114-179-219.46.114.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 14:40:20 | <ncf> | it's really just best to stick to the intuition that we're dealing with arbitrary ways that values could be related oh bye then |
| 14:41:46 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 14:41:56 | × | Guest2820 quits (~Guest28@HFA62-0-131-117.bb.netvision.net.il) (Quit: Client closed) |
| 14:42:03 | → | gurkenglas joins (~gurkengla@dynamic-089-204-138-097.89.204.138.pool.telefonica.de) |
| 14:43:53 | <ncf> | gurkenglas: https://ircbrowse.tomsmeding.com/browse/lchaskell?id=891025#trid891025 |
| 14:43:59 | <gurkenglas> | *reads some* okay yeah i see now why relations, not functions. |
| 14:45:06 | <geekosaur> | fwiw my understanding is this all derives from relations between sets, which are less flexible than functions? |
| 14:45:07 | <gurkenglas> | it's about commuting squares |
| 14:45:16 | → | waleee joins (~waleee@h-176-10-137-138.NA.cust.bahnhof.se) |
| 14:45:41 | <gurkenglas> | i don't see yet why one wouldn't go straight to categories instead of staying at relations *keeps reading* |
| 14:45:42 | × | coot quits (~coot@213.134.171.3) (Quit: coot) |
| 14:46:17 | → | king_gs joins (~Thunderbi@187.201.41.239) |
| 14:46:33 | → | MajorBiscuit joins (~MajorBisc@2001:1c00:2408:a400:67e:5371:52a7:9b9a) |
| 14:46:33 | <ncf> | there's a nice conceptual explanation of parametricity in terms of category if you're interested https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html |
| 14:46:47 | <ncf> | it's a bit high-level |
| 14:48:18 | <gurkenglas> | *reads introduction* hesjustlikemeforreal |
| 14:49:35 | <gurkenglas> | oh yeah i should have read this years ago |
| 14:49:53 | <gurkenglas> | (which i would have if i had seem *this* one years ago :P) |
| 14:51:10 | <cheater> | hey all |
| 14:51:21 | <cheater> | what's that stuff that starts with a pound sign? like GH.encodeField #pubkey pubkey raw_ |
| 14:54:58 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 14:56:32 | <geekosaur> | these days it's equivalent to `@"pubkey"`, because nobody liked it; as such, it's kinda hard to find documentation for |
| 14:56:57 | <geekosaur> | (and likely both are going away in favor of record dot syntax, sadly) |
| 14:58:45 | <geekosaur> | basically it desugars to a HasField constraint (https://downloads.haskell.org/ghc/9.6.1-alpha3/docs/users_guide/exts/hasfield.html) |
| 14:59:55 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 15:00:26 | <gurkenglas> | *reads further* omfg it then goes on to accidentally hand me what i needed to formalize my CT insight en passant, 50% chance |
| 15:01:43 | <ncf> | the bit about sections? |
| 15:03:18 | <ncf> | that's essentially why i was objecting that you can do this: you need dependent types to express sections |
| 15:07:50 | <cheater> | geekosaur: and what's `@"pubkey"` ? |
| 15:11:38 | <cheater> | reading the link... |
| 15:11:45 | <cheater> | so uh... is there any difference? |
| 15:13:42 | × | ddellacosta quits (~ddellacos@146.70.166.10) (Quit: WeeChat 3.8) |
| 15:14:40 | → | ddellacosta joins (~ddellacos@146.70.166.10) |
| 15:16:27 | <geekosaur> | any difference where? |
| 15:16:30 | × | king_gs quits (~Thunderbi@187.201.41.239) (Read error: Connection reset by peer) |
| 15:16:58 | <geekosaur> | the @"foo" version requires proper support for type level strings; that's relatively recent |
| 15:17:00 | → | king_gs joins (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) |
| 15:17:11 | <geekosaur> | #foo goes back a bit farther |
| 15:17:37 | <geekosaur> | in either case it's more flexible than old style field selectors |
| 15:18:14 | <geekosaur> | (and is equivalent to doing record accesses/updates using lens; in fact HasField is pretty much the same as the one used by lens) |
| 15:18:37 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 15:19:13 | <geekosaur> | so using #foo instead of @"foo" just gets that code more compatibility with older ghcs |
| 15:19:16 | → | polyphem_ joins (~rod@2a02:810d:840:8754:fedd:193c:1a4:58ad) |
| 15:19:50 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 255 seconds) |
| 15:20:16 | → | Guest11 joins (~Guest11@c83-251-160-169.bredband.tele2.se) |
| 15:20:50 | <gurkenglas> | ncf: yes, the bit about sections. if *this* is what doing it with dependent types looks like that is pretty strong evidence that i do need em |
| 15:21:32 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 15:21:56 | × | Guest11 quits (~Guest11@c83-251-160-169.bredband.tele2.se) (Client Quit) |
| 15:22:07 | <cheater> | geekosaur: hmm... ok |
| 15:24:20 | × | ddellacosta quits (~ddellacos@146.70.166.10) (Quit: WeeChat 3.8) |
| 15:24:44 | → | ddellacosta joins (~ddellacos@146.70.166.10) |
| 15:24:58 | <geekosaur> | more precisely older ghcs had Symbol / type level strings, but @"foo" wasn't yet accepted |
| 15:25:07 | <geekosaur> | iirc |
| 15:25:24 | <geekosaur> | so you had to use #foo |
| 15:26:13 | <gurkenglas> | ncf: one exercise that fell out of my insight was "there's a unique natural way to define composition for free categories" and the bit about sections also reminds me of my proof there |
| 15:26:25 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 15:27:22 | <gurkenglas> | (which is evidence that this language fits my use case) |
| 15:28:17 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 15:28:51 | <gurkenglas> | (made that connection after my three-lines-ago 8-minutes-ago line) |
| 15:30:36 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 15:31:45 | → | Guest2870 joins (~Guest28@HFA62-0-131-117.bb.netvision.net.il) |
| 15:31:45 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 15:32:53 | × | Guest2870 quits (~Guest28@HFA62-0-131-117.bb.netvision.net.il) (Client Quit) |
| 15:35:30 | × | king_gs quits (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) (Ping timeout: 255 seconds) |
| 15:38:58 | × | teo quits (~teo@user/teo) (Ping timeout: 252 seconds) |
| 15:38:58 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:41:36 | → | jero98772 joins (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) |
| 15:45:52 | codolio | is now known as dolio |
| 15:46:06 | → | Ashkan joins (~Ashkan@a119011.upc-a.chello.nl) |
| 15:48:15 | <Ashkan> | Hello |
| 15:48:15 | <Ashkan> | I've noticed a lot of `newtype` definitions use an `un-` prefix for the field inside e.g. `HandlerFor { unHandlerFor :: HandlerData site site -> ...` but others go the opposite direction and use a `run-` prefix like `ResourceT`. I was wondering why is that ? |
| 15:51:30 | <geekosaur> | `un` implies unwrapping; `run` implies execution or evaluation |
| 15:52:29 | <c_wraith> | I don't really think the prefix means that much. |
| 15:53:15 | × | waleee quits (~waleee@h-176-10-137-138.NA.cust.bahnhof.se) (Ping timeout: 248 seconds) |
| 15:53:44 | × | Everything quits (~Everythin@46.185.124.65) (Quit: leaving) |
| 15:54:03 | × | foul_owl quits (~kerry@157.97.134.62) (Ping timeout: 255 seconds) |
| 15:55:04 | × | kenran` quits (~user@user/kenran) (Remote host closed the connection) |
| 15:56:23 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:22c2:703e:85c8:b082) (Quit: WeeChat 2.8) |
| 15:59:14 | → | Guest73 joins (~Guest73@165.225.213.116) |
| 15:59:20 | <Ashkan> | when is it considered unwrapping ? e.g. both `HandlerFor` and `StateT` essentially contain the same thing : a function from something to something else. They encapsulate an action that requires an argument and produces a result in the desired monad |
| 16:00:11 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds) |
| 16:00:39 | <Ashkan> | I have my own datatype which I'm not sure how to name `newtype InMemeory id session a = InMemeory {unInMemory :: TVar (M.Map id session) -> STM a` |
| 16:00:39 | <Ashkan> | It is supposed to mean : an in-memory session store is a `TVar` holding a map from `id`s to `sessions` |
| 16:01:34 | <gurkenglas> | why do you have it? |
| 16:01:40 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 16:02:00 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 16:02:51 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 16:03:16 | → | king_gs joins (~Thunderbi@187.201.41.239) |
| 16:04:25 | × | chele quits (~chele@user/chele) (Quit: Leaving) |
| 16:08:37 | → | gentauro joins (~gentauro@user/gentauro) |
| 16:10:36 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:12:07 | → | CiaoSen joins (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 16:15:28 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 16:15:29 | <Ashkan> | have what ? the `InMemory` ? |
| 16:17:22 | → | jinsun__ joins (~jinsun@user/jinsun) |
| 16:17:22 | jinsun | is now known as Guest1057 |
| 16:17:22 | × | Guest1057 quits (~jinsun@user/jinsun) (Killed (molybdenum.libera.chat (Nickname regained by services))) |
| 16:17:22 | jinsun__ | is now known as jinsun |
| 16:21:06 | <geekosaur> | I would wonder what the newtype is getting you |
| 16:22:17 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 255 seconds) |
| 16:22:44 | × | king_gs quits (~Thunderbi@187.201.41.239) (Read error: Connection reset by peer) |
| 16:23:35 | → | razetime joins (~Thunderbi@117.193.3.64) |
| 16:24:19 | × | pwntips_ quits (~user@24-113-98-114.wavecable.com) (Ping timeout: 246 seconds) |
| 16:24:36 | → | king_gs joins (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) |
| 16:24:43 | × | Ashkan quits (~Ashkan@a119011.upc-a.chello.nl) (Ping timeout: 260 seconds) |
| 16:24:51 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 16:24:51 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 16:25:45 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 16:26:26 | → | pwntips_ joins (~user@24-113-98-114.wavecable.com) |
| 16:31:37 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:32:50 | × | 078AALVPE quits (~Thunderbi@2a02:8109:abc0:6434:64ad:38c9:a22a:dbbb) (Remote host closed the connection) |
| 16:32:51 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 16:33:44 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) |
| 16:34:05 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 16:34:06 | × | vglfr quits (~vglfr@145.224.100.76) (Ping timeout: 255 seconds) |
| 16:34:38 | × | Guest73 quits (~Guest73@165.225.213.116) (Ping timeout: 260 seconds) |
| 16:35:35 | → | BasLaa joins (~BasLaa@84-28-141-28.cable.dynamic.v4.ziggo.nl) |
| 16:37:43 | × | BasLaa quits (~BasLaa@84-28-141-28.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 16:41:12 | → | vglfr joins (~vglfr@145.224.100.76) |
| 16:46:57 | → | mmhat joins (~mmh@p200300f1c7046216ee086bfffe095315.dip0.t-ipconnect.de) |
| 16:48:03 | × | vglfr quits (~vglfr@145.224.100.76) (Ping timeout: 255 seconds) |
| 16:49:07 | × | mbuf quits (~Shakthi@49.204.115.87) (Quit: Leaving) |
| 16:49:23 | → | vglfr joins (~vglfr@145.224.100.76) |
| 16:51:06 | → | euandreh joins (~Thunderbi@189.6.18.7) |
| 16:51:38 | → | Guest11 joins (~Guest11@c83-251-160-169.bredband.tele2.se) |
| 16:51:47 | × | mmhat quits (~mmh@p200300f1c7046216ee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 16:52:34 | × | Guest11 quits (~Guest11@c83-251-160-169.bredband.tele2.se) (Client Quit) |
| 16:55:01 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) (Remote host closed the connection) |
| 17:10:48 | × | vglfr quits (~vglfr@145.224.100.76) (Read error: Connection reset by peer) |
| 17:11:00 | → | vglfr joins (~vglfr@145.224.100.76) |
| 17:14:05 | → | Tuplanolla joins (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) |
| 17:17:12 | × | razetime quits (~Thunderbi@117.193.3.64) (Remote host closed the connection) |
| 17:17:47 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 17:18:59 | × | polyphem_ quits (~rod@2a02:810d:840:8754:fedd:193c:1a4:58ad) (Ping timeout: 255 seconds) |
| 17:19:46 | → | polyphem_ joins (~rod@2a02:810d:840:8754:224e:f6ff:fe5e:bc17) |
| 17:30:09 | <cheater> | geekosaur: thanks |
| 17:32:38 | → | stackdroid18 joins (14094@de1.hashbang.sh) |
| 17:34:25 | → | zeenk joins (~zeenk@2a02:2f04:a20d:f900::7fe) |
| 17:34:44 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 17:35:09 | × | MajorBiscuit quits (~MajorBisc@2001:1c00:2408:a400:67e:5371:52a7:9b9a) (Quit: WeeChat 3.6) |
| 17:36:33 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 17:39:08 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 17:42:47 | × | king_gs quits (~Thunderbi@2806:103e:29:1779:19a5:ca6b:2f79:45e7) (Ping timeout: 264 seconds) |
| 17:43:06 | → | king_gs joins (~Thunderbi@187.201.41.239) |
| 17:44:48 | → | mechap joins (~mechap@user/mechap) |
| 17:45:37 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) |
| 17:46:25 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:47:04 | → | foul_owl joins (~kerry@193.29.61.203) |
| 17:53:44 | × | codaraxis___ quits (~codaraxis@user/codaraxis) (Quit: Leaving) |
| 17:59:08 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 246 seconds) |
| 18:00:15 | × | nschoe quits (~q@141.101.51.197) (Ping timeout: 260 seconds) |
| 18:02:28 | → | econo joins (uid147250@user/econo) |
| 18:03:12 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 18:03:48 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 18:04:29 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 18:05:26 | × | CiaoSen quits (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 18:11:03 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 18:11:18 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 18:11:48 | → | Kuttenbrunzer joins (~Kuttenbru@2a02:8108:8b80:1d48::9550) |
| 18:15:51 | × | Midjak quits (~Midjak@82.66.147.146) (Read error: Connection reset by peer) |
| 18:16:39 | × | dcoutts_ quits (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) (Remote host closed the connection) |
| 18:16:50 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 18:17:02 | → | dcoutts_ joins (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) |
| 18:21:21 | × | Kuttenbrunzer quits (~Kuttenbru@2a02:8108:8b80:1d48::9550) (Quit: Where is it) |
| 18:21:34 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 3.8) |
| 18:23:17 | → | mechap joins (~mechap@user/mechap) |
| 18:23:42 | → | Ashkan joins (~Ashkan@ec2-54-78-14-109.eu-west-1.compute.amazonaws.com) |
| 18:24:28 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 18:24:46 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:25:01 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 18:26:36 | → | opticblast joins (~Thunderbi@172.58.83.235) |
| 18:28:57 | → | king_gs1 joins (~Thunderbi@187.201.41.239) |
| 18:29:03 | × | king_gs quits (~Thunderbi@187.201.41.239) (Read error: Connection reset by peer) |
| 18:29:03 | king_gs1 | is now known as king_gs |
| 18:30:39 | → | Monster196883 joins (~hp@103.15.228.66) |
| 18:31:59 | → | azimut_ joins (~azimut@gateway/tor-sasl/azimut) |
| 18:32:26 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 18:33:21 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 18:33:43 | → | califax joins (~califax@user/califx) |
| 18:35:39 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 256 seconds) |
| 18:38:06 | → | ft joins (~ft@p3e9bc443.dip0.t-ipconnect.de) |
| 18:42:20 | → | hugo- joins (znc@verdigris.lysator.liu.se) |
| 18:44:43 | × | king_gs quits (~Thunderbi@187.201.41.239) (Ping timeout: 256 seconds) |
| 18:46:44 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 18:50:26 | × | azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 18:50:39 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 18:50:54 | × | opticblast quits (~Thunderbi@172.58.83.235) (Ping timeout: 255 seconds) |
| 18:53:01 | → | Midjak joins (~Midjak@82.66.147.146) |
| 18:53:24 | × | Midjak quits (~Midjak@82.66.147.146) (Remote host closed the connection) |
| 18:53:59 | → | Midjak joins (~Midjak@82.66.147.146) |
| 18:57:15 | → | whatsupdoc joins (uid509081@id-509081.hampstead.irccloud.com) |
| 18:58:01 | × | michalz quits (~michalz@185.246.207.203) (Remote host closed the connection) |
| 18:59:12 | → | nschoe joins (~q@2a01:e0a:8e:a190:91bd:1aae:19b1:2ad9) |
| 19:01:16 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 19:07:12 | <dminuoso_> | Ashkan: Names dont have intrinsic meaning, we humans attach meaning to them. Seasoned programmers have a tendency to name according to some semantics or mind model. |
| 19:09:11 | × | Midjak quits (~Midjak@82.66.147.146) (Ping timeout: 264 seconds) |
| 19:09:20 | <dminuoso_> | One of my all time favourite package is `monad-chronicle`, which has very "suggestive" names that make a lot of sense if you adopt a certain mindmodel: https://hackage.haskell.org/package/monad-chronicle-1.0.1/docs/Control-Monad-Chronicle-Class.html#v:retcon |
| 19:09:24 | → | harveypwca joins (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
| 19:10:26 | × | azure_vermilion quits (~azure_ver@164.39.138.83) (Remote host closed the connection) |
| 19:11:27 | × | mei quits (~mei@user/mei) (Quit: mei) |
| 19:11:27 | → | azure_vermilion joins (~Thunderbi@164.39.138.83) |
| 19:11:35 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Ping timeout: 264 seconds) |
| 19:15:17 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 19:17:15 | → | Midjak joins (~Midjak@82.66.147.146) |
| 19:17:24 | × | azure_vermilion quits (~Thunderbi@164.39.138.83) (Quit: azure_vermilion) |
| 19:19:18 | × | Midjak quits (~Midjak@82.66.147.146) (Read error: Connection reset by peer) |
| 19:19:51 | → | Midjak joins (~Midjak@82.66.147.146) |
| 19:20:17 | → | kenaryn joins (~aurele@cre71-h03-89-88-44-27.dsl.sta.abo.bbox.fr) |
| 19:24:46 | × | Ashkan quits (~Ashkan@ec2-54-78-14-109.eu-west-1.compute.amazonaws.com) (Quit: Client closed) |
| 19:28:06 | × | trev quits (~trev@user/trev) (Remote host closed the connection) |
| 19:28:57 | → | trev joins (~trev@user/trev) |
| 19:32:36 | × | dcoutts_ quits (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) (Remote host closed the connection) |
| 19:32:59 | → | dcoutts_ joins (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) |
| 19:34:30 | → | dhil joins (~dhil@78.45.150.83.ewm.ftth.as8758.net) |
| 19:34:35 | × | fserucas quits (~fserucas@2001:818:e376:a400:fb92:70c1:dd88:c7d7) (Ping timeout: 256 seconds) |
| 19:35:37 | → | bilegeek joins (~bilegeek@2600:1008:b027:385c:33be:5951:6763:bc55) |
| 19:35:54 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 255 seconds) |
| 19:38:26 | → | michalz joins (~michalz@185.246.207.193) |
| 19:39:57 | × | dcoutts_ quits (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) (Ping timeout: 255 seconds) |
| 19:44:57 | → | Ashkan joins (~Ashkan@a119011.upc-a.chello.nl) |
| 19:45:57 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:8429:4ceb:8103:61ef) (Remote host closed the connection) |
| 19:51:38 | → | Guest73 joins (~Guest73@165.225.213.116) |
| 19:57:57 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 19:59:05 | → | hagbard joins (~hagbard@user/hagbard) |
| 19:59:45 | × | dhil quits (~dhil@78.45.150.83.ewm.ftth.as8758.net) (Ping timeout: 255 seconds) |
| 20:03:00 | × | vglfr quits (~vglfr@145.224.100.76) (Remote host closed the connection) |
| 20:03:31 | × | harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
| 20:05:37 | → | vglfr joins (~vglfr@145.224.100.76) |
| 20:06:01 | → | dcoutts_ joins (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) |
| 20:07:32 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 20:12:51 | × | michalz quits (~michalz@185.246.207.193) (Remote host closed the connection) |
| 20:13:58 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 20:16:51 | → | michalz joins (~michalz@185.246.207.221) |
| 20:17:29 | → | mncheck joins (~mncheck@193.224.205.254) |
| 20:17:30 | × | mncheck quits (~mncheck@193.224.205.254) (Read error: Connection reset by peer) |
| 20:20:21 | <hagbard> | Hi. A small code snippet results in a warning about noncanonical return definitions. Can someone explain to me (a noob) what that means and what to to about for the specific example? https://paste.tomsmeding.com/Dtd4qtz7 |
| 20:21:20 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:21:26 | <Jade[m]1> | return should be implemented like return = pure where pure is the function from the Applicative typeclass |
| 20:21:46 | <Jade[m]1> | return is simply a relict from when there was no type hierarchy for monads |
| 20:22:00 | → | 077AAMFUK joins (~mncheck@193.224.205.254) |
| 20:22:45 | × | Monster196883 quits (~hp@103.15.228.66) (Ping timeout: 256 seconds) |
| 20:23:44 | <hagbard> | thanks Jade[m]1 . *thinks about it* |
| 20:24:27 | <[exa]> | hagbard: to supplement the "problematic" case -- assumption that `return` is indistinguishable from `pure` is very common, and breaking it in your monads may very easily break libraries |
| 20:25:19 | <Jade[m]1> | which is why it's deprecated - stuff like that shouldn't happen (but it does) |
| 20:25:33 | <[exa]> | (and there's a few other kinda semantic gripes there, such as return not actually returning anywhere, etc.) |
| 20:25:35 | × | vglfr quits (~vglfr@145.224.100.76) (Remote host closed the connection) |
| 20:26:46 | → | vglfr joins (~vglfr@145.224.100.76) |
| 20:26:48 | × | vglfr quits (~vglfr@145.224.100.76) (Remote host closed the connection) |
| 20:27:20 | <Jade[m]1> | the only place where it "returns" is in the context of a do-block as the last statement |
| 20:27:33 | <Jade[m]1> | which in itself shouldn't be a reason to call it that |
| 20:27:38 | <[exa]> | hagbard: btw I assume your `pure` implementation for applicative isn't different, right? |
| 20:28:07 | <hagbard> | That's right. |
| 20:28:50 | <[exa]> | hagbard: ok that's good. You can safely erase the `return` then :] |
| 20:29:40 | <[exa]> | Jade[m]1: +1 :] |
| 20:29:53 | → | vglfr joins (~vglfr@145.224.100.76) |
| 20:30:18 | × | Guest73 quits (~Guest73@165.225.213.116) (Ping timeout: 260 seconds) |
| 20:30:34 | <Jade[m]1> | * which in itself shouldn't be a *reason* to call it that, because it's just syntactic sugar |
| 20:31:09 | <hagbard> | So, i just get rid of the return line? |
| 20:31:25 | <Jade[m]1> | yep, the default implementation takes care of it |
| 20:31:32 | <[exa]> | hagbard: yap, that should work. The default is `return=pure` |
| 20:31:40 | <hagbard> | Got rid of the warning, thanks! |
| 20:31:54 | <[exa]> | also 1 line golfed \o/ |
| 20:31:59 | × | dcoutts_ quits (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 20:32:48 | <Jade[m]1> | [exa]: hahaha |
| 20:35:26 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 20:42:03 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 20:44:34 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Remote host closed the connection) |
| 20:44:37 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:44:53 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 20:48:29 | × | niko quits (niko@libera/staff/niko) (Ping timeout: 615 seconds) |
| 20:51:36 | × | vglfr quits (~vglfr@145.224.100.76) (Remote host closed the connection) |
| 20:53:18 | → | vglfr joins (~vglfr@145.224.100.76) |
| 20:53:30 | × | Ashkan quits (~Ashkan@a119011.upc-a.chello.nl) (Quit: Client closed) |
| 20:53:59 | → | fnurglewitz joins (uid263868@id-263868.lymington.irccloud.com) |
| 20:55:46 | <fnurglewitz> | anyone knows if there's a way to download a file via https and pass it to a function as a lazy bytestring? my goal is to let the function "drive" when the chunks of the file are read (to avoid loading the whole file in memory before starting to process it) |
| 20:56:34 | <fnurglewitz> | I tried to do it with withResponse/brRead but failed |
| 20:56:52 | <c_wraith> | that's not really compatible with http |
| 20:57:35 | <c_wraith> | (unless you're doing stuff with the range header and the server supports it |
| 20:57:37 | <c_wraith> | ) |
| 20:57:46 | <sm> | I've heard of streaming ajax responses I think.. |
| 20:58:05 | <geekosaur> | but that's not strictly http |
| 20:58:07 | <c_wraith> | sure, long-polling exists |
| 20:58:20 | <Jade[m]1> | mhm |
| 20:58:25 | <c_wraith> | but that's server-driven, not client-driven |
| 20:58:30 | <geekosaur> | if you make an http or https request the response comes back as one big lump of data that you can't really stream |
| 20:58:43 | <Jade[m]1> | I don't think it's a problem to process the entire response at once |
| 20:59:00 | <Jade[m]1> | which is the intended way |
| 20:59:59 | <mauke> | if you make an http request, the response comes back on a socket, which the only thing you can do with is stream |
| 21:00:14 | <mauke> | i.e. call read() repeatedly |
| 21:00:34 | <c_wraith> | If you read too slowly, http servers consider that to be an attack and terminate the connection |
| 21:00:43 | <fnurglewitz> | understood |
| 21:00:46 | <c_wraith> | You can't let the consumer drive the process arbitrarily |
| 21:01:16 | <mauke> | eh, slow connections are a thing |
| 21:02:25 | <mauke> | my concern is more that this would involve unsafeInterleaveIO, which I consider black magic |
| 21:02:30 | <fnurglewitz> | it should still be possible to start parse the bytestring before receiving all the data, right? |
| 21:02:32 | <c_wraith> | like I said before - if you really want to drive this from the consumer side, you want to make multiple http requests with range headers - and you need the server to support them |
| 21:02:50 | <geekosaur> | I was going to suggest conduit, which is the principled way |
| 21:03:00 | <fnurglewitz> | the data is going into a conduit later |
| 21:03:12 | <fnurglewitz> | net -> json-stream -> conduit |
| 21:03:17 | <mauke> | if you need it as a single (even lazy) bytestring, there's going to be some friction |
| 21:03:50 | <fnurglewitz> | yup, a single lazy bytestring (which should be just a list of bytestrings internally if I understood correctly) |
| 21:04:12 | <mauke> | yeah, that means unsafeInterleaveIO *shudder* |
| 21:06:55 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 21:07:01 | → | dcoutts_ joins (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) |
| 21:07:25 | <fnurglewitz> | never used it :D |
| 21:08:27 | <mauke> | good. your soul can still be saved |
| 21:08:32 | <fnurglewitz> | oh ok, I suppose the lazy BS readFile function uses it because when I read the file from disk the process uses like 15M of memory |
| 21:08:37 | → | Guest73 joins (~Guest73@165.225.213.116) |
| 21:08:38 | <fnurglewitz> | with a 1.5G file |
| 21:08:54 | <c_wraith> | honestly, unsafePerformIO is fine unless you intentionally make it awful. |
| 21:08:55 | <fnurglewitz> | when downloading it directly from the net the memory is 2G, RIP |
| 21:09:19 | <c_wraith> | unlike unsafePerformST, which gets much more awful much more easily. |
| 21:09:36 | <fnurglewitz> | I wonder if dowloading the file to the filesystem and then reading it helps a bit with the memory |
| 21:09:41 | <Guest73> | Hi, was reading https://wiki.haskell.org/Seq, at the end of the page there's this example, but it doesn't compile. Not sure what that example is supposed to mean? https://godbolt.org/z/xY7nM1bKn |
| 21:10:01 | <fnurglewitz> | maybe the chunks are garbage collected as soon as the buffers are written to disk |
| 21:10:03 | <fnurglewitz> | hm |
| 21:10:10 | × | lyle quits (~lyle@104.246.145.237) (Quit: WeeChat 3.8) |
| 21:10:35 | <mauke> | https://hackage.haskell.org/package/bytestring-0.11.4.0/docs/src/Data.ByteString.Lazy.html#hGetContentsN <- here's how that's implemented |
| 21:10:36 | <geekosaur> | Guest73, those aren't code, they are values with their types |
| 21:10:36 | <c_wraith> | Guest73: that's just showing two expressions. it's not intended to be complete code |
| 21:11:26 | <fnurglewitz> | mauke: lovely <3 |
| 21:12:18 | <fnurglewitz> | I have just 1 doubt now |
| 21:12:19 | <Guest73> | Ok maybe more specifically, does `const undefined :: a -> b` mean something, or what is it missing to mean something? |
| 21:12:28 | <fnurglewitz> | I understand that I can't drive when the server sends data to my socket |
| 21:12:43 | <geekosaur> | :t const undefined |
| 21:12:44 | <lambdabot> | b -> a |
| 21:12:49 | <fnurglewitz> | but still, shouldn't the lazy bytestring I produce be parsed while the data is coming? |
| 21:12:52 | <geekosaur> | :t const |
| 21:12:52 | <lambdabot> | a -> b -> a |
| 21:13:04 | <fnurglewitz> | as of now it's like the parser waits for the whole file to be in memory |
| 21:13:27 | <geekosaur> | in this case `a` is `(undefined :: a)` (any type, since it never actually produces a value), and `b` is yet to be specified |
| 21:13:38 | <mauke> | fnurglewitz: depends on how you're reading the data from the network |
| 21:13:47 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 248 seconds) |
| 21:13:55 | <fnurglewitz> | may i link a pastebin? the code is horrible but probably you can spot where I'm wrong |
| 21:13:55 | × | hugo- quits (znc@verdigris.lysator.liu.se) (Ping timeout: 260 seconds) |
| 21:14:08 | <mauke> | sure |
| 21:14:23 | <geekosaur> | and the point of this is that thyere is normally no way to distinguish between the two `undefined`s |
| 21:14:29 | <fnurglewitz> | mauke: https://pastebin.com/TEXNyjKS |
| 21:14:37 | <fnurglewitz> | pls don't mind the code, I'm really bad :D |
| 21:14:44 | <mauke> | (I'm probably not going to be much help, but I hope others are more knowledgeable) |
| 21:15:46 | <geekosaur> | but `seq` means these two cases (direct `undefined` used at a function type, vs. a function which always produces `undefined` when applied) can be distinguished |
| 21:15:58 | <geekosaur> | it is admittedly a tricky case |
| 21:16:15 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 248 seconds) |
| 21:16:53 | <Guest73> | Ok thanks geekosaur, will take a few minutes (...hours) to sink that in :P |
| 21:18:28 | <mauke> | fnurglewitz: OK, so your provaRead/go function contains a loop that collects the whole response in memory before returning |
| 21:19:20 | <fnurglewitz> | mauke: I was hoping for it to be lazy |
| 21:19:55 | → | dhil joins (~dhil@78.45.150.83.ewm.ftth.as8758.net) |
| 21:20:02 | <mauke> | it can't be, really; it's sequenced by IO |
| 21:21:18 | <fnurglewitz> | hm, but readFile is lazy :D |
| 21:21:25 | <fnurglewitz> | and it's still IO |
| 21:22:15 | <geekosaur> | readFile uses unsafeInterleaveIO, which is evil |
| 21:22:22 | <fnurglewitz> | :D |
| 21:22:43 | <fnurglewitz> | maybe something evil like mutating an IORef? |
| 21:22:56 | <geekosaur> | it's doing reads in pure code |
| 21:23:07 | <geekosaur> | s/reads/I\/O/ |
| 21:23:42 | <fnurglewitz> | or maybe just spawn wget, wait for it to be done and read from FS, lol |
| 21:24:07 | <mauke> | the "morally right" way to do this would be to use https://hackage.haskell.org/package/json-stream-0.4.5.2/docs/Data-JsonStream-Parser.html#t:ParseOutput |
| 21:24:17 | <mauke> | and feed it bytestring chunks as they're received |
| 21:24:35 | <mauke> | (I don't know if conduit has a streaming json parser built in) |
| 21:25:31 | <fnurglewitz> | I can try |
| 21:25:34 | <fnurglewitz> | thanks |
| 21:25:38 | <fnurglewitz> | "morally" :D |
| 21:25:44 | <geekosaur> | "built in" isn't a thing; rather, it provides an interface for things like JSON parsers to use, much as base provides a framework for traditional I/O |
| 21:25:59 | <mauke> | in fact, the whole thing should probably be set up as a conduit pipeline, not just the part after JSON parsing |
| 21:26:03 | <mauke> | https://hackage.haskell.org/package/http-conduit-2.3.8/docs/Network-HTTP-Client-Conduit.html#v:withResponse |
| 21:26:39 | <mauke> | you'd "just" have to fit the JSON parser in there somehow |
| 21:27:02 | <fnurglewitz> | sounds scary |
| 21:27:19 | <fnurglewitz> | I'll try |
| 21:27:36 | <geekosaur> | https://hackage.haskell.org/package/ndjson-conduit ? |
| 21:27:57 | <mauke> | doesn't sound like it's newline delimited |
| 21:28:02 | × | mrcsno quits (~mrcsno@71.69.152.220) (Read error: Connection reset by peer) |
| 21:28:10 | <mauke> | because that's the other issue: raw JSON isn't exactly streaming friendly |
| 21:28:39 | <fnurglewitz> | luckily the json is quite simple |
| 21:28:44 | <mauke> | hey, but at least conduit has actual documentation |
| 21:28:46 | <fnurglewitz> | json-stream had no issues reading it |
| 21:28:48 | <fnurglewitz> | *parsing |
| 21:29:23 | <mauke> | I tried 'streaming' and parts of the documentation just devolve into unhinged ranting |
| 21:29:38 | <mauke> | and the documentation stops halfway through :-) |
| 21:30:13 | <mauke> | fnurglewitz: you weren't really doing streaming, though. you just fed the whole input to parseLazyByteString |
| 21:30:49 | <fnurglewitz> | when reading from FS the process topped at 15M in memory though |
| 21:31:07 | <fnurglewitz> | it never loaded the whole json in memory |
| 21:31:28 | → | hugo- joins (znc@verdigris.lysator.liu.se) |
| 21:31:38 | <fnurglewitz> | when getting it from http-client I agree that it wasn't doing any streaming |
| 21:31:40 | × | dhil quits (~dhil@78.45.150.83.ewm.ftth.as8758.net) (Ping timeout: 260 seconds) |
| 21:31:51 | <mauke> | yes, because of the unsafeInterleaveIO shenanigans in readFile |
| 21:32:09 | <fnurglewitz> | best function ever |
| 21:32:38 | × | ph88 quits (~ph88@ip5b426553.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 21:32:47 | × | trev quits (~trev@user/trev) (Remote host closed the connection) |
| 21:33:18 | × | Guest73 quits (~Guest73@165.225.213.116) (Ping timeout: 260 seconds) |
| 21:36:15 | → | __monty__ joins (~toonn@user/toonn) |
| 21:36:25 | → | rekahsoft joins (~rekahsoft@142.188.185.92) |
| 21:36:27 | → | cyphase joins (~cyphase@user/cyphase) |
| 21:37:14 | → | fbytez joins (~uid@2001:bc8:2117:100::) |
| 21:39:16 | × | kenaryn quits (~aurele@cre71-h03-89-88-44-27.dsl.sta.abo.bbox.fr) (Quit: leaving) |
| 21:39:49 | → | notzmv joins (~zmv@user/notzmv) |
| 21:40:26 | → | Guest73 joins (~Guest73@165.225.213.116) |
| 21:50:03 | × | hugo- quits (znc@verdigris.lysator.liu.se) (Ping timeout: 248 seconds) |
| 21:53:24 | → | akegalj joins (~akegalj@78-1-169-101.adsl.net.t-com.hr) |
| 21:55:26 | → | niko joins (niko@libera/staff/niko) |
| 21:56:51 | → | xkuru joins (~xkuru@user/xkuru) |
| 21:57:03 | → | Sinbad joins (~Sinbad@user/sinbad) |
| 21:58:52 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 22:00:13 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 22:01:16 | <Sinbad> | using cabal install with --prefix=<some-path> or --bindir=<some-path> doesn't seem to make any difference, it always installs into ~/.cabal/bin. am I overlooking something? |
| 22:01:19 | → | hugo- joins (znc@verdigris.lysator.liu.se) |
| 22:01:26 | <akegalj> | what is the intuition behind traverse over list. traverse (\x -> [0..x]) [0..2] === [[0,0,0],[0,0,1],[0,0,2],[0,1,0],[0,1,1],[0,1,2]] . I cant figure out how to use this, or even build model around it. When is this used and when is it useful ? |
| 22:01:45 | × | michalz quits (~michalz@185.246.207.221) (Remote host closed the connection) |
| 22:02:03 | <Sinbad> | I am using cabal-install version 3.8.1.0 |
| 22:02:16 | → | Guest|57 joins (~Guest|57@2004223482.kn.vutbr.cz) |
| 22:02:28 | <c_wraith> | akegalj: that example probably isn't very useful. But you can think of it as a combination of fmap and sequenceA, each of which is quite natural there |
| 22:02:59 | <geekosaur> | Sinbad, those are cabal v1-style. for v2 you want --installdir |
| 22:03:13 | <c_wraith> | > fmap (\x -> [0 .. x]) [0..2] -- yeah, over lists it's just map |
| 22:03:14 | <lambdabot> | [[0],[0,1],[0,1,2]] |
| 22:03:20 | <jackdk> | Also, you often find implementations of things because they must exist, not because they're "for" anything in particular. |
| 22:03:24 | <geekosaur> | (v2 doesn't really install, it drops a symlink into cabal's store) |
| 22:03:35 | <c_wraith> | > sequenceA [[1,2],[3,4],[5,6,7]] |
| 22:03:37 | <lambdabot> | [[1,3,5],[1,3,6],[1,3,7],[1,4,5],[1,4,6],[1,4,7],[2,3,5],[2,3,6],[2,3,7],[2,... |
| 22:04:02 | <c_wraith> | so sequenceA is pretty naturally just a sort of generalized product, over lists of lists |
| 22:04:25 | <c_wraith> | traverse just happens to do both at once. Not always useful for lists of lists, but often a very useful combination |
| 22:06:32 | × | thegeekinside quits (~thegeekin@189.141.115.134) (Ping timeout: 252 seconds) |
| 22:07:39 | × | Guest|57 quits (~Guest|57@2004223482.kn.vutbr.cz) (Quit: Connection closed) |
| 22:07:50 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 260 seconds) |
| 22:07:52 | × | eggplantade quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 22:11:06 | <akegalj> | c_wraith: ok, I think I had wrong intution about sequence. It makes sense now. Thanks for patience! |
| 22:11:35 | <Sinbad> | geekosaur: thanks. where is this documented? the help just list all the flags what I am using and what you just said without mentioning v1/v2. the docs (stable) don't even contain --installdir |
| 22:11:35 | × | nschoe quits (~q@2a01:e0a:8e:a190:91bd:1aae:19b1:2ad9) (Ping timeout: 264 seconds) |
| 22:12:27 | → | Square2 joins (~Square4@user/square) |
| 22:13:54 | <geekosaur> | I'm not sure it is. 😞 I know it because I've been using cabal for years. the help in particular is a known problem area which I think people will be working on (hopefully they'll do a Season of Docs project on it…) |
| 22:14:32 | <geekosaur> | https://cabal.readthedocs.io/en/3.8/cabal-commands.html?highlight=--installdir#cabal-install |
| 22:15:09 | <geekosaur> | (the "stable" thing is a recently discovered wart in the docs, which they're still trying to sort out) |
| 22:15:48 | <geekosaur> | (readthedocs picked it automatically and they're still trying to figutre out how to make it pick the right one; it should be using the doc set I did) |
| 22:20:59 | <Sinbad> | geekosaur: I see, I should keep in mind to read the 3.8 docs. I tried first the --help, found --bindir and went with it without reading to to bottom where the very last entry is --installdir. I might fill a bug about that. |
| 22:21:58 | <geekosaur> | yeh, the v1 and v2-style options are all jumbled together |
| 22:24:26 | → | kenaryn joins (~aurele@89-88-44-27.abo.bbox.fr) |
| 22:24:57 | × | kenaryn quits (~aurele@89-88-44-27.abo.bbox.fr) (Client Quit) |
| 22:28:09 | × | dcoutts_ quits (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) (Ping timeout: 255 seconds) |
| 22:30:10 | → | dcoutts_ joins (~duncan@cpc69403-oxfd27-2-0-cust285.4-3.cable.virginm.net) |
| 22:34:14 | → | thegeekinside joins (~thegeekin@189.141.115.134) |
| 22:36:05 | × | Guest73 quits (~Guest73@165.225.213.116) (Quit: Client closed) |
| 22:36:16 | <remexre> | anyone know the name of the technique for getting extensible datatypes/languages w/ pattern functors as like, Fix (PartA :+: PartB :+: PartC) |
| 22:37:35 | <akegalj> | how to find out lambdabot options? Is there help for it here on irc? I was sent a message via lambdabot which was delivered when I got online - which is a nice so would like to find out how can I use it |
| 22:38:36 | <geekosaur> | not sure what you mean by options? |
| 22:39:18 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:40:37 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 22:40:46 | <geekosaur> | https://github.com/lambdabot/lambdabot/pull/205/files has a full list of commands (and you can see it's waiting to be accepted upstream) |
| 22:42:52 | × | Sinbad quits (~Sinbad@user/sinbad) (Quit: WeeChat 3.8) |
| 22:43:02 | <akegalj> | geekosaur: thanks! so to send message to someone who is offline I do `@ask user msg` |
| 22:43:56 | <geekosaur> | or @tell, yes. (it just changes the word used in the delivered message: `<foo> asks` vs. `<foo> says`) |
| 22:44:27 | <akegalj> | got it |
| 22:44:58 | × | gurkenglas quits (~gurkengla@dynamic-089-204-138-097.89.204.138.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 22:46:49 | → | ph88 joins (~ph88@ip5b426553.dynamic.kabel-deutschland.de) |
| 22:47:13 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:49:57 | <monochrom> | remexre: Perhaps "data types a la carte"? That's the name of the paper that did it. |
| 22:50:01 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 22:51:10 | <remexre> | That's it, thanks! |
| 22:54:26 | → | slack1256 joins (~slack1256@186.11.13.167) |
| 22:55:40 | × | forell quits (~forell@user/forell) (Ping timeout: 252 seconds) |
| 22:59:47 | × | ubert quits (~Thunderbi@p548c9fde.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 22:59:48 | → | ub joins (~Thunderbi@p548c9fde.dip0.t-ipconnect.de) |
| 23:00:03 | → | forell joins (~forell@user/forell) |
| 23:01:35 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Quit: ZNC - https://znc.in) |
| 23:01:38 | × | tubogram44 quits (~tubogram@user/tubogram) (Quit: See ya later!) |
| 23:02:01 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 23:02:05 | ub | is now known as ubert |
| 23:05:19 | × | rekahsoft quits (~rekahsoft@142.188.185.92) (Ping timeout: 268 seconds) |
| 23:09:55 | → | tubogram44 joins (~tubogram@user/tubogram) |
| 23:24:14 | × | akegalj quits (~akegalj@78-1-169-101.adsl.net.t-com.hr) (Quit: leaving) |
| 23:27:26 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 23:27:44 | → | img joins (~img@user/img) |
| 23:29:14 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 23:38:34 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 23:40:07 | × | ski quits (~ski@remote11.chalmers.se) (Quit: Lost terminal) |
| 23:42:56 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 23:43:42 | → | bilegeek_ joins (~bilegeek@183.sub-174-208-230.myvzw.com) |
| 23:46:31 | × | bilegeek quits (~bilegeek@2600:1008:b027:385c:33be:5951:6763:bc55) (Ping timeout: 260 seconds) |
| 23:50:48 | → | opticblast joins (~Thunderbi@172.58.83.235) |
All times are in UTC on 2023-03-01.