| 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> | <orbicularis> reminder this exists https://godbolt.org/noscript/haskell |
| 2024-04-16 12:39:49 +0200 | <haskellbridge> | <orbicularis> i wish it had more IR and so on |
| 2024-04-16 12:40:03 +0200 | <haskellbridge> | <orbicularis> like it would be super cool to have a version of this on steroids |
| 2024-04-16 12:40:36 +0200 | <haskellbridge> | <orbicularis> 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) |