| 2024-04-16 00:04:05 +0200 | lainon | (~lainon@2607:fb90:af24:4a15:91e7:ba33:e025:e099) (Quit: lainon) |
| 2024-04-16 00:05:01 +0200 | chele_ | (~chele@user/chele) (Remote host closed the connection) |
| 2024-04-16 00:06:50 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-16 00:08:22 +0200 | Square2 | (~Square4@user/square) |
| 2024-04-16 00:11:23 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 2024-04-16 00:11:23 +0200 | Square | (~Square@user/square) (Ping timeout: 264 seconds) |
| 2024-04-16 00:12:04 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 2024-04-16 00:30:12 +0200 | CATS | (apic@brezn3.muc.ccc.de) (Ping timeout: 260 seconds) |
| 2024-04-16 00:42:31 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-04-16 00:42:43 +0200 | CATS | (apic@brezn3.muc.ccc.de) |
| 2024-04-16 00:43:03 +0200 | acidjnk | (~acidjnk@p200300d6e714dc36e896bc542a6281cf.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 2024-04-16 00:51:31 +0200 | mima | (~mmh@aftr-62-216-211-38.dynamic.mnet-online.de) (Ping timeout: 246 seconds) |
| 2024-04-16 00:54:20 +0200 | janus | (~janus@user/janus) () |
| 2024-04-16 01:05:30 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-04-16 01:09:49 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Ping timeout: 272 seconds) |
| 2024-04-16 01:11:19 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 01:14:08 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-04-16 01:22:45 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) (Ping timeout: 256 seconds) |
| 2024-04-16 01:23:59 +0200 | YuutaW | (~YuutaW@2404:f4c0:f9c3:502::100:17b7) |
| 2024-04-16 01:26:57 +0200 | son0p | (~ff@186.115.73.190) |
| 2024-04-16 01:29:33 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 2024-04-16 01:31:45 +0200 | son0p | (~ff@186.115.73.190) (Ping timeout: 268 seconds) |
| 2024-04-16 01:34:59 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-04-16 01:36:13 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
| 2024-04-16 01:38:45 +0200 | qqq | (~qqq@92.43.167.61) (Ping timeout: 252 seconds) |
| 2024-04-16 01:40:38 +0200 | qqq | (~qqq@92.43.167.73) |
| 2024-04-16 01:41:55 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3141-2665-793a-5dc9-a564-c4a6.rev.sfr.net) (Remote host closed the connection) |
| 2024-04-16 01:45:20 +0200 | YuutaW | (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (Ping timeout: 260 seconds) |
| 2024-04-16 01:46:19 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) |
| 2024-04-16 01:46:32 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 01:47:23 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Quit: quit) |
| 2024-04-16 01:47:59 +0200 | qqq | (~qqq@92.43.167.73) (Ping timeout: 264 seconds) |
| 2024-04-16 01:48:39 +0200 | qqq | (~qqq@92.43.167.61) |
| 2024-04-16 01:55:03 +0200 | tri | (~tri@2600:8805:da0e:9d00:6593:a12b:f5e0:81d0) |
| 2024-04-16 01:59:48 +0200 | tri | (~tri@2600:8805:da0e:9d00:6593:a12b:f5e0:81d0) (Ping timeout: 268 seconds) |
| 2024-04-16 02:02:57 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2024-04-16 02:05:15 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2024-04-16 02:05:40 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2024-04-16 02:10:39 +0200 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) |
| 2024-04-16 02:12:01 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 246 seconds) |
| 2024-04-16 02:17:18 +0200 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-16 02:17:56 +0200 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
| 2024-04-16 02:20:28 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 2024-04-16 02:20:58 +0200 | peterbecich | (~Thunderbi@47.229.123.186) |
| 2024-04-16 02:33:27 +0200 | <Inst> | what's the replacement for overlapping instances again? |
| 2024-04-16 02:34:29 +0200 | <dolio> | The various pragmas with similar names. |
| 2024-04-16 02:34:32 +0200 | <geekosaur> | overlapping instances are still there, you just do them differently (fine control instead of indiscriminately in a whole source file) |
| 2024-04-16 02:36:25 +0200 | peterbecich | (~Thunderbi@47.229.123.186) (Ping timeout: 256 seconds) |
| 2024-04-16 02:39:07 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) (Ping timeout: 272 seconds) |
| 2024-04-16 02:42:55 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 272 seconds) |
| 2024-04-16 02:43:37 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 02:43:40 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-04-16 02:46:04 +0200 | mei | (~mei@user/mei) |
| 2024-04-16 02:46:50 +0200 | causal | (~eric@50.35.88.207) |
| 2024-04-16 02:48:12 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 2024-04-16 03:00:17 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 03:07:51 +0200 | <probie> | Which of the parser combinator libraries (or any parsing library if it's really good) do people recommend these days if I don't really care about performance, but would like to give helpful error messages? My current choice is trifecta, but is there something better? |
| 2024-04-16 03:11:24 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 2024-04-16 03:12:16 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) |
| 2024-04-16 03:12:28 +0200 | <jackdk> | I could never figure out trifecta. If you and your team make it work, I don't see any reason to change. I don't know if it caught on, but someone released https://github.com/mesabloo/diagnose | https://hackage.haskell.org/package/diagnose a couple of years back, and it appears to have converters for megaparsec errors |
| 2024-04-16 03:13:03 +0200 | euleritian | (~euleritia@dynamic-176-004-212-165.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-16 03:13:20 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-16 03:15:15 +0200 | <jackdk> | The discussion around the announcement for `diagnose` also makes reference to `errata` and `chapelure`. I'd be interested to know if you evaluate these and like one or the other the most |
| 2024-04-16 03:16:47 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 2024-04-16 03:17:35 +0200 | halloy3555 | (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-04-16 03:18:59 +0200 | halloy3555 | (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Remote host closed the connection) |
| 2024-04-16 03:19:14 +0200 | halloy3555 | (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-04-16 03:19:24 +0200 | <sm> | megaparsec++ |
| 2024-04-16 03:19:39 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 255 seconds) |
| 2024-04-16 03:20:47 +0200 | halloy3555 | (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Remote host closed the connection) |
| 2024-04-16 03:21:02 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-04-16 03:24:50 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) |
| 2024-04-16 03:27:35 +0200 | <probie> | Using something like diagnose or errata seems like a good idea. I think I'll be boring and go with megaparsec + diagnose |
| 2024-04-16 03:28:08 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 03:31:47 +0200 | Core4595 | (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) |
| 2024-04-16 03:31:47 +0200 | rosco | (~rosco@aq052236.dynamic.ppp.asahi-net.or.jp) (Read error: Connection reset by peer) |
| 2024-04-16 03:32:11 +0200 | Core4595 | (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) (Read error: Connection reset by peer) |
| 2024-04-16 03:32:25 +0200 | rosco | (~rosco@aq052236.dynamic.ppp.asahi-net.or.jp) |
| 2024-04-16 03:32:59 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) (Ping timeout: 264 seconds) |
| 2024-04-16 03:33:44 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-04-16 03:34:22 +0200 | <Inst> | I don't understand why people complain about lazy functional programming |
| 2024-04-16 03:34:30 +0200 | <Inst> | trying to inject FP into Julia, ugh |
| 2024-04-16 03:34:50 +0200 | <Inst> | at least Python turns FP idioms into iterators |
| 2024-04-16 03:34:57 +0200 | <geekosaur> | <cynic> it forces them to think </cynic> |
| 2024-04-16 03:36:07 +0200 | mei | (~mei@user/mei) |
| 2024-04-16 03:36:11 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) (Ping timeout: 260 seconds) |
| 2024-04-16 03:37:14 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) |
| 2024-04-16 03:38:39 +0200 | <Inst> | like, typed FP is an optimum for FP |
| 2024-04-16 03:39:24 +0200 | <Inst> | has drawbacks, but usually being familiar with workarounds solves the problem |
| 2024-04-16 03:40:14 +0200 | <Inst> | lazy FP also seems to be a local maxima, since while you have to worry about space leaks, you only get as much processing as you need |
| 2024-04-16 03:43:59 +0200 | <monochrom> | <extreme cynicism> Because programmers are control freaks. </extreme cynicism> |
| 2024-04-16 03:45:04 +0200 | <monochrom> | <moar extreme cynicism> Oh they are also hypocrites too. Look how they embrace OOP which obscures control even more than laziness does </moar extreme cynicism> |
| 2024-04-16 03:45:33 +0200 | <monochrom> | At that point I'm wondering if I should just s/cynicism/fundamental hatred of humanity/ |
| 2024-04-16 03:46:07 +0200 | <probie> | monochrom: You're not wrong. In my late teens, I had a bad habit of writing inline assembly in my C because I didn't trust the compiler to produce "the right" code (ignoring the fact that gcc generally did a better job than me anyway) |
| 2024-04-16 03:46:14 +0200 | <Inst> | don't, it made me very very unpopular |
| 2024-04-16 03:47:15 +0200 | otto_s | (~user@p4ff27773.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2024-04-16 03:47:37 +0200 | <geekosaur> | I only resorted to inline asm in 2 cases, and in both of them I considered it a compiler bug |
| 2024-04-16 03:47:44 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 2024-04-16 03:47:46 +0200 | Core7966 | (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) |
| 2024-04-16 03:47:54 +0200 | rosco | (~rosco@aq052236.dynamic.ppp.asahi-net.or.jp) (Read error: Connection reset by peer) |
| 2024-04-16 03:47:55 +0200 | <geekosaur> | it's the compiler's job to worry about the asm for me! |
| 2024-04-16 03:48:24 +0200 | Core7966 | (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) (Read error: Connection reset by peer) |
| 2024-04-16 03:48:38 +0200 | otto_s | (~user@p4ff2776b.dip0.t-ipconnect.de) |
| 2024-04-16 03:49:00 +0200 | rosco | (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) |
| 2024-04-16 03:50:43 +0200 | xff0x | (~xff0x@2405:6580:b080:900:1540:8996:2d0b:5b54) (Ping timeout: 255 seconds) |
| 2024-04-16 03:53:56 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 03:55:26 +0200 | <geekosaur> | granted, I started out writing asm (and hand-assembling it, for ancient microcomputers). for me the whole point of a compiler was to get away from writing the asm myself |
| 2024-04-16 03:57:03 +0200 | <jackdk> | probie: if you move off trifecta, write up an example first for the rest of us? |
| 2024-04-16 03:58:27 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 2024-04-16 03:58:34 +0200 | <geekosaur> | (also, C was my introduction to types. if this doesn't make sense to you, you didn't start out doing asm) |
| 2024-04-16 04:02:33 +0200 | cipherrot | (~znc-user@user/petrichor) |
| 2024-04-16 04:03:02 +0200 | petrichor | (~znc-user@user/petrichor) (Ping timeout: 256 seconds) |
| 2024-04-16 04:03:09 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 04:03:13 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-04-16 04:04:08 +0200 | <monochrom> | It is OK to start types with that. That's what happened at the beginning of PL research too. For example Strachey's Fundamental Concepts in Programming Languages. |
| 2024-04-16 04:04:30 +0200 | <jackdk> | geekosaur: staring out doing BASIC meant that C could be my introduction to types, too. Though I dabbled in pascal for a while, but a young kid with a textbook and no-one else to talk to about pascal can only get so far |
| 2024-04-16 04:07:05 +0200 | <geekosaur> | strictly speaking I started out on BASIC too, but it was such a limited toy that I abandoned it for asm quickly |
| 2024-04-16 04:08:56 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-04-16 04:14:14 +0200 | <monochrom> | Oh BASIC had types. It was just combining the type safety of C with the hungarian-wannabe sigil system of Perl. |
| 2024-04-16 04:14:42 +0200 | <monochrom> | N is of the number type, N$ is of the string type. |
| 2024-04-16 04:14:59 +0200 | <jackdk> | despite predating both |
| 2024-04-16 04:15:40 +0200 | <jackdk> | VB (and maybe others) extended that to avoid having to write `dim i as integer`: you had `%` for ints, `&` for longs, etc. (IIRC) |
| 2024-04-16 04:18:16 +0200 | <c_wraith> | that definitely predates VB. It was in the old TRS-80 basic I first learned to program in. |
| 2024-04-16 04:18:40 +0200 | <geekosaur> | I recall it having % but not & |
| 2024-04-16 04:18:46 +0200 | <c_wraith> | well. not longs, that hardware didn't have them. But it had integers and floats. |
| 2024-04-16 04:18:54 +0200 | <geekosaur> | yeh |
| 2024-04-16 04:19:00 +0200 | <c_wraith> | though it didn't have floating-point hardware, so they were *slow* |
| 2024-04-16 04:19:53 +0200 | <geekosaur> | nobody had invented floating point coprocessors yet. and when Intel got around to it, it was a sideboard stack machine |
| 2024-04-16 04:20:26 +0200 | <geekosaur> | I was especially happy to let the compiler deal with that mess |
| 2024-04-16 04:21:04 +0200 | <jackdk> | kids these days don't know how good they have it. I remember an errata card for TI (99/4A) Extended Basic saying they removed the ability for subroutines to call themselves because "it was occasionally useful but mostly a mistake" |
| 2024-04-16 04:21:51 +0200 | <monochrom> | Nah I think kids these days would love to have that card mandated so they don't have to learn recursion. |
| 2024-04-16 04:22:13 +0200 | sgarcia_ | (sgarcia@swarm.znchost.com) (Quit: Hosted by www.ZNCHost.com) |
| 2024-04-16 04:22:18 +0200 | <geekosaur> | that one is understandable though, the TMS9900 thought it was a baby IBM mainframe. BALR anyone? |
| 2024-04-16 04:23:06 +0200 | <monochrom> | But BASIC's dumb GOSUB rendered recursion useless. So the claim was right in context. (You need at least parameter passing to make recursion useful.) |
| 2024-04-16 04:23:09 +0200 | <geekosaur> | (stuffed the return address into a register, and $DEITY help you if you overwrote it) |
| 2024-04-16 04:23:42 +0200 | <monochrom> | Well, perhaps s/dumb/simpleton/ |
| 2024-04-16 04:23:57 +0200 | <c_wraith> | yeah, GOSUB didn't have any idea of parameters. Just global variables. So, recursion wasn't very useful... |
| 2024-04-16 04:24:59 +0200 | <geekosaur> | mm, right, I at one point had a BASIC preprocessor that did silly things like use an array ZZ as a parameter stack |
| 2024-04-16 04:25:08 +0200 | sgarcia | (sgarcia@swarm.znchost.com) |
| 2024-04-16 04:25:26 +0200 | <geekosaur> | as well as adding control structures |
| 2024-04-16 04:25:44 +0200 | Katarushisu1 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 2024-04-16 04:26:00 +0200 | <geekosaur> | I ditched it when I got Turbo Pascal |
| 2024-04-16 04:26:07 +0200 | Katarushisu1 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 2024-04-16 04:31:19 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) |
| 2024-04-16 04:33:35 +0200 | as_ | (~as@2800:a4:307:6f00:2530:9589:e186:2373) |
| 2024-04-16 04:34:34 +0200 | yuuta | (~YuutaW@mail.yuuta.moe) |
| 2024-04-16 04:34:42 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-16 04:36:17 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) (Ping timeout: 272 seconds) |
| 2024-04-16 04:37:31 +0200 | as_ | (~as@2800:a4:307:6f00:2530:9589:e186:2373) (Quit: Leaving) |
| 2024-04-16 04:37:38 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-04-16 04:38:59 +0200 | mei | (~mei@user/mei) (Ping timeout: 264 seconds) |
| 2024-04-16 04:39:03 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-16 04:39:29 +0200 | mei | (~mei@user/mei) |
| 2024-04-16 04:43:39 +0200 | yuuta | (~YuutaW@mail.yuuta.moe) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-16 04:44:58 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) |
| 2024-04-16 04:45:10 +0200 | td_ | (~td@i53870931.versanet.de) (Ping timeout: 255 seconds) |
| 2024-04-16 04:46:52 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-04-16 04:46:52 +0200 | td_ | (~td@i53870911.versanet.de) |
| 2024-04-16 04:59:02 +0200 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 2024-04-16 05:00:08 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-04-16 05:00:21 +0200 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-04-16 05:02:33 +0200 | mei | (~mei@user/mei) |
| 2024-04-16 05:09:44 +0200 | peterbecich | (~Thunderbi@47.229.123.186) |
| 2024-04-16 05:11:45 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2024-04-16 05:13:00 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 260 seconds) |
| 2024-04-16 05:16:39 +0200 | peterbecich | (~Thunderbi@47.229.123.186) (Ping timeout: 256 seconds) |
| 2024-04-16 05:19:11 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:bc1:a006:8998:5e0a:9eb8:f34d) |
| 2024-04-16 05:37:15 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 05:39:27 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-16 05:43:46 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 2024-04-16 05:53:22 +0200 | peterbecich | (~Thunderbi@47.229.123.186) |
| 2024-04-16 05:59:44 +0200 | aforemny | (~aforemny@i59F516ED.versanet.de) |
| 2024-04-16 06:00:54 +0200 | aforemny_ | (~aforemny@2001:9e8:6cdd:b100:9200:9bf0:8eb2:3efb) (Ping timeout: 256 seconds) |
| 2024-04-16 06:03:25 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2024-04-16 06:05:31 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) (Ping timeout: 256 seconds) |
| 2024-04-16 06:06:40 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) |
| 2024-04-16 06:13:19 +0200 | michalz | (~michalz@185.246.207.215) |
| 2024-04-16 06:29:37 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 2024-04-16 06:39:46 +0200 | kmein | (~weechat@user/kmein) (Ping timeout: 246 seconds) |
| 2024-04-16 06:42:01 +0200 | <jackdk> | monochrom: TI Extended BASIC extended its `CALL` instruction to support calling into user-defined subprograms with arguments, including parameter passing |
| 2024-04-16 06:45:39 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 252 seconds) |
| 2024-04-16 06:53:40 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) |
| 2024-04-16 07:00:19 +0200 | kmein | (~weechat@user/kmein) |
| 2024-04-16 07:00:52 +0200 | <mauke> | "You need at least parameter passing to make recursion useful." <- not really. you do need per-call storage ("activation frame"?), though, especially for the return address |
| 2024-04-16 07:01:31 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-04-16 07:01:38 +0200 | <mauke> | but parameter/return value passing can be emulated with globals |
| 2024-04-16 07:02:23 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 264 seconds) |
| 2024-04-16 07:03:13 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 246 seconds) |
| 2024-04-16 07:07:08 +0200 | danza | (~francesco@ba-19-155-176.service.infuturo.it) |
| 2024-04-16 07:14:57 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 07:17:42 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 2024-04-16 07:19:28 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 260 seconds) |
| 2024-04-16 07:21:31 +0200 | euleritian | (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) |
| 2024-04-16 07:22:51 +0200 | peterbecich | (~Thunderbi@47.229.123.186) (Ping timeout: 272 seconds) |
| 2024-04-16 07:25:16 +0200 | philopsos | (~caecilius@user/philopsos) |
| 2024-04-16 07:30:03 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-04-16 07:36:20 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-04-16 07:38:46 +0200 | xdminsy | (~xdminsy@117.147.70.203) |
| 2024-04-16 07:40:55 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 07:46:56 +0200 | zetef | (~quassel@5.2.182.99) |
| 2024-04-16 07:51:57 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 07:53:37 +0200 | <monochrom> | Activation frames are the low-level reduce-everything-to-von-Neumann-model view. I take the high-level everything-serves-to-realize-lambda-caluclus view. It's parameter passing at that level. |
| 2024-04-16 08:00:14 +0200 | mima | (~mmh@aftr-62-216-211-171.dynamic.mnet-online.de) |
| 2024-04-16 08:00:47 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 08:21:01 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-04-16 08:29:25 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) |
| 2024-04-16 08:32:16 +0200 | danza | (~francesco@ba-19-155-176.service.infuturo.it) (Ping timeout: 260 seconds) |
| 2024-04-16 08:34:12 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2024-04-16 08:34:59 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-04-16 08:37:03 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) (Quit: Leaving) |
| 2024-04-16 08:37:26 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-04-16 08:40:28 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 08:42:42 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-04-16 08:43:16 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-04-16 08:51:18 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) (Ping timeout: 250 seconds) |
| 2024-04-16 08:53:12 +0200 | kraftwerk28 | (~kraftwerk@164.92.219.160) (Quit: *disconnects*) |
| 2024-04-16 08:54:50 +0200 | ACuriousMoose | (~ACuriousM@142.166.18.53) (Ping timeout: 256 seconds) |
| 2024-04-16 08:55:21 +0200 | zetef | (~quassel@5.2.182.99) (Ping timeout: 255 seconds) |
| 2024-04-16 08:55:30 +0200 | ACuriousMoose | (~ACuriousM@142.68.181.38) |
| 2024-04-16 08:56:58 +0200 | acidjnk | (~acidjnk@p200300d6e714dc20691c30fd92f896ed.dip0.t-ipconnect.de) |
| 2024-04-16 09:05:15 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-04-16 09:05:44 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-04-16 09:07:59 +0200 | jle` | (~jle`@2603-8001-3b02-84d4-a77f-f741-f7ec-5267.res6.spectrum.com) (Ping timeout: 256 seconds) |
| 2024-04-16 09:08:48 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:9428:fb32:50c:b0cc) |
| 2024-04-16 09:13:25 +0200 | jamesmartinez | (uid6451@id-6451.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-04-16 09:15:49 +0200 | zetef | (~quassel@5.2.182.99) |
| 2024-04-16 09:20:06 +0200 | euleritian | (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-16 09:20:23 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-16 09:22:01 +0200 | rosco | (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) (Ping timeout: 256 seconds) |
| 2024-04-16 09:22:45 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 09:29:47 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 2024-04-16 09:29:47 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-04-16 09:35:26 +0200 | vglfr | (~vglfr@185.124.31.142) |
| 2024-04-16 09:40:43 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-04-16 09:43:06 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-04-16 09:44:12 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-04-16 09:47:42 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-16 09:51:15 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2024-04-16 09:53:14 +0200 | euleritian | (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) |
| 2024-04-16 09:57:10 +0200 | euleritian | (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-16 09:57:12 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Ping timeout: 260 seconds) |
| 2024-04-16 09:57:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-16 09:58:03 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) |
| 2024-04-16 09:58:04 +0200 | vglfr | (~vglfr@185.124.31.142) (Read error: Connection reset by peer) |
| 2024-04-16 09:58:23 +0200 | vglfr | (~vglfr@158.red-81-45-80.staticip.rima-tde.net) |
| 2024-04-16 09:59:57 +0200 | cheater | (~Username@user/cheater) (Read error: Connection reset by peer) |
| 2024-04-16 10:00:23 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) |
| 2024-04-16 10:00:46 +0200 | cheater | (~Username@user/cheater) |
| 2024-04-16 10:02:04 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) (Remote host closed the connection) |
| 2024-04-16 10:02:29 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) |
| 2024-04-16 10:17:27 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-04-16 10:18:49 +0200 | zetef | (~quassel@5.2.182.99) (Ping timeout: 256 seconds) |
| 2024-04-16 10:23:59 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 10:26:28 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-04-16 10:27:45 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-04-16 10:33:58 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-04-16 10:34:22 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-04-16 10:44:53 +0200 | zetef | (~quassel@5.2.182.99) |
| 2024-04-16 10:45:14 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2024-04-16 10:47:59 +0200 | mima | (~mmh@aftr-62-216-211-171.dynamic.mnet-online.de) (Ping timeout: 264 seconds) |
| 2024-04-16 10:49:24 +0200 | chele | (~chele@user/chele) |
| 2024-04-16 10:50:46 +0200 | ft | (~ft@p4fc2a20e.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-04-16 10:59:51 +0200 | JimL | (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-04-16 11:05:18 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:5592:43e9:751e:c0fc) |
| 2024-04-16 11:05:18 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:5592:43e9:751e:c0fc) (Changing host) |
| 2024-04-16 11:05:18 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-04-16 11:12:59 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-04-16 11:13:08 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-16 11:20:33 +0200 | JimL | (~quassel@89.162.16.26) |
| 2024-04-16 11:22:38 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 11:25:35 +0200 | JimL | (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-04-16 11:25:52 +0200 | JimL | (~quassel@89.162.16.26) |
| 2024-04-16 11:28:06 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-04-16 11:30:32 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 11:31:21 +0200 | cfricke | (~cfricke@user/cfricke) (Client Quit) |
| 2024-04-16 11:32:20 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:1996:3c8e:f64b:a77b) |
| 2024-04-16 11:34:20 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-04-16 11:38:11 +0200 | anon1123 | anon8697 |
| 2024-04-16 11:38:43 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 255 seconds) |
| 2024-04-16 11:45:03 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Ping timeout: 272 seconds) |
| 2024-04-16 11:57:47 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-04-16 11:59:13 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2024-04-16 11:59:35 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-04-16 12:00:40 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-04-16 12:00:49 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2024-04-16 12:01:18 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-04-16 12:02:10 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 260 seconds) |
| 2024-04-16 12:03:21 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) |
| 2024-04-16 12:03:27 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:bc1:a006:8998:5e0a:9eb8:f34d) (Ping timeout: 260 seconds) |
| 2024-04-16 12:03:54 +0200 | tv | (~tv@user/tv) (Ping timeout: 255 seconds) |
| 2024-04-16 12:04:06 +0200 | zetef | (~quassel@5.2.182.99) (Ping timeout: 252 seconds) |
| 2024-04-16 12:06:52 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) |
| 2024-04-16 12:10:53 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 240 seconds) |
| 2024-04-16 12:17:05 +0200 | tv | (~tv@user/tv) |
| 2024-04-16 12:19:21 +0200 | zetef | (~quassel@5.2.182.99) |
| 2024-04-16 12:26:34 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) (Remote host closed the connection) |
| 2024-04-16 12:29:12 +0200 | <masaeedu> | the `base` and `directory` packages use a definition of `FilePath` that is `FilePath = String`. in the `filepath` package these are referred to as "legacy filepaths", and it recommends migrating to using its new `OsPath` representation because "it is more correct. is there an equivalent of the `directory` package that works with `OsPath`s? |
| 2024-04-16 12:34:46 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) |
| 2024-04-16 12:35:03 +0200 | Inst | (~Inst@user/Inst) (Read error: Connection reset by peer) |
| 2024-04-16 12:37:19 +0200 | <masaeedu> | there's also `RawFilePath = ByteString` from `unix`... |
| 2024-04-16 12:38:36 +0200 | <jackdk> | Not sure, but I am also aware of `path-io`, but I haven't considered its relative merits vs. `OsPath` |
| 2024-04-16 12:39:15 +0200 | <haskellbridge> | <o​rbicularis> reminder this exists https://godbolt.org/noscript/haskell |
| 2024-04-16 12:39:49 +0200 | <haskellbridge> | <o​rbicularis> i wish it had more IR and so on |
| 2024-04-16 12:40:03 +0200 | <haskellbridge> | <o​rbicularis> like it would be super cool to have a version of this on steroids |
| 2024-04-16 12:40:36 +0200 | <haskellbridge> | <o​rbicularis> takes a cabal package in, compiles it in various GHC's and with various cabal.project's, compares them, runs benchmarks and compares those too, etc |
| 2024-04-16 12:40:53 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) (Ping timeout: 240 seconds) |
| 2024-04-16 12:41:00 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 2024-04-16 12:41:51 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) |
| 2024-04-16 12:42:35 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-04-16 12:45:21 +0200 | zetef | (~quassel@5.2.182.99) (Remote host closed the connection) |
| 2024-04-16 12:46:09 +0200 | zetef | (~quassel@5.2.182.99) |
| 2024-04-16 12:53:31 +0200 | destituion | (~destituio@2a02:2121:107:22da:94a0:4297:56fa:10c9) (Ping timeout: 256 seconds) |
| 2024-04-16 12:55:49 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) (Read error: Connection reset by peer) |
| 2024-04-16 12:55:56 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) (Ping timeout: 268 seconds) |
| 2024-04-16 12:56:11 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) |
| 2024-04-16 13:04:41 +0200 | xff0x | (~xff0x@2405:6580:b080:900:64dd:977c:c397:439c) |
| 2024-04-16 13:06:12 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-04-16 13:06:27 +0200 | danse-nr3 | (~danse-nr3@151.37.230.221) (Remote host closed the connection) |
| 2024-04-16 13:06:51 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-16 13:07:26 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) |
| 2024-04-16 13:08:04 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 2024-04-16 13:08:35 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) |
| 2024-04-16 13:14:59 +0200 | zetef | (~quassel@5.2.182.99) (Ping timeout: 272 seconds) |
| 2024-04-16 13:15:02 +0200 | Inst | (~Inst@user/Inst) |
| 2024-04-16 13:16:32 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) (Remote host closed the connection) |
| 2024-04-16 13:17:27 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 2024-04-16 13:17:49 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 2024-04-16 13:18:49 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3240-dc75-0888-f0c5-8353-6a7e.rev.sfr.net) |
| 2024-04-16 13:19:56 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) |
| 2024-04-16 13:20:18 +0200 | masaeedu | (~masaeedu@user/masaeedu) (Ping timeout: 268 seconds) |
| 2024-04-16 13:24:47 +0200 | constxd | (~constxd@user/constxd) |
| 2024-04-16 13:24:53 +0200 | <constxd> | lads |
| 2024-04-16 13:24:59 +0200 | <constxd> | https://www.cambridge.org/core/journals/journal-of-functional-programming/article/knuthmorrispratt… |
| 2024-04-16 13:25:30 +0200 | <constxd> | if you scroll down a bit to the `verticalSet` function definition |
| 2024-04-16 13:26:30 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 2024-04-16 13:26:32 +0200 | <constxd> | am i missing something or should it say ([x] `isPrefixOf`) instead of (isPrefixOf [x]) |
| 2024-04-16 13:29:03 +0200 | <constxd> | (isPrefixOf [x]) seems like it will only ever match [] or [x] |
| 2024-04-16 13:30:05 +0200 | <[Leary]> | constxd: They're the same thing, the first is just clearer in its meaning. |
| 2024-04-16 13:30:47 +0200 | <constxd> | oh right lol |
| 2024-04-16 13:31:12 +0200 | <constxd> | (isPrefixOf [x]) does not mean what you'd think it means if you read it out loud |
| 2024-04-16 13:31:35 +0200 | <constxd> | thanks i thought i was going crazy |
| 2024-04-16 13:34:46 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 2024-04-16 13:39:50 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 2024-04-16 13:40:59 +0200 | zetef | (~quassel@5.2.182.99) |
| 2024-04-16 13:41:33 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 2024-04-16 13:46:35 +0200 | puke | (~puke@user/puke) (Ping timeout: 260 seconds) |
| 2024-04-16 13:47:08 +0200 | puke | (~puke@user/puke) |
| 2024-04-16 13:48:46 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) |
| 2024-04-16 13:50:01 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 2024-04-16 13:50:33 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 2024-04-16 13:58:45 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-04-16 13:58:46 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 2024-04-16 14:00:58 +0200 | zetef | (~quassel@5.2.182.99) (Remote host closed the connection) |
| 2024-04-16 14:01:35 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2024-04-16 14:02:05 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-04-16 14:04:23 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Client Quit) |
| 2024-04-16 14:06:14 +0200 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 2024-04-16 14:11:43 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 256 seconds) |
| 2024-04-16 14:12:40 +0200 | danse-nr3 | (~danse-nr3@151.35.170.130) |
| 2024-04-16 14:13:22 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3240-dc75-0888-f0c5-8353-6a7e.rev.sfr.net) (Remote host closed the connection) |
| 2024-04-16 14:13:34 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2024-04-16 14:17:16 +0200 | danse-nr3 | (~danse-nr3@151.35.170.130) (Remote host closed the connection) |
| 2024-04-16 14:21:09 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Ping timeout: 255 seconds) |
| 2024-04-16 14:23:51 +0200 | danse-nr3 | (~danse-nr3@151.35.170.130) |
| 2024-04-16 14:26:38 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 14:26:48 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 14:31:53 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-04-16 14:37:24 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 14:37:25 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 14:42:32 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Remote host closed the connection) |
| 2024-04-16 14:42:49 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-04-16 14:52:31 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 15:03:04 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-04-16 15:03:54 +0200 | n8n | (n8n@user/n8n) (Quit: WeeChat 4.2.2) |
| 2024-04-16 15:05:30 +0200 | mei | (~mei@user/mei) |
| 2024-04-16 15:05:44 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 15:09:33 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 15:12:53 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2024-04-16 15:13:12 +0200 | euleritian | (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) |
| 2024-04-16 15:13:13 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 15:14:29 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-04-16 15:14:47 +0200 | Guest3 | (~Guest3@2400:1a00:bd11:3bf8:2e0:4cff:fefc:a34d) |
| 2024-04-16 15:14:47 +0200 | Guest3 | (~Guest3@2400:1a00:bd11:3bf8:2e0:4cff:fefc:a34d) (Client Quit) |
| 2024-04-16 15:18:44 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-04-16 15:19:23 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 15:23:15 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 2024-04-16 15:23:21 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 15:25:51 +0200 | mima | (~mmh@aftr-62-216-211-171.dynamic.mnet-online.de) |
| 2024-04-16 15:27:43 +0200 | euleritian | (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-16 15:28:00 +0200 | euleritian | (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) |
| 2024-04-16 15:29:12 +0200 | euleritian | (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-16 15:29:29 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-16 15:31:29 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 15:37:24 +0200 | <danse-nr3> | <3 ghcup |
| 2024-04-16 15:37:25 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 15:44:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 2024-04-16 15:45:39 +0200 | euleritian | (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) |
| 2024-04-16 15:47:47 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 15:53:04 +0200 | causal | (~eric@50.35.88.207) (Quit: WeeChat 4.1.1) |
| 2024-04-16 15:53:33 +0200 | qqq | (~qqq@92.43.167.61) (Quit: Lost terminal) |
| 2024-04-16 15:57:39 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 15:58:15 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-04-16 15:59:43 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 16:03:46 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 16:09:29 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 16:10:22 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-04-16 16:10:49 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 2024-04-16 16:10:56 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 16:14:19 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-16 16:14:49 +0200 | danse-nr3 | (~danse-nr3@151.35.170.130) (Ping timeout: 246 seconds) |
| 2024-04-16 16:15:11 +0200 | noumenon | (~noumenon@113.51-175-156.customer.lyse.net) |
| 2024-04-16 16:15:47 +0200 | rosco | (~rosco@2001:240:242f:d6eb:22d4:a19b:ae5c:b29d) |
| 2024-04-16 16:18:03 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 16:20:16 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 16:20:56 +0200 | qqq | (~qqq@92.43.167.61) |
| 2024-04-16 16:27:48 +0200 | danse-nr3 | (~danse-nr3@151.35.170.130) |
| 2024-04-16 16:28:04 +0200 | <Inst> | with Cont monad |
| 2024-04-16 16:28:38 +0200 | <Inst> | *> / >> is just, have the next line take its previous line as a continuation? |
| 2024-04-16 16:29:21 +0200 | <Inst> | a >> b, b is the continuation of a? |
| 2024-04-16 16:29:28 +0200 | <Inst> | but that's also interesting, there's also a backwards cont monad :3 |
| 2024-04-16 16:29:40 +0200 | masaeedu | (~masaeedu@user/masaeedu) |
| 2024-04-16 16:30:17 +0200 | <Inst> | and discarding the result of the previous cont monad? |
| 2024-04-16 16:30:24 +0200 | <Inst> | *cont monadic value, sigh |
| 2024-04-16 16:31:35 +0200 | <Inst> | besides AccumT, SelectT, and ContT, are there any important monads to know about? |
| 2024-04-16 16:32:00 +0200 | <Inst> | Monad zoo is, afaik, Maybe / Either, IO, State, Reader, Writer, List / List-like |
| 2024-04-16 16:33:01 +0200 | <Inst> | Identity, ST is just IO rigged up to give access to STRef and no other IO |
| 2024-04-16 16:33:02 +0200 | <raehik> | If I want to do error handling in type-level functions, there's no way around doing a bunch of manual Either wrappers, right? |
| 2024-04-16 16:33:37 +0200 | <raehik> | (use case, these functions return TypeError on failures, but that results in non-pretty errors at usage sites) |
| 2024-04-16 16:45:46 +0200 | Arsen | (~arsen@gentoo/developer/managarm.dev.Arsen) (Quit: Quit.) |
| 2024-04-16 16:47:57 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 16:50:21 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 2024-04-16 16:51:27 +0200 | <EvanR> | you mean, you want type level do-notation? |
| 2024-04-16 16:54:27 +0200 | Arsen | (~arsen@gentoo/developer/managarm.dev.Arsen) |
| 2024-04-16 17:01:42 +0200 | euleritian | (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-16 17:01:59 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-16 17:02:27 +0200 | guygastineau | (~guygastin@137.184.131.156) (Quit: ZNC - https://znc.in) |
| 2024-04-16 17:02:53 +0200 | <dmj`> | Inst: (->) and (,) |
| 2024-04-16 17:04:18 +0200 | <Inst> | (->) is just exotic manipulation of functions for reader, iirc, <*> is used as a gimmick to golf function application, as is join, and I was told not to use it because most people don't know the trick |
| 2024-04-16 17:04:45 +0200 | <Inst> | in the same way, say, uncurry (*>) (a,b) is smelly |
| 2024-04-16 17:05:16 +0200 | <Inst> | erm, uncurry ($>) (a, functor b) |
| 2024-04-16 17:05:20 +0200 | RMSBach | (~guygastin@137.184.131.156) |
| 2024-04-16 17:05:27 +0200 | JeremyB99 | (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 2024-04-16 17:07:24 +0200 | <Inst> | (,) primitive writer monad |
| 2024-04-16 17:09:09 +0200 | <Inst> | (,(,)) etc is fun, albeit unergonomic, and (,) iirc space leaks as non-CPS writer monads leak |
| 2024-04-16 17:09:44 +0200 | <Inst> | (,) also has a monoid instance, awesome |
| 2024-04-16 17:11:29 +0200 | <Inst> | (a :: a -> b -> c) <*> (b :: a -> b) = \u -> a u (b u) iirc |
| 2024-04-16 17:14:05 +0200 | <Inst> | but honestly <$> isn't that useless when it comes to function types, since <$> has a lower precedence than ., so it might come in handy |
| 2024-04-16 17:14:38 +0200 | <Inst> | i would like some help, though, with the weirdness of liftIO |
| 2024-04-16 17:15:00 +0200 | <Inst> | oh, I think I understand now |
| 2024-04-16 17:15:02 +0200 | <Inst> | https://hackage.haskell.org/package/transformers-0.6.1.1/docs/src/Control.Monad.Trans.Maybe.html#M… |
| 2024-04-16 17:15:20 +0200 | <Inst> | the first liftIO just ids on an IO type, then lifts into the monad transformer |
| 2024-04-16 17:16:12 +0200 | <raehik> | EvanR: sure, or any libraries that might support a similar pattern |
| 2024-04-16 17:16:59 +0200 | <raehik> | (I am thinking purely of the latter) |
| 2024-04-16 17:18:19 +0200 | <EvanR> | using operators instead of do notation turns out to not harm the syntax much |
| 2024-04-16 17:20:23 +0200 | <EvanR> | but you can't do lambda at type level |
| 2024-04-16 17:20:26 +0200 | eron | (~eron@168.196.116.143) |
| 2024-04-16 17:20:53 +0200 | <EvanR> | (in haskell) |
| 2024-04-16 17:21:47 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 17:24:49 +0200 | eron | (~eron@168.196.116.143) (Client Quit) |
| 2024-04-16 17:29:58 +0200 | qqq | (~qqq@92.43.167.61) (Read error: Connection reset by peer) |
| 2024-04-16 17:30:46 +0200 | qqq | (~qqq@92.43.167.61) |
| 2024-04-16 17:31:54 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds) |
| 2024-04-16 17:35:52 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 17:37:20 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 2024-04-16 17:37:29 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 17:38:09 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 17:38:53 +0200 | <Inst> | this is now in... https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/required_type_arguments.html#:~:text=A%20r… |
| 2024-04-16 17:39:12 +0200 | <Inst> | I suspect there's fundamental reasons type lambdas won't be included, but one day... your types will be written in do notation! |
| 2024-04-16 17:40:02 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 17:41:19 +0200 | <cheater> | so what would a simple type look like in do notation? |
| 2024-04-16 17:41:29 +0200 | <cheater> | like foo :: Bar -> Baz -> Quux |
| 2024-04-16 17:41:40 +0200 | <cheater> | what does that look like in do notation? |
| 2024-04-16 17:41:52 +0200 | <EvanR> | in haskell there's this thing where you want the type checker to work automatically without human interaction at some point, and lambdas mess that up |
| 2024-04-16 17:42:44 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 17:42:58 +0200 | <EvanR> | cheater, imagine datakinds, where the constructors of a type like Either are promoted to types themselves |
| 2024-04-16 17:43:17 +0200 | <EvanR> | function types are not a good example for this |
| 2024-04-16 17:43:19 +0200 | <cheater> | unable to |
| 2024-04-16 17:43:30 +0200 | JuanDaugherty | Lycurgus |
| 2024-04-16 17:43:48 +0200 | Lycurgus | (~juan@user/JuanDaugherty) (Changing host) |
| 2024-04-16 17:43:48 +0200 | Lycurgus | (~juan@user/Lycurgus) |
| 2024-04-16 17:43:51 +0200 | kimiamania | (~671c7418@user/kimiamania) (Quit: PegeLinux) |
| 2024-04-16 17:44:29 +0200 | EvanR | (~EvanR@user/evanr) (Quit: Leaving) |
| 2024-04-16 17:44:36 +0200 | kimiamania | (~76637481@user/kimiamania) |
| 2024-04-16 17:45:23 +0200 | kimiamania | (~76637481@user/kimiamania) (Client Quit) |
| 2024-04-16 17:45:28 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 255 seconds) |
| 2024-04-16 17:47:58 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 17:48:42 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 17:49:02 +0200 | kimiamania | (~76637481@user/kimiamania) |
| 2024-04-16 17:50:15 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 17:50:45 +0200 | EvanR | (~EvanR@user/evanr) |
| 2024-04-16 17:50:58 +0200 | nschoe | (~nschoe@2a01:e0a:8e:a190:aa00:da1d:4eed:33ec) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-16 17:51:15 +0200 | nschoe | (~nschoe@2a01:e0a:8e:a190:1a14:5923:b0ce:d13e) |
| 2024-04-16 17:53:21 +0200 | <Inst> | cheater: (do Bar) -> do foo <- Baz; Quux foo? |
| 2024-04-16 17:53:41 +0200 | <cheater> | i don't know |
| 2024-04-16 17:53:46 +0200 | <cheater> | are you asking me? |
| 2024-04-16 17:54:00 +0200 | <Inst> | It's a suggestion |
| 2024-04-16 17:54:20 +0200 | <Inst> | actually, that doesn't even work out |
| 2024-04-16 17:54:20 +0200 | <Inst> | :( |
| 2024-04-16 17:54:41 +0200 | <Inst> | would be closer to |
| 2024-04-16 17:54:43 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-04-16 17:54:54 +0200 | <Inst> | ehhh, probably not |
| 2024-04-16 17:55:09 +0200 | <Inst> | I am really not versed on dependent types |
| 2024-04-16 17:55:43 +0200 | <Inst> | but how far does -XRequiredTypeArguments bring us to DTs? |
| 2024-04-16 17:59:24 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 255 seconds) |
| 2024-04-16 18:00:03 +0200 | Lycurgus | (~juan@user/Lycurgus) (Quit: Lycurgus) |
| 2024-04-16 18:01:28 +0200 | <ncf> | sounds like it has nothing to do with it |
| 2024-04-16 18:01:36 +0200 | <ncf> | this is just a matter of implicit vs explicit? |
| 2024-04-16 18:02:44 +0200 | esph | (~weechat@user/esph) (Ping timeout: 268 seconds) |
| 2024-04-16 18:03:21 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 18:03:29 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2024-04-16 18:04:08 +0200 | haocrcmt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 2024-04-16 18:04:14 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 18:04:16 +0200 | danse-nr3 | (~danse-nr3@151.35.170.130) (Ping timeout: 268 seconds) |
| 2024-04-16 18:05:27 +0200 | <raehik> | Inst: no closer, it's just handy for certain type-to-term code |
| 2024-04-16 18:05:47 +0200 | <Inst> | it's technically bringing type level down to term level |
| 2024-04-16 18:06:11 +0200 | <raehik> | sometimes you still need to use Proxy#, but in many cases where you're spamming TypeApplications, RequiredTypeArguments can simplify your syntax |
| 2024-04-16 18:06:20 +0200 | <Inst> | also, iirc, my usage of typeapplications has been wonky :( |
| 2024-04-16 18:06:23 +0200 | <raehik> | (and clarify how functions should be used) |
| 2024-04-16 18:06:23 +0200 | <ncf> | no it's not?? it's just syntax |
| 2024-04-16 18:06:57 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 18:07:00 +0200 | <raehik> | Inst: it might appear so but it's really just a special way to specify typevars in a function! |
| 2024-04-16 18:07:29 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-04-16 18:09:41 +0200 | <Inst> | I guess, you still have (a :: Type), and I mean the only time I think without typeclasses you can do something wonky with generic output types (without typeclass restrictions) is unsafeCoerce, which in my experience, is a great way to get segfaults |
| 2024-04-16 18:09:42 +0200 | <Inst> | <3 |
| 2024-04-16 18:11:30 +0200 | euphores | (~SASL_euph@user/euphores) (Client Quit) |
| 2024-04-16 18:11:45 +0200 | <raehik> | (typeclasses can be polymorphic over kind btw) |
| 2024-04-16 18:11:49 +0200 | <raehik> | https://github.com/raehik/binrep/blob/8d10873c0416e8785e55c205559a8c0b0ade05ae/src/Binrep/BLen.hs#… |
| 2024-04-16 18:12:02 +0200 | <Inst> | erm, should have done a :: type |
| 2024-04-16 18:12:38 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 18:16:48 +0200 | esph | (~weechat@user/esph) |
| 2024-04-16 18:17:59 +0200 | <raehik> | i didn't realize for a very long time GHC is auto-polymorphic on typeclass args |
| 2024-04-16 18:18:05 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 2024-04-16 18:18:31 +0200 | <raehik> | since if you ever use it concretely it's forced to a Type. it just magically works out when you want a kind-polymorphic typeclass |
| 2024-04-16 18:18:44 +0200 | <Inst> | also wtf |
| 2024-04-16 18:19:05 +0200 | <Inst> | instance GenericFoldMap BLen where |
| 2024-04-16 18:19:11 +0200 | <Inst> | a class is an instance of a class? |
| 2024-04-16 18:19:37 +0200 | <raehik> | yeah xD since `BLen :: Type -> Constraint`! |
| 2024-04-16 18:19:59 +0200 | greenflower | (~greenflow@2409:4071:4d4b:d3ae:27cf:a6f5:bf97:a564) |
| 2024-04-16 18:19:59 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-04-16 18:20:12 +0200 | <raehik> | and GenericFoldMap only uses its type as a tag/index, never instantiates it, so it can be any kind haha |
| 2024-04-16 18:22:17 +0200 | Inst | 's brain explodes |
| 2024-04-16 18:22:28 +0200 | <Inst> | phantom-typed typeclasses |
| 2024-04-16 18:23:02 +0200 | <raehik> | pretty much exactly where you'd want RequiredTypeArguments, because they're inherently ambiguous |
| 2024-04-16 18:23:32 +0200 | <Inst> | the typedef inside the instance dec is also blowing my mind |
| 2024-04-16 18:23:43 +0200 | <Inst> | what don't I know about typeclasses and instances (without extensions)? |
| 2024-04-16 18:23:46 +0200 | <Inst> | probably a hell of a lot :( |
| 2024-04-16 18:24:00 +0200 | <raehik> | That's an associated type family. Nothing special, just a type family that belongs to a class |
| 2024-04-16 18:24:09 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Ping timeout: 252 seconds) |
| 2024-04-16 18:24:42 +0200 | <Inst> | oh, so it's defined as a type family |
| 2024-04-16 18:24:53 +0200 | <Inst> | i got confused because i didn't see any extensions on top |
| 2024-04-16 18:25:16 +0200 | <raehik> | I use a long list of default extensions (i am one of "those" haskellers) |
| 2024-04-16 18:29:06 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-04-16 18:32:53 +0200 | <kuribas> | Who doesn't? |
| 2024-04-16 18:33:12 +0200 | greenflower | (~greenflow@2409:4071:4d4b:d3ae:27cf:a6f5:bf97:a564) (Quit: Client closed) |
| 2024-04-16 18:34:00 +0200 | vglfr | (~vglfr@158.red-81-45-80.staticip.rima-tde.net) (Ping timeout: 256 seconds) |
| 2024-04-16 18:34:02 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 2024-04-16 18:34:45 +0200 | <raehik> | I wouldn't know since any codebase I tread I leave behind a wake of GHC2021 and more >:) |
| 2024-04-16 18:34:57 +0200 | vglfr | (~vglfr@185.124.31.115) |
| 2024-04-16 18:35:11 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 2024-04-16 18:40:47 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-04-16 18:41:45 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 18:44:37 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) (Quit: Leaving) |
| 2024-04-16 18:45:28 +0200 | Core4466 | (~rosco@2001:240:242f:d6eb:20db:887f:8f97:4055) |
| 2024-04-16 18:48:22 +0200 | rosco | (~rosco@2001:240:242f:d6eb:22d4:a19b:ae5c:b29d) (Ping timeout: 268 seconds) |
| 2024-04-16 18:48:27 +0200 | Nixkernal | (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch) (Ping timeout: 255 seconds) |
| 2024-04-16 18:49:21 +0200 | Eoco | (~ian@128.101.131.218) (Ping timeout: 255 seconds) |
| 2024-04-16 18:49:55 +0200 | Eoco | (~ian@128.101.131.218) |
| 2024-04-16 18:51:58 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
| 2024-04-16 18:57:27 +0200 | Eoco | (~ian@128.101.131.218) (Remote host closed the connection) |
| 2024-04-16 18:58:05 +0200 | Eoco | (~ian@128.101.131.218) |
| 2024-04-16 18:58:16 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 19:02:02 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 19:02:23 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 264 seconds) |
| 2024-04-16 19:03:25 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 19:14:08 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 19:15:25 +0200 | vglfr | (~vglfr@185.124.31.115) (Read error: Connection reset by peer) |
| 2024-04-16 19:15:50 +0200 | vglfr | (~vglfr@139.47.115.46) |
| 2024-04-16 19:20:13 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 19:21:06 +0200 | ski | (~ski@ext-1-033.eduroam.chalmers.se) (Read error: Connection reset by peer) |
| 2024-04-16 19:22:43 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-04-16 19:23:11 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 19:25:31 +0200 | Inst | (~Inst@user/Inst) (Read error: Connection reset by peer) |
| 2024-04-16 19:26:33 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 2024-04-16 19:27:05 +0200 | <ph88> | Does someone know a good termination checker library? Not necessarily to check haskell itself, preferably language agnostic |
| 2024-04-16 19:30:13 +0200 | ski | (~ski@ext-1-033.eduroam.chalmers.se) |
| 2024-04-16 19:33:14 +0200 | Inst | (~Inst@user/Inst) |
| 2024-04-16 19:33:56 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 19:36:28 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 19:38:21 +0200 | <glguy> | Agda, Coq, Isabelle. Any interactive theorem prover is probably going to have something |
| 2024-04-16 19:44:41 +0200 | <Inst> | raehik: not sure if that's healthy, but I don't care that much anymore |
| 2024-04-16 19:44:46 +0200 | <Inst> | at least on Tiobe Haskell is clearly ahead of Scala |
| 2024-04-16 19:48:15 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 19:49:33 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 272 seconds) |
| 2024-04-16 19:50:36 +0200 | vglfr | (~vglfr@139.47.115.46) (Read error: Connection reset by peer) |
| 2024-04-16 19:50:50 +0200 | vglfr | (~vglfr@139.47.115.46) |
| 2024-04-16 19:51:00 +0200 | target_i | (~target_i@user/target-i/x-6023099) |
| 2024-04-16 19:51:38 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 19:51:46 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-04-16 19:52:39 +0200 | <ph88> | glguy, ye that's good though a bit hard to incorporate into another project i suppose |
| 2024-04-16 19:53:33 +0200 | <glguy> | Termination checking tends to depend deeply on the thing you're termination checking |
| 2024-04-16 19:53:45 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 19:54:05 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 19:54:10 +0200 | <glguy> | If you just want to check arbitrary properties, some of which might be termination variants that you're going to check, you might just want an SMT checker |
| 2024-04-16 19:56:15 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 2024-04-16 19:57:57 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-04-16 19:58:15 +0200 | euleritian | (~euleritia@dynamic-176-004-192-223.176.4.pool.telefonica.de) |
| 2024-04-16 20:00:09 +0200 | p3n | (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-16 20:00:13 +0200 | <ph88> | glguy, you mean like svb / z3 ? |
| 2024-04-16 20:00:25 +0200 | <glguy> | yeah |
| 2024-04-16 20:01:13 +0200 | <ph88> | glguy, how come the termination checking depend deeply on the thing you are checking? In general control flow of pretty much any programming language is very similar, where you enter/exit blocks of codes, branches and loops |
| 2024-04-16 20:01:30 +0200 | p3n | (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 2024-04-16 20:04:00 +0200 | euleritian | (~euleritia@dynamic-176-004-192-223.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-16 20:04:18 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-16 20:05:23 +0200 | <monochrom> | That is like what I saw in a math channel a long time ago. Someone asked "Hi how do I solve equations?" |
| 2024-04-16 20:05:41 +0200 | <glguy> | monochrom: was the answer also SMT? |
| 2024-04-16 20:05:41 +0200 | <monochrom> | Yeah, how do you solve equations? |
| 2024-04-16 20:06:15 +0200 | <monochrom> | No one answered. The asker eventually confessed they had merely things like "5x+4=6" in mind. |
| 2024-04-16 20:08:26 +0200 | <monochrom> | Or maybe I answered. "It depends on the equation." |
| 2024-04-16 20:08:50 +0200 | <monochrom> | No, I was not that kind. I answered "it is undecidable". |
| 2024-04-16 20:10:09 +0200 | ft | (~ft@p4fc2a20e.dip0.t-ipconnect.de) |
| 2024-04-16 20:11:35 +0200 | <monochrom> | Now, let's look at how that actually is equivalent to termination checking, even in practice, even bullet-point-by-bullet-point. |
| 2024-04-16 20:13:53 +0200 | <monochrom> | The most common cases that average programmers have in mind are like "for (i = 0; i < n; i++)". |
| 2024-04-16 20:14:24 +0200 | <dolio> | Well, all termination checkers report false results, yeah. |
| 2024-04-16 20:14:49 +0200 | <monochrom> | Without make it a really harder problem, it can be generalized linearly, e.g., "for (i = 4; i < n; i+=2)" is no more difficult. |
| 2024-04-16 20:15:10 +0200 | <glguy> | dolio: because all programs eventually terminate even if due to environmental factors? |
| 2024-04-16 20:15:22 +0200 | <monochrom> | That class just requires solving linear inequalities and is a solved problem. |
| 2024-04-16 20:15:34 +0200 | <c_wraith> | That usually terminates. if n is not the max int. and nothing in the loop body is mutating i or n. |
| 2024-04-16 20:15:45 +0200 | <dolio> | For an example of how it depends, Agda's current termination checker is based on the assumption that it is predicative. If you allow impredicative types (like, data types with quantifiers over all types in them), then it will tell you some non-terminating things are actually terminating. |
| 2024-04-16 20:16:17 +0200 | <c_wraith> | actually, I guess n being the max int *shouldn't* break that, since it's a < |
| 2024-04-16 20:16:39 +0200 | <dolio> | Because some of its, "this is a smaller value," inferences are wrong depending on how you instantiate the quantifier. |
| 2024-04-16 20:17:13 +0200 | <glguy> | c_wraith: the tricky case was n+=2, but even then we're still OK because it would be an invalid C program that tried to overflow the int, so we know there's some outer reason why n could never be so large |
| 2024-04-16 20:17:15 +0200 | <dolio> | So, you probably can't just use Agda's checker on GHC. |
| 2024-04-16 20:17:22 +0200 | <c_wraith> | glguy: hah |
| 2024-04-16 20:17:47 +0200 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 256 seconds) |
| 2024-04-16 20:17:48 +0200 | <monochrom> | But of course average programmers have seen nothing. There are times the conditions of the for loop requires solving quadratic inequalities instead. That is also solved now, but it requires a different algorithm from linear inequalities. |
| 2024-04-16 20:18:57 +0200 | <c_wraith> | monochrom: and imagine thinking like a C programmer trying to envision how to get something to prove their huffman tree construction terminates! |
| 2024-04-16 20:19:20 +0200 | <c_wraith> | (ok, you can cheat and know it needs n-1 merges and therefore use a for loop. but the naive while loop!) |
| 2024-04-16 20:19:55 +0200 | <monochrom> | Yeah, next up you don't have a for loop, you have a while loop that cannot be reduced to a for loop. You now require domain-specific knowledge. |
| 2024-04-16 20:21:20 +0200 | <EvanR> | ph88, and all languages where that is the case have undecidable termination checking, making the question super easy! |
| 2024-04-16 20:21:24 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 20:21:38 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 20:21:41 +0200 | <glguy> | I've seen code written by advanced programmers who were trying to make termination checking easy. No loops but pages of copy-pasted if statements |
| 2024-04-16 20:21:49 +0200 | <glguy> | or at least that's why I figure they were doing that |
| 2024-04-16 20:22:03 +0200 | <monochrom> | I have been teaching Prim's algorithm and Dijkstra's algorithm, which are of the form "while priority queue not empty, dequeue". Now someone has to hand-add an axiom "dequeue descreases size by 1" or else there is no reason why a checker knows that it terminates. |
| 2024-04-16 20:22:13 +0200 | <dolio> | Also, Agda is (hopefully) soon getting a new termination checker. But, the way it works involves knowing the details of (co)data types to determine what is a valid program. |
| 2024-04-16 20:22:46 +0200 | <EvanR> | if statements, with terminating condition, terminate. But also "for loop that does nothing but create another array based on this other array element by element i.e. map" |
| 2024-04-16 20:22:46 +0200 | <glguy> | dolio: doesn't the current checker rely on such properties of (co)data to do termination checking already? |
| 2024-04-16 20:22:52 +0200 | <dolio> | Because the way you handle finitary data is distinct from infinitary codata. |
| 2024-04-16 20:23:06 +0200 | <cheater> | glguy: no. it's loop unrolling. |
| 2024-04-16 20:23:16 +0200 | <c_wraith> | John Carmack had a blog post about rewriting his rocket control software into a form that had only a single loop, no function calls or macros, and only branched forward. He said it wasn't *great*, but it was really good for finding redundant code and forcing him to be very aware of obstacles to real-time functioning. |
| 2024-04-16 20:23:21 +0200 | <dolio> | glguy: Yeah, but the new one is better. |
| 2024-04-16 20:23:33 +0200 | <glguy> | cheater: you have to know how to write a loop to call what you're doing unrolling |
| 2024-04-16 20:23:57 +0200 | <cheater> | c_wraith: i do a similar thing when auditing software |
| 2024-04-16 20:24:02 +0200 | <cheater> | i forgot what i called it but |
| 2024-04-16 20:24:04 +0200 | <glguy> | dolio: any pointer you can recommend if I'm curious to see what changes are coming? |
| 2024-04-16 20:24:18 +0200 | <monochrom> | Oh next up is BFS and DFS! Take BFS for example. It does "while queue not empty: dequeue, but on some condition, add back a whole lot of things to the queue!" Now why doesn't it go on forever! |
| 2024-04-16 20:24:22 +0200 | <dolio> | glguy: https://github.com/agda/agda/pull/7152 |
| 2024-04-16 20:24:40 +0200 | <c_wraith> | monochrom: pfft. *my* BFS can run forever just fine! |
| 2024-04-16 20:24:47 +0200 | <monochrom> | haha |
| 2024-04-16 20:25:19 +0200 | <dolio> | In Haskell you have a problem because data and codata are the same, so how do you know when you're supposed to argue based on something being data vs. codata? |
| 2024-04-16 20:25:26 +0200 | <cheater> | you want to see the data path from a root call of some sort, to some important syscall/lib function call. so essentially you take a function you are calling, and you inline calls to all other functions, until you get to the syscall. then, you take all assumptions (like e.g. the if branch will take this branch and not that one) and you simplify and simplify until you're left with a single big "formula" for the final call (or as few formulas as possible) |
| 2024-04-16 20:25:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-16 20:25:59 +0200 | <cheater> | you prune calls to unimportant functions like eg logging |
| 2024-04-16 20:26:33 +0200 | <cheater> | you're left with the actual code of what's happening, hopefully limited to a single screen or two |
| 2024-04-16 20:27:13 +0200 | <glguy> | dolio: easy: there are two cases so you try one and then the other *nod* |
| 2024-04-16 20:27:24 +0200 | <EvanR> | data Program = Syscall Argument Program |
| 2024-04-16 20:27:27 +0200 | <c_wraith> | ... And then my coworker takes every line and puts it at a different place in an inheritance hierarchy before leaving the company. |
| 2024-04-16 20:28:20 +0200 | <cheater> | obviously |
| 2024-04-16 20:28:32 +0200 | <dolio> | Anyhow, that's why you use agda2hs. :Ăľ |
| 2024-04-16 20:28:42 +0200 | <cheater> | what about hs2agda? |
| 2024-04-16 20:29:41 +0200 | xdminsy | (~xdminsy@117.147.70.203) (Read error: Connection reset by peer) |
| 2024-04-16 20:32:02 +0200 | <ph88> | EvanR, where -what- exactly is the case? |
| 2024-04-16 20:33:06 +0200 | <ph88> | dolio, do you have a sources about Agda is (hopefully) soon getting a new termination checker ?? |
| 2024-04-16 20:33:26 +0200 | <dolio> | ph88: Yeah, see the issue I linked to glguy above. |
| 2024-04-16 20:33:28 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) |
| 2024-04-16 20:33:51 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Quit: segfaultfizzbuzz) |
| 2024-04-16 20:34:12 +0200 | <EvanR> | ph88, "every language is just block entry, block exit, function call, function return" |
| 2024-04-16 20:34:27 +0200 | <ph88> | dolio, thanks |
| 2024-04-16 20:35:01 +0200 | <ph88> | EvanR, ya sure but i like to know per block of code whether it terminates, not as a yes/no answer for an entire program |
| 2024-04-16 20:35:20 +0200 | <EvanR> | can blocks be nested? |
| 2024-04-16 20:35:24 +0200 | <cheater> | EvanR: why block entry. who are you trying to keep out |
| 2024-04-16 20:35:44 +0200 | <EvanR> | anyway, halting problems |
| 2024-04-16 20:35:49 +0200 | <ph88> | EvanR, not sure what you mean by nested. Blocks can be jumped from many other blocks and jump to many other blocks |
| 2024-04-16 20:35:56 +0200 | <cheater> | what's the deal with halting, anyways? |
| 2024-04-16 20:36:01 +0200 | <monochrom> | and why block exit, who are you trying to keep in! >:) |
| 2024-04-16 20:36:24 +0200 | <ph88> | termination checking is more difficult than the halting problem (according to wikipedia) yet there are termination checkers that can check things |
| 2024-04-16 20:36:52 +0200 | <EvanR> | it's much easier in languages which have sensible structure and not algol style |
| 2024-04-16 20:36:55 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-04-16 20:37:15 +0200 | sammelweis | (~quassel@96.76.243.253) (Ping timeout: 252 seconds) |
| 2024-04-16 20:37:15 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 2024-04-16 20:37:21 +0200 | <cheater> | i particularly love it when i'm talking about some specific technique that can work under specific circumstances and some n00b dances up and goes "bbb -b but halting problem! this cannot work in general" |
| 2024-04-16 20:37:40 +0200 | <cheater> | and then you have to have an hour long conversation about how they're missing imagination |
| 2024-04-16 20:38:02 +0200 | <dolio> | Termination checkers that actually get used rule out programs that actually halt, usually. |
| 2024-04-16 20:38:03 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 2024-04-16 20:38:05 +0200 | <cheater> | missing? lacking |
| 2024-04-16 20:38:06 +0200 | <EvanR> | you gotta think outside the box, and by outside the box, I mean within the constraints of the problem xD |
| 2024-04-16 20:38:16 +0200 | <cheater> | precisely. |
| 2024-04-16 20:38:30 +0200 | <cheater> | to think outside the box, first create a very tiny box, so tiny that only you can crawl into it. |
| 2024-04-16 20:38:43 +0200 | <cheater> | and within that tiny box, you are unbounded in your freedom. |
| 2024-04-16 20:38:47 +0200 | <EvanR> | lol |
| 2024-04-16 20:38:56 +0200 | <ph88> | dolio, that's fine when there are parts of the program that can not be checked in that way. It was never my requirement to get perfect checking of the entire program, only there where possible |
| 2024-04-16 20:38:57 +0200 | <dolio> | Like, in Agda's current checker, you can't write recursion over rose trees without inlining the definition of `map` on lists into your recursion. |
| 2024-04-16 20:39:11 +0200 | <monochrom> | Well the converse holds too. There are other noobs who can solve one special case and dances up and think it generalizes. |
| 2024-04-16 20:39:49 +0200 | <cheater> | stop throwing shade on AI |
| 2024-04-16 20:40:15 +0200 | <monochrom> | No I'm throwing shade on humanity itself. AIs are doing great. |
| 2024-04-16 20:40:20 +0200 | <cheater> | and that "Al", is he in the room with us right now? |
| 2024-04-16 20:40:26 +0200 | <ph88> | if one takes an SMT solver to check for termination (where possible) isn't that re-inventing the wheel when there are already full fledged termination checkers (for example the one in Agda) ? |
| 2024-04-16 20:41:01 +0200 | <EvanR> | I wonder if you can do a "who's on first" but with two people talking about AI and "Al" with bad fonts on IRC |
| 2024-04-16 20:41:48 +0200 | <cheater> | ph88: yes. in particular, any sufficiently complicated test suite contains an ad-hoc, informally-specified, bug-ridden, slow implementation of half of the haskell type system. |
| 2024-04-16 20:44:03 +0200 | <ph88> | my doubts are whether is should look for something out of the box, or create something myself on top of some smt checker or whatnot starting with the simple cases. At least with the smt checker i will be able to build up knowledge where as a checker as a library is difficult to grok when there are problems, but probably has superior results. Any advice ? |
| 2024-04-16 20:46:47 +0200 | <mauke> | https://www.youtube.com/watch?v=uq-gYOrU8bA |
| 2024-04-16 20:47:51 +0200 | <monochrom> | My advice is orthogonal. Whatever you pick up, you remember to ask what it cannot solve, and also ask its author what they never intend to solve. That way you may finally appreciate why some of us said "it depends", why "it depends" is the only correct answer to an underspecified "how to check termination" question. |
| 2024-04-16 20:51:14 +0200 | <cheater> | ph88: i would say grow with your checker |
| 2024-04-16 20:51:22 +0200 | <cheater> | trying to roll your own will teach you a lot of stuff |
| 2024-04-16 20:51:31 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-04-16 20:51:32 +0200 | <cheater> | you'll be able to appreciate more advanced tools better |
| 2024-04-16 20:51:47 +0200 | <ph88> | thanks monochrom , cheater |
| 2024-04-16 20:52:34 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) |
| 2024-04-16 20:53:00 +0200 | <masaeedu> | ph88: is your goal to implement termination checking for a language implemented in Haskell? |
| 2024-04-16 20:56:03 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 272 seconds) |
| 2024-04-16 20:57:01 +0200 | <probie> | Termination checking is simple: `terminates :: Program -> Bool; terminates _ = True` and just restrict `Program` to only be made up things which always terminate (e.g. primitive recursive functions) |
| 2024-04-16 20:57:04 +0200 | dcoutts | (~duncan@cpc69400-oxfd27-2-0-cust750.4-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2024-04-16 20:57:28 +0200 | <monochrom> | :( |
| 2024-04-16 20:58:10 +0200 | <monochrom> | But you can make it even better with "terminates :: Program -> ()" >:) |
| 2024-04-16 20:58:35 +0200 | <EvanR> | semi decidable |
| 2024-04-16 20:59:09 +0200 | <ph88> | masaeedu, ye |
| 2024-04-16 20:59:48 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 20:59:51 +0200 | <ph88> | probie, how do you know which things always terminate though? |
| 2024-04-16 21:00:09 +0200 | yeitrafferin | (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) (Quit: Leaving) |
| 2024-04-16 21:00:47 +0200 | <monochrom> | We know that primitive recursive functions terminate. We know that System F programs terminate. There are other examples. |
| 2024-04-16 21:01:09 +0200 | <monochrom> | We know that VCR programs terminate if you don't enable "repeat". |
| 2024-04-16 21:01:27 +0200 | <ph88> | VCR programs? |
| 2024-04-16 21:01:45 +0200 | <monochrom> | https://en.wikipedia.org/wiki/Videocassette_recorder |
| 2024-04-16 21:01:49 +0200 | <ph88> | lol |
| 2024-04-16 21:02:09 +0200 | <monochrom> | You can tell it "start recording on Tuesday 2PM-3PM" |
| 2024-04-16 21:02:27 +0200 | <ph88> | monochrom, what if i take my language, whatever i can convert to a terminating language (system F) i can say it terminates, and other things i can say "i don't know?" then maybe i don't need to do any checking and only converting |
| 2024-04-16 21:02:56 +0200 | <monochrom> | What if 99% of your actual programs convert to the unknown case? |
| 2024-04-16 21:03:52 +0200 | <monochrom> | Or you may reply "no, only 1%". |
| 2024-04-16 21:04:01 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-04-16 21:04:05 +0200 | <monochrom> | Either way, it again proves "it depends". |
| 2024-04-16 21:04:26 +0200 | <EvanR> | you could interpret the terminatingness using quantum mechanics |
| 2024-04-16 21:04:37 +0200 | <EvanR> | 99% terminating 1% not |
| 2024-04-16 21:04:39 +0200 | <probie> | That's an interesting spin on things |
| 2024-04-16 21:04:54 +0200 | <EvanR> | lol |
| 2024-04-16 21:04:58 +0200 | <monochrom> | haha |
| 2024-04-16 21:05:17 +0200 | <monochrom> | Was that "spin" intended pun? :) |
| 2024-04-16 21:05:45 +0200 | <ph88> | monochrom, i know there is a "a depends". I'm looking for the practical simplest approach to get going |
| 2024-04-16 21:05:57 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) (Ping timeout: 256 seconds) |
| 2024-04-16 21:06:05 +0200 | <probie> | yes, that was the intention |
| 2024-04-16 21:07:08 +0200 | <mauke> | charming |
| 2024-04-16 21:07:20 +0200 | <masaeedu> | ph88: a really simple solution is to simply banish direct recursion from your language. |
| 2024-04-16 21:08:27 +0200 | <masaeedu> | whether this is feasible depends on what your language is used for |
| 2024-04-16 21:08:34 +0200 | <masaeedu> | but e.g. Dhall uses this approach to great effect |
| 2024-04-16 21:08:53 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-16 21:09:01 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) |
| 2024-04-16 21:11:05 +0200 | <masaeedu> | you can still do recursive things, but it involves a bit of careful thinking and reformulation (often balanced by work you'd end up doing anyway to appease a termination checker) |
| 2024-04-16 21:12:36 +0200 | <ph88> | oh lambda cube, i saw that before ^^ |
| 2024-04-16 21:13:08 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 21:13:54 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) (Ping timeout: 268 seconds) |
| 2024-04-16 21:15:15 +0200 | <masaeedu> | yeah, Dhall implements a lot of really cool ideas |
| 2024-04-16 21:15:29 +0200 | <masaeedu> | in this case what's relevant is the absence of a feature |
| 2024-04-16 21:15:58 +0200 | <ph88> | related http://neilmitchell.blogspot.com/2020/11/turing-incomplete-languages.html |
| 2024-04-16 21:16:08 +0200 | <masaeedu> | i.e. you just can't do the direct recursion that makes termination checking necessary |
| 2024-04-16 21:17:26 +0200 | <monochrom> | I am not thrilled at guaranteed-termination languages in the context of "I want to learn/build termination checking"> |
| 2024-04-16 21:18:08 +0200 | <monochrom> | It is like "I'm interested in building a lie detector on one of those islands in logic puzzles where everyone on the island tells the truth always". |
| 2024-04-16 21:19:34 +0200 | <int-e> | . o O ( https://xkcd.com/246/ ) |
| 2024-04-16 21:20:12 +0200 | <masaeedu> | I'm not meaning to suggest you'd prohibit direct recursion and then build a termination checker anyway |
| 2024-04-16 21:21:15 +0200 | Rodney_ | (~Rodney@176.254.244.83) |
| 2024-04-16 21:21:53 +0200 | <masaeedu> | Only to say that, depending on your needs, you can go quite a long ways without direct recursion |
| 2024-04-16 21:23:52 +0200 | tv | (~tv@user/tv) (Ping timeout: 246 seconds) |
| 2024-04-16 21:25:43 +0200 | <masaeedu> | monochrom: that said, i probably didn't quite understand your comment. after all the OP's goal in adding a termination checker is to presumably to end up with a guaranteed-termination language. |
| 2024-04-16 21:28:09 +0200 | rosco | (~rosco@2001:240:242f:d6eb:ca19:e23f:936a:839f) |
| 2024-04-16 21:29:16 +0200 | <masaeedu> | the only question is how to limit the progam's use of direct recursion so that termination is still guaranteed. |
| 2024-04-16 21:29:26 +0200 | <masaeedu> | and the simplest limitation i can think of is to just ban it |
| 2024-04-16 21:30:46 +0200 | Core4466 | (~rosco@2001:240:242f:d6eb:20db:887f:8f97:4055) (Ping timeout: 256 seconds) |
| 2024-04-16 21:30:49 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 21:32:16 +0200 | dispater- | (~dispater@217.155.58.82) |
| 2024-04-16 21:32:45 +0200 | orcus | (~orcus@217.155.58.82) |
| 2024-04-16 21:35:10 +0200 | orcus | (~orcus@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 21:35:10 +0200 | dispater- | (~dispater@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 21:37:33 +0200 | tv | (~tv@user/tv) |
| 2024-04-16 21:38:19 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 21:38:37 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-04-16 21:39:41 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-04-16 21:41:45 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-04-16 21:41:47 +0200 | dcoutts | (~duncan@cpc69400-oxfd27-2-0-cust750.4-3.cable.virginm.net) |
| 2024-04-16 21:41:58 +0200 | dispater- | (~dispater@217.155.58.82) |
| 2024-04-16 21:42:25 +0200 | jinsun | (~jinsun@user/jinsun) (Read error: Connection reset by peer) |
| 2024-04-16 21:42:28 +0200 | orcus | (~orcus@217.155.58.82) |
| 2024-04-16 21:43:11 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 2024-04-16 21:44:09 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) |
| 2024-04-16 21:44:30 +0200 | <monochrom> | Or the goal is to learn termination checking. |
| 2024-04-16 21:46:43 +0200 | <masaeedu> | that could be. iirc they were asking for a library that implements termination checking that could be dropped into their project |
| 2024-04-16 21:46:59 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-04-16 21:47:12 +0200 | <monochrom> | Then perhaps too late to rewrite the project. |
| 2024-04-16 21:48:33 +0200 | cheater_ | (~Username@user/cheater) |
| 2024-04-16 21:48:52 +0200 | <monochrom> | But let's talk about interesting normal forms! |
| 2024-04-16 21:49:51 +0200 | cheater_ | (~Username@user/cheater) (Read error: Connection reset by peer) |
| 2024-04-16 21:50:04 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 256 seconds) |
| 2024-04-16 21:50:30 +0200 | <monochrom> | In recursion theory (the one where you draw a line between primitive recursive functions and other recursive functions), every function equals [unbounded] minimization over some primitive recursive function. (IIRC "Kleene recursion theorem") |
| 2024-04-16 21:50:35 +0200 | cheater_ | (~Username@user/cheater) |
| 2024-04-16 21:50:35 +0200 | cheater_ | cheater |
| 2024-04-16 21:52:26 +0200 | <monochrom> | In von Neumann computing, every program is interpreted by the CPU, i.e., one "simple" loop over a manifestly terminating loop body. |
| 2024-04-16 21:53:44 +0200 | <monochrom> | Some programmers even emulate a version of that by hand (CPS transform then trampolining) in Javascript and Python to support unlimited recursion depth. |
| 2024-04-16 21:53:52 +0200 | <int-e> | this may take a WHILE |
| 2024-04-16 21:55:29 +0200 | <monochrom> | The general meme is pretty interesting. You can always factor out all possibility of non-termination to the outermost level, and it needs only one level. |
| 2024-04-16 21:58:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 21:59:15 +0200 | <monochrom> | There is also a pretty cute normal form theorem for the terminating part. Every total computing function equals (some catamorphism) . (some anamorphism), i.e., there exists an intermediate data structure such that you use the input to drive unfolding to the intermediate, then you fold the intermediate. |
| 2024-04-16 21:59:29 +0200 | <monochrom> | err s/computing/computable/ |
| 2024-04-16 22:02:30 +0200 | <monochrom> | There is some version of that for imperative programming too. In Ralf Back and Joachim von Wright's book The Refinement Calculus (and probably some of their papers), using monotonic predicate transformers as the theory of imperative programming, every terminating program equals (something only angelically nondeterministic) ; (something only demonically nondeterministic) IIRC. |
| 2024-04-16 22:02:33 +0200 | <int-e> | There's also the logical version where you need exactly one unbounded existential quantifier to describe a r.e. set. |
| 2024-04-16 22:02:57 +0200 | <monochrom> | Yeah, that one. |
| 2024-04-16 22:05:05 +0200 | JeremyB99 | (~JeremyB99@208.64.173.20) (Ping timeout: 272 seconds) |
| 2024-04-16 22:05:35 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 2024-04-16 22:06:15 +0200 | <monochrom> | If you actually ask me how exactly "cata . ana" is analogous to "angel ; demon", I don't actually know, apart from how you can always factor an arbitrary thing to "one restriction . the opposite restriction". |
| 2024-04-16 22:07:13 +0200 | dispater- | (~dispater@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 22:07:14 +0200 | orcus | (~orcus@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 22:08:04 +0200 | <monochrom> | Oh yeah and of course every monad factorable to right.left :) |
| 2024-04-16 22:11:04 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 22:11:43 +0200 | orcus | (~orcus@217.155.58.82) |
| 2024-04-16 22:11:47 +0200 | orcus | (~orcus@217.155.58.82) (Client Quit) |
| 2024-04-16 22:14:53 +0200 | <masaeedu> | > Every total computing function equals (some catamorphism) . (some anamorphism) |
| 2024-04-16 22:14:55 +0200 | <lambdabot> | error: |
| 2024-04-16 22:14:55 +0200 | <lambdabot> | Data constructor not in scope: |
| 2024-04-16 22:14:55 +0200 | <lambdabot> | Every |
| 2024-04-16 22:14:59 +0200 | <masaeedu> | that's interesting. do you have a reference for that? |
| 2024-04-16 22:15:01 +0200 | <masaeedu> | whoops |
| 2024-04-16 22:15:52 +0200 | Square | (~Square@user/square) |
| 2024-04-16 22:16:59 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 2024-04-16 22:18:26 +0200 | rosco | (~rosco@2001:240:242f:d6eb:ca19:e23f:936a:839f) (Read error: Connection reset by peer) |
| 2024-04-16 22:18:34 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-04-16 22:18:41 +0200 | rosco | (~rosco@aq028228.dynamic.ppp.asahi-net.or.jp) |
| 2024-04-16 22:18:41 +0200 | <monochrom> | I forgot. Maybe one of those recursion scheme papers. |
| 2024-04-16 22:19:09 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 2024-04-16 22:22:09 +0200 | n8n | (n8n@user/n8n) |
| 2024-04-16 22:23:44 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 2024-04-16 22:26:45 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-04-16 22:27:14 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 2024-04-16 22:27:15 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 2024-04-16 22:27:37 +0200 | <probie> | :t \h -> let hylo f g = let go = f . fmap go . g in go in hylo (uncurry (.)) (\x -> (x,x)) h () |
| 2024-04-16 22:27:38 +0200 | <lambdabot> | (b -> b) -> b |
| 2024-04-16 22:28:46 +0200 | dispater- | (~dispater@217.155.58.82) |
| 2024-04-16 22:29:22 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Quit: Leaving) |
| 2024-04-16 22:30:46 +0200 | orcus | (~orcus@217.155.58.82) |
| 2024-04-16 22:31:08 +0200 | <probie> | > let fix = \h -> let hylo f g = let go = f . fmap go . g in go in hylo (uncurry (.)) (\x -> (x,x)) h () in fix (\r n -> if n <= 0 then 1 else n * (r (n - 1))) 5 |
| 2024-04-16 22:31:09 +0200 | <lambdabot> | 120 |
| 2024-04-16 22:32:03 +0200 | orcus | (~orcus@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 22:32:03 +0200 | dispater- | (~dispater@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 22:37:29 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 2024-04-16 22:37:54 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 2024-04-16 22:38:53 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 22:39:20 +0200 | phma | (phma@2001:5b0:215a:e298:fd17:443b:b4a0:861c) (Read error: Connection reset by peer) |
| 2024-04-16 22:40:13 +0200 | phma | (phma@2001:5b0:210d:72b8:fcdc:5db1:5990:c6e2) |
| 2024-04-16 22:40:19 +0200 | <Inst> | question: is it me, or did, in the past few months, Haskell give up? |
| 2024-04-16 22:40:37 +0200 | <Rembane> | Inst: It's you |
| 2024-04-16 22:40:47 +0200 | <probie> | What does it mean for a programming language to "give up"? |
| 2024-04-16 22:41:12 +0200 | <Inst> | i'll drop it, it's silly |
| 2024-04-16 22:41:23 +0200 | <Inst> | just seems as though there's nothing fun happening these days |
| 2024-04-16 22:41:47 +0200 | <int-e> | that's totally you |
| 2024-04-16 22:42:16 +0200 | <Inst> | https://downloads.haskell.org/ghc/latest/docs/users_guide/9.8.1-notes.html |
| 2024-04-16 22:42:28 +0200 | <monochrom> | That's a sign of a language actually used in anger. |
| 2024-04-16 22:43:03 +0200 | <monochrom> | You don't hear C, an actually used language, go "we have a new type system extension!" even every year. |
| 2024-04-16 22:44:03 +0200 | <probie> | C may have avoided that, but languages seem to bolt on new features at an alarming rate these days |
| 2024-04-16 22:44:12 +0200 | <Inst> | i'm just annoyed because ben gamari was talking about adding stack-protector support to clang to help keep weird msys libs working on windows for ghc 9.10.x |
| 2024-04-16 22:44:23 +0200 | <Inst> | i guess he forgot :( |
| 2024-04-16 22:44:24 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-04-16 22:44:34 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 22:44:52 +0200 | <Inst> | let's see, while i was busy |
| 2024-04-16 22:44:53 +0200 | <Inst> | https://downloads.haskell.org/ghc/latest/docs/users_guide/9.8.1-notes.html |
| 2024-04-16 22:46:15 +0200 | <int-e> | so "nothing fun is happening" means "nobody's implementing the one feature I currently care about in this moment"? |
| 2024-04-16 22:46:25 +0200 | <Inst> | i don't even care about it |
| 2024-04-16 22:46:29 +0200 | <Inst> | i'm not on windows anymore |
| 2024-04-16 22:46:39 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 2024-04-16 22:46:44 +0200 | <Inst> | 9.8 is sort of boring, no new extensions |
| 2024-04-16 22:47:00 +0200 | <Inst> | https://downloads.haskell.org/ghc/9.10.1-alpha2/docs/users_guide/9.10.1-notes.html |
| 2024-04-16 22:47:07 +0200 | <Inst> | GHC2024 is a big improvement |
| 2024-04-16 22:48:17 +0200 | <monochrom> | Actually C regresses: https://queue.acm.org/detail.cfm?id=3588242 then look for "incendiary realloc" |
| 2024-04-16 22:49:47 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:71fb:90e9:99e2:5642) |
| 2024-04-16 22:49:47 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:71fb:90e9:99e2:5642) (Changing host) |
| 2024-04-16 22:49:47 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-04-16 22:49:51 +0200 | <monochrom> | The sign of an actually used language: The standard committee is so bored, they start to take away prior guarantees that users need. >:) |
| 2024-04-16 22:50:55 +0200 | <Inst> | is that actually a bad thing? :) |
| 2024-04-16 22:50:59 +0200 | <probie> | > C23 declares realloc(ptr,0) to be undefined behavior |
| 2024-04-16 22:51:01 +0200 | <monochrom> | Oh wait GHC2024 has dropped? |
| 2024-04-16 22:51:32 +0200 | <Inst> | lambdacase finally made the cut |
| 2024-04-16 22:51:34 +0200 | <probie> | Inst: An idiom for `free` now no longer promises to free for no good reason? That seems rather dangerous |
| 2024-04-16 22:51:36 +0200 | <Inst> | well, technically no |
| 2024-04-16 22:51:56 +0200 | <Inst> | 9.10.1 hasn't hit rc1 status yet |
| 2024-04-16 22:52:07 +0200 | <monochrom> | It's why the article says this new standard sets the whole world on fire. |
| 2024-04-16 22:53:08 +0200 | <monochrom> | I feel like not enough people make this drama go viral on social media and cause an uproar. |
| 2024-04-16 22:53:52 +0200 | <monochrom> | Then again who has time for social media drama with a actual programming job. Like I said, sign of a language actually used. |
| 2024-04-16 22:54:04 +0200 | <dolio> | Most people don't pay any attention to what C actually does. They just go around telling everyone they should write everything in it. |
| 2024-04-16 22:54:16 +0200 | <monochrom> | heh |
| 2024-04-16 22:54:53 +0200 | <c_wraith> | "Developers who manage to figure out what the standard actually means are frequently appalled." truer words never spoken of C |
| 2024-04-16 22:54:57 +0200 | <mauke> | finally I can zero-initialize my variables with = {} |
| 2024-04-16 22:55:01 +0200 | <mauke> | = {0} was just too long |
| 2024-04-16 22:55:07 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 272 seconds) |
| 2024-04-16 22:55:09 +0200 | <Inst> | isn't there a substantial population of developers for which writing everything in C isn't a major loss? |
| 2024-04-16 22:55:42 +0200 | <cheater> | mauke thinking like a true C-nile |
| 2024-04-16 22:55:43 +0200 | <monochrom> | I think the latter is a truism: You like the language you picked (or maybe stockholmed in), therefore you tell everyone to switch to it. I have friends doing that with C++. |
| 2024-04-16 22:56:02 +0200 | <int-e> | monochrom: How have I not heard of this C23 insanity. |
| 2024-04-16 22:56:32 +0200 | <dolio> | I'm not even convinced that the people who say everything should be written in C actually write C. They just want everyone else to use it so that their programs are 'fast'. |
| 2024-04-16 22:56:35 +0200 | <monochrom> | Then again I do the same, just with Haskell instead, or sometimes Lean when in the right context. :) |
| 2024-04-16 22:56:42 +0200 | <int-e> | I guess it's fine since nobody is using C in 2024, right... *cries into a pillow* |
| 2024-04-16 22:56:46 +0200 | <probie> | monochrom: I avoid this problem by just hating all languages |
| 2024-04-16 22:57:09 +0200 | <Inst> | i'm guessing the fun stuff right now is GHCJS and Asterius (wasm) backends |
| 2024-04-16 22:57:37 +0200 | <cheater> | probie: me, but programmers |
| 2024-04-16 22:57:48 +0200 | <monochrom> | My students who go to hackathons write exclusively in Javascript, i.e., their projects are exclusively web apps. So yeah, actually nobody is using C in 2024, at least true of hackathons. |
| 2024-04-16 22:58:00 +0200 | <EvanR> | people who say everything should be written in C are ridiculous. Obviously everything should be written in rust |
| 2024-04-16 22:58:20 +0200 | <cheater> | he said the r-word |
| 2024-04-16 22:58:24 +0200 | <Inst> | i'm just saying meeting julia community it's obvious that different programmers have different use cases for programming languages |
| 2024-04-16 22:58:26 +0200 | <int-e> | EvanR: what are you using as flame repellent? |
| 2024-04-16 22:58:38 +0200 | <Inst> | i'm hypothesizing there exists a group of developers for which C covers all of their needs |
| 2024-04-16 22:58:44 +0200 | <EvanR> | tellurium |
| 2024-04-16 22:58:50 +0200 | <jle`> | arduino programmers |
| 2024-04-16 22:58:52 +0200 | <mauke> | "it's impossible to implement the standard memmove() function efficiently in standard C" - how is that an issue? |
| 2024-04-16 22:59:24 +0200 | <jle`> | actually i take that back, arduiono programmers need better than C |
| 2024-04-16 22:59:35 +0200 | <mauke> | (also, depends on your definition of "efficiently") |
| 2024-04-16 23:01:41 +0200 | <c_wraith> | jle`: I seem to recall a lot of discussion of python on arduino |
| 2024-04-16 23:01:53 +0200 | <monochrom> | Actually the other angle is that whatever C23 decrees is becoming irrelevant anyway. |
| 2024-04-16 23:02:10 +0200 | <probie> | int-e: I still use C from time to time in 2024. Rust is a moving target (so is C to a lesser extent, but some flags to the compiler asking for c99 fix that) with a huge dependency footprint |
| 2024-04-16 23:02:45 +0200 | dispater- | (~dispater@217.155.58.82) |
| 2024-04-16 23:02:47 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 2024-04-16 23:03:14 +0200 | orcus | (~orcus@217.155.58.82) |
| 2024-04-16 23:03:19 +0200 | <benjaminl> | I mostly write new stuff in rust, but there's a *huge* body of existing C code that needs to be maintained |
| 2024-04-16 23:03:53 +0200 | <Inst> | iirc Haskell can FFI effortlessly into C, but it can only FFI into Rust with difficulty |
| 2024-04-16 23:04:02 +0200 | <monochrom> | In the case of still using C for desktop apps, one just writes to GNU C on x86/arm or MS C or... and can safely ignore standard C UBs where the actual compiler and platform gives an extra guarantee. |
| 2024-04-16 23:04:03 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 255 seconds) |
| 2024-04-16 23:04:19 +0200 | <c_wraith> | "effortlessly" is an exaggeration if the C api is complicated at all... |
| 2024-04-16 23:04:33 +0200 | <int-e> | probie: I don't think that C is going away anytime soon; it's still the go to language for low level code that needs to be highly portable. |
| 2024-04-16 23:04:34 +0200 | <benjaminl> | yeah, C is basically the only cross-language ABI |
| 2024-04-16 23:04:35 +0200 | <monochrom> | And in the case of embedded systems, you are wedded to the extra guarantees of the compiler and platform anyway. |
| 2024-04-16 23:04:48 +0200 | <benjaminl> | if you want to FFI into not-C stuff, you have to lower the not-C to the C ABI first |
| 2024-04-16 23:05:04 +0200 | <dolio> | What does this have to do with writing every program in C? |
| 2024-04-16 23:05:05 +0200 | <int-e> | probie: I'm also certainly not one of the people who's advocating to use Rust for everything. |
| 2024-04-16 23:05:19 +0200 | <monochrom> | And finally in the case of school assignments (which is what I actually know professionally), you just use C as an Algol. |
| 2024-04-16 23:05:25 +0200 | <Inst> | well my point is that writing every program in C is correct |
| 2024-04-16 23:05:36 +0200 | <Inst> | if you are a programmer for which every program you need to write is best written in C |
| 2024-04-16 23:05:49 +0200 | orcus | (~orcus@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 23:05:49 +0200 | dispater- | (~dispater@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 23:05:50 +0200 | <dolio> | Your point is that you didn't read what I wrote? |
| 2024-04-16 23:05:53 +0200 | <int-e> | (Heck the number of times I've pondered doing some small thing in Rust and then used C++ because I wanted to be flexible with pointers...) |
| 2024-04-16 23:06:22 +0200 | <int-e> | I get what all the lifetimes are for, but they can be a burden. |
| 2024-04-16 23:06:37 +0200 | <benjaminl> | monochrom: IME most C implementations that exist don't define enough of the UB from the standard to really make a dent |
| 2024-04-16 23:06:43 +0200 | <Inst> | well we got on a tangent from "write it in c" |
| 2024-04-16 23:07:27 +0200 | <benjaminl> | like... pretty sure gcc still treats side-effect-free infinite loops as UB, for example |
| 2024-04-16 23:07:55 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 2024-04-16 23:08:03 +0200 | JeremyB99 | (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 2024-04-16 23:08:03 +0200 | <Inst> | EvanR: how's the macro community in Rust? |
| 2024-04-16 23:08:09 +0200 | dispater- | (~dispater@217.155.58.82) |
| 2024-04-16 23:08:18 +0200 | michalz | (~michalz@185.246.207.215) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-16 23:08:18 +0200 | <Inst> | afaik the problem with Rust is ergonomics, but it seems as though their macros can fix all their ergo needs |
| 2024-04-16 23:08:24 +0200 | dispater- | (~dispater@217.155.58.82) (Remote host closed the connection) |
| 2024-04-16 23:09:07 +0200 | <monochrom> | int-e: When that happens, I blame myself for still trying to treat Rust as C++ or even Haskell. For example, that time when I thought that writing my own linked list library was a good way to learn Rust... |
| 2024-04-16 23:09:53 +0200 | <monochrom> | Quickly I realized how much I have presumed either GC or malloc/free all my life subconsciously. |
| 2024-04-16 23:11:49 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-04-16 23:12:26 +0200 | zetef | (~quassel@5.2.182.98) |
| 2024-04-16 23:12:47 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-04-16 23:12:57 +0200 | <monochrom> | So I concluded that whenever I want data structures I should just use what's already in Rust's standard library (which has resolved all internal ownership questions, or at least unsafe-coerced them). My own variables should only be primitive types or references to ready-made data structures. Then my code has no issues. |
| 2024-04-16 23:16:24 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-16 23:18:52 +0200 | JeremyB99 | (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 2024-04-16 23:20:57 +0200 | JeremyB99 | (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 2024-04-16 23:21:11 +0200 | gorignak | (~gorignak@user/gorignak) |
| 2024-04-16 23:21:20 +0200 | gorignak | (~gorignak@user/gorignak) (Client Quit) |
| 2024-04-16 23:25:15 +0200 | flukiluke | (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Ping timeout: 268 seconds) |
| 2024-04-16 23:25:34 +0200 | flukiluke | (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
| 2024-04-16 23:25:42 +0200 | JeremyB99 | (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 2024-04-16 23:26:25 +0200 | <monochrom> | But if you do want to write your own data structures in Rust and therefore run into one of those pointer ownership issues, std::mem's replace and swap may help. Think of them as like CAS --- atomic operations but for ownership tracking. |
| 2024-04-16 23:26:52 +0200 | noumenon | (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 2024-04-16 23:28:17 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 2024-04-16 23:28:34 +0200 | Square2 | (~Square4@user/square) |
| 2024-04-16 23:31:58 +0200 | Square | (~Square@user/square) (Ping timeout: 255 seconds) |
| 2024-04-16 23:32:18 +0200 | <monochrom> | OK GHC2024. I don't like DataKinds, GADTs, MonoLocalBinds. :( |
| 2024-04-16 23:32:35 +0200 | <c_wraith> | wait. MonoLocalBinds should never be on by default :( |
| 2024-04-16 23:33:09 +0200 | <monochrom> | There is consolation in "GHC2021 remains the default langauge" even for 9.10. |
| 2024-04-16 23:33:23 +0200 | <int-e> | monochrom: do DataKinds or GADTs actively hurt you? |
| 2024-04-16 23:33:35 +0200 | <c_wraith> | GADTs turns on MonoLocalBinds |
| 2024-04-16 23:33:38 +0200 | <int-e> | (Also GADTs are nice, but obviously that's an opinion.) |
| 2024-04-16 23:33:56 +0200 | <int-e> | Ah. That's fair I guess. |
| 2024-04-16 23:33:59 +0200 | <monochrom> | IIRC IIUC GADTs is better with MonoLocalBinds, so that's why. Blame it on GADTs. >:( |
| 2024-04-16 23:34:31 +0200 | <monochrom> | int-e, I am just being right-wing conservative. :) |
| 2024-04-16 23:34:44 +0200 | <monochrom> | reactionary actually :D |
| 2024-04-16 23:35:12 +0200 | <monochrom> | But I'm happy with LambdaCase. But I'm unhappy with how MultiwayIf is still out. |
| 2024-04-16 23:35:36 +0200 | <monochrom> | Do people really hate anything remotely resembling if-then-else that much? |
| 2024-04-16 23:36:09 +0200 | <c_wraith> | I think there were some cases where there is no principal type for a definition involving a GADT, and MonoLocalBinds makes inference possible in some additional cases because you skip trying to find the principal type |
| 2024-04-16 23:36:41 +0200 | <monochrom> | I need it for like weight-balanced binary search trees where you have to say "if 3*x < y then ... else if x > 3*y then ... else no rotation needed". |
| 2024-04-16 23:37:22 +0200 | <monochrom> | And each of the two "..."s contain one more genuine if-then-else i.e. inequalities not reducible to pattern matching. |
| 2024-04-16 23:37:53 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2024-04-16 23:37:57 +0200 | <int-e> | I usually find a way to write that with guards |
| 2024-04-16 23:37:58 +0200 | <monochrom> | Hot take unpopular opinion: Pattern matching is overrated. There is such a thing as pattern matching blindness, too. |
| 2024-04-16 23:38:36 +0200 | <monochrom> | MultiwayIf is just guards without needing a declaration. Why not admit it into GHC2024. |
| 2024-04-16 23:39:31 +0200 | <dolio> | Isn't multiway if kind of gnarly? |
| 2024-04-16 23:39:40 +0200 | <monochrom> | I say no! |
| 2024-04-16 23:39:55 +0200 | <dolio> | Like, if you end up nesting them it's difficult to parse or something. |
| 2024-04-16 23:40:31 +0200 | <dolio> | Like, the feature is fine, but the syntax is bad, or something. |
| 2024-04-16 23:40:39 +0200 | <monochrom> | Hrm. I wouldn't mind being forced to add parentheses to help both computer and humans. |
| 2024-04-16 23:40:52 +0200 | <int-e> | dolio: hmm doesn't look too terrible at a glance: https://downloads.haskell.org/ghc/9.10.1-alpha3/docs/users_guide/exts/multiway_if.html |
| 2024-04-16 23:41:17 +0200 | <monochrom> | But I understand that this is another unpopular opinion. People irrationally hate parentheses too. |
| 2024-04-16 23:41:37 +0200 | it_ | (~quassel@v2202212189510211193.supersrv.de) (Quit: No Ping reply in 180 seconds.) |
| 2024-04-16 23:41:54 +0200 | <Inst> | if you're inline nesting with multiway if / guards you're doing it wrong |
| 2024-04-16 23:42:07 +0200 | <Inst> | this is haskell, just stuff some stuff in let expression / where clause and call it a day |
| 2024-04-16 23:42:12 +0200 | <monochrom> | Oh they have a layout rule for that. So yeah problem solved? (OK I admit lack of imagination.) |
| 2024-04-16 23:42:48 +0200 | <monochrom> | But I haven't actually needed nesting in my use case. |
| 2024-04-16 23:43:32 +0200 | <monochrom> | Like I said I wouldn't even mind banning nesting, requiring me to add parentheses. |
| 2024-04-16 23:44:03 +0200 | <int-e> | I guess I just don't find `case () of` too onerous so I never went looking for MultiWayIf |
| 2024-04-16 23:44:21 +0200 | <monochrom> | :( |
| 2024-04-16 23:44:48 +0200 | <int-e> | I do agree that it looks harmless enough so it could've been included in GHC2024 |
| 2024-04-16 23:45:10 +0200 | <monochrom> | BTW it is `case () of _` to be complete. >:) |
| 2024-04-16 23:45:11 +0200 | <int-e> | So maybe nobody asked |
| 2024-04-16 23:45:18 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-04-16 23:45:20 +0200 | <int-e> | monochrom: yes I know |
| 2024-04-16 23:45:39 +0200 | <int-e> | monochrom: the _ needs to be repeated for every case too |
| 2024-04-16 23:45:42 +0200 | <int-e> | err |
| 2024-04-16 23:45:44 +0200 | <yushyin> | the examples from the \cases proposal suggests that you can often use it instead of MultiWayIf |
| 2024-04-16 23:45:54 +0200 | <int-e> | no... |
| 2024-04-16 23:46:00 +0200 | int-e | is just stupid |
| 2024-04-16 23:46:09 +0200 | <int-e> | (you /can/ repeat it of course) |
| 2024-04-16 23:46:12 +0200 | <monochrom> | I will wait for GHC2050ArcticIcesheetAllMeltedEdition" |
| 2024-04-16 23:46:55 +0200 | <monochrom> | yushyin, my said use case does not want a lambda either. |
| 2024-04-16 23:46:56 +0200 | it_ | (~quassel@v2202212189510211193.supersrv.de) |
| 2024-04-16 23:47:30 +0200 | <monochrom> | I already know how to encode everything in terms of everything else stop telling me I could have written it in Core heh |
| 2024-04-16 23:48:17 +0200 | <int-e> | Haskell isn't reductive. It's part of its charm. |
| 2024-04-16 23:48:48 +0200 | <Inst> | btw, pattern guards doesn't support ;, right? |
| 2024-04-16 23:49:59 +0200 | <monochrom> | I think all of us agree that there is a balance between breadth and minimalism, either extreme is bad. So I'm just whining how the consensus balance is slightly away from my preference, don't mind me if necessary heh |
| 2024-04-16 23:50:28 +0200 | <int-e> | monochrom: at least your comments have a point |
| 2024-04-16 23:50:38 +0200 | <monochrom> | Right, pattern guards don't have a notion of ; or layout at all. |
| 2024-04-16 23:50:49 +0200 | <Inst> | no, because , is a substitute for && |
| 2024-04-16 23:50:57 +0200 | <Inst> | ; could be a substitute for or |
| 2024-04-16 23:51:01 +0200 | <Inst> | || |
| 2024-04-16 23:51:10 +0200 | <monochrom> | Ugh how could anyone guess that. |
| 2024-04-16 23:51:18 +0200 | <Inst> | only if they prolog too much |
| 2024-04-16 23:51:32 +0200 | <monochrom> | You need to hear my favourite true story. |
| 2024-04-16 23:51:57 +0200 | <Inst> | Seems like I do. |
| 2024-04-16 23:52:07 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-16 23:52:12 +0200 | <monochrom> | Two decades ago my friend was an on-site tech support person. One day he visited a small company office to install new software. |
| 2024-04-16 23:52:14 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-04-16 23:52:37 +0200 | <monochrom> | The people in the small office kept asking him "Will it support 1048"? |
| 2024-04-16 23:52:46 +0200 | <monochrom> | Can you guess what "1048" meant? |
| 2024-04-16 23:53:24 +0200 | <c_wraith> | some local version of y2k? |
| 2024-04-16 23:53:29 +0200 | <monochrom> | How is any outsider supposed to guess a homebrew insider abbreviation from an echo chamber? |
| 2024-04-16 23:53:42 +0200 | <monochrom> | Answer: 1024x768 resolution. |
| 2024-04-16 23:54:03 +0200 | <c_wraith> | I thought about that, but rejected it because 24 /= 48 |
| 2024-04-16 23:55:07 +0200 | <Inst> | uhhh, where did the 48 come from? |
| 2024-04-16 23:55:45 +0200 | <int-e> | . o O ( XGA ) |
| 2024-04-16 23:55:47 +0200 | <monochrom> | It also "helped" that they were Chinese. We don't prononce the full version as "ten twenty-four by seven sixty-eight". We literally say "one zero two four seven six eight". Then it's easier to see how one would randomly just pick out 4 digits out of it for short. |
| 2024-04-16 23:56:50 +0200 | orcus- | (~orcus@mail.brprice.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-16 23:56:50 +0200 | dispater | (~dispater@mail.brprice.uk) (Quit: ZNC 1.8.2 - https://znc.in) |