Logs on 2024-04-16 (liberachat/#haskell)
| 00:02:57 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 00:05:15 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 00:05:40 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 00:10:39 | → | ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com) |
| 00:12:01 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 246 seconds) |
| 00:17:18 | × | CrunchyFlakes quits (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 00:17:56 | → | CrunchyFlakes joins (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
| 00:20:28 | → | madeleine-sydney joins (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 00:20:58 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 00:33:27 | <Inst> | what's the replacement for overlapping instances again? |
| 00:34:29 | <dolio> | The various pragmas with similar names. |
| 00:34:32 | <geekosaur> | overlapping instances are still there, you just do them differently (fine control instead of indiscriminately in a whole source file) |
| 00:36:25 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 256 seconds) |
| 00:39:07 | × | JeremyB99 quits (~JeremyB99@208.64.173.20) (Ping timeout: 272 seconds) |
| 00:42:55 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 272 seconds) |
| 00:43:37 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 00:43:40 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 00:46:04 | → | mei joins (~mei@user/mei) |
| 00:46:50 | → | causal joins (~eric@50.35.88.207) |
| 00:48:12 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 01:00:17 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 01:07:51 | <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? |
| 01:11:24 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 01:12:16 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 01:12:28 | <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 |
| 01:13:03 | × | euleritian quits (~euleritia@dynamic-176-004-212-165.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 01:13:20 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 01:15:15 | <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 |
| 01:16:47 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 01:17:35 | → | halloy3555 joins (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 01:18:59 | × | halloy3555 quits (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Remote host closed the connection) |
| 01:19:14 | → | halloy3555 joins (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 01:19:24 | <sm> | megaparsec++ |
| 01:19:39 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 255 seconds) |
| 01:20:47 | × | halloy3555 quits (~halloy355@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Remote host closed the connection) |
| 01:21:02 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 01:24:50 | → | JeremyB99 joins (~JeremyB99@208.64.173.20) |
| 01:27:35 | <probie> | Using something like diagnose or errata seems like a good idea. I think I'll be boring and go with megaparsec + diagnose |
| 01:28:08 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 01:31:47 | → | Core4595 joins (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) |
| 01:31:47 | × | rosco quits (~rosco@aq052236.dynamic.ppp.asahi-net.or.jp) (Read error: Connection reset by peer) |
| 01:32:11 | × | Core4595 quits (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) (Read error: Connection reset by peer) |
| 01:32:25 | → | rosco joins (~rosco@aq052236.dynamic.ppp.asahi-net.or.jp) |
| 01:32:59 | × | JeremyB99 quits (~JeremyB99@208.64.173.20) (Ping timeout: 264 seconds) |
| 01:33:44 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 01:34:22 | <Inst> | I don't understand why people complain about lazy functional programming |
| 01:34:30 | <Inst> | trying to inject FP into Julia, ugh |
| 01:34:50 | <Inst> | at least Python turns FP idioms into iterators |
| 01:34:57 | <geekosaur> | <cynic> it forces them to think </cynic> |
| 01:36:07 | → | mei joins (~mei@user/mei) |
| 01:36:11 | × | YuutaW quits (~YuutaW@mail.yuuta.moe) (Ping timeout: 260 seconds) |
| 01:37:14 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 01:38:39 | <Inst> | like, typed FP is an optimum for FP |
| 01:39:24 | <Inst> | has drawbacks, but usually being familiar with workarounds solves the problem |
| 01:40:14 | <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 |
| 01:43:59 | <monochrom> | <extreme cynicism> Because programmers are control freaks. </extreme cynicism> |
| 01:45:04 | <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> |
| 01:45:33 | <monochrom> | At that point I'm wondering if I should just s/cynicism/fundamental hatred of humanity/ |
| 01:46:07 | <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) |
| 01:46:14 | <Inst> | don't, it made me very very unpopular |
| 01:47:15 | × | otto_s quits (~user@p4ff27773.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 01:47:37 | <geekosaur> | I only resorted to inline asm in 2 cases, and in both of them I considered it a compiler bug |
| 01:47:44 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 01:47:46 | → | Core7966 joins (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) |
| 01:47:54 | × | rosco quits (~rosco@aq052236.dynamic.ppp.asahi-net.or.jp) (Read error: Connection reset by peer) |
| 01:47:55 | <geekosaur> | it's the compiler's job to worry about the asm for me! |
| 01:48:24 | × | Core7966 quits (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) (Read error: Connection reset by peer) |
| 01:48:38 | → | otto_s joins (~user@p4ff2776b.dip0.t-ipconnect.de) |
| 01:49:00 | → | rosco joins (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) |
| 01:50:43 | × | xff0x quits (~xff0x@2405:6580:b080:900:1540:8996:2d0b:5b54) (Ping timeout: 255 seconds) |
| 01:53:56 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 01:55:26 | <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 |
| 01:57:03 | <jackdk> | probie: if you move off trifecta, write up an example first for the rest of us? |
| 01:58:27 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 01:58:34 | <geekosaur> | (also, C was my introduction to types. if this doesn't make sense to you, you didn't start out doing asm) |
| 02:02:33 | → | cipherrot joins (~znc-user@user/petrichor) |
| 02:03:02 | × | petrichor quits (~znc-user@user/petrichor) (Ping timeout: 256 seconds) |
| 02:03:09 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 02:03:13 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 02:04:08 | <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. |
| 02:04:30 | <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 |
| 02:07:05 | <geekosaur> | strictly speaking I started out on BASIC too, but it was such a limited toy that I abandoned it for asm quickly |
| 02:08:56 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:14:14 | <monochrom> | Oh BASIC had types. It was just combining the type safety of C with the hungarian-wannabe sigil system of Perl. |
| 02:14:42 | <monochrom> | N is of the number type, N$ is of the string type. |
| 02:14:59 | <jackdk> | despite predating both |
| 02:15:40 | <jackdk> | VB (and maybe others) extended that to avoid having to write `dim i as integer`: you had `%` for ints, `&` for longs, etc. (IIRC) |
| 02:18:16 | <c_wraith> | that definitely predates VB. It was in the old TRS-80 basic I first learned to program in. |
| 02:18:40 | <geekosaur> | I recall it having % but not & |
| 02:18:46 | <c_wraith> | well. not longs, that hardware didn't have them. But it had integers and floats. |
| 02:18:54 | <geekosaur> | yeh |
| 02:19:00 | <c_wraith> | though it didn't have floating-point hardware, so they were *slow* |
| 02:19:53 | <geekosaur> | nobody had invented floating point coprocessors yet. and when Intel got around to it, it was a sideboard stack machine |
| 02:20:26 | <geekosaur> | I was especially happy to let the compiler deal with that mess |
| 02:21:04 | <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" |
| 02:21:51 | <monochrom> | Nah I think kids these days would love to have that card mandated so they don't have to learn recursion. |
| 02:22:13 | × | sgarcia_ quits (sgarcia@swarm.znchost.com) (Quit: Hosted by www.ZNCHost.com) |
| 02:22:18 | <geekosaur> | that one is understandable though, the TMS9900 thought it was a baby IBM mainframe. BALR anyone? |
| 02:23:06 | <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.) |
| 02:23:09 | <geekosaur> | (stuffed the return address into a register, and $DEITY help you if you overwrote it) |
| 02:23:42 | <monochrom> | Well, perhaps s/dumb/simpleton/ |
| 02:23:57 | <c_wraith> | yeah, GOSUB didn't have any idea of parameters. Just global variables. So, recursion wasn't very useful... |
| 02:24:59 | <geekosaur> | mm, right, I at one point had a BASIC preprocessor that did silly things like use an array ZZ as a parameter stack |
| 02:25:08 | → | sgarcia joins (sgarcia@swarm.znchost.com) |
| 02:25:26 | <geekosaur> | as well as adding control structures |
| 02:25:44 | × | Katarushisu1 quits (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 02:26:00 | <geekosaur> | I ditched it when I got Turbo Pascal |
| 02:26:07 | → | Katarushisu1 joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 02:31:19 | → | JeremyB99 joins (~JeremyB99@208.64.173.20) |
| 02:33:35 | → | as_ joins (~as@2800:a4:307:6f00:2530:9589:e186:2373) |
| 02:34:34 | → | yuuta joins (~YuutaW@mail.yuuta.moe) |
| 02:34:42 | × | YuutaW quits (~YuutaW@mail.yuuta.moe) (Quit: ZNC 1.8.2 - https://znc.in) |
| 02:36:17 | × | JeremyB99 quits (~JeremyB99@208.64.173.20) (Ping timeout: 272 seconds) |
| 02:37:31 | × | as_ quits (~as@2800:a4:307:6f00:2530:9589:e186:2373) (Quit: Leaving) |
| 02:37:38 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:38:59 | × | mei quits (~mei@user/mei) (Ping timeout: 264 seconds) |
| 02:39:03 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 02:39:29 | → | mei joins (~mei@user/mei) |
| 02:43:39 | × | yuuta quits (~YuutaW@mail.yuuta.moe) (Quit: ZNC 1.8.2 - https://znc.in) |
| 02:44:58 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 02:45:10 | × | td_ quits (~td@i53870931.versanet.de) (Ping timeout: 255 seconds) |
| 02:46:52 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 02:46:52 | → | td_ joins (~td@i53870911.versanet.de) |
| 02:59:02 | → | ddellacosta joins (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 03:00:08 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 03:00:21 | × | ryanbooker quits (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 03:02:33 | → | mei joins (~mei@user/mei) |
| 03:09:44 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 03:11:45 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds) |
| 03:13:00 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 260 seconds) |
| 03:16:39 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 256 seconds) |
| 03:19:11 | → | JeremyB99 joins (~JeremyB99@2607:fb91:bc1:a006:8998:5e0a:9eb8:f34d) |
| 03:37:15 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 03:39:27 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:43:46 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 03:53:22 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 03:59:44 | → | aforemny joins (~aforemny@i59F516ED.versanet.de) |
| 04:00:54 | × | aforemny_ quits (~aforemny@2001:9e8:6cdd:b100:9200:9bf0:8eb2:3efb) (Ping timeout: 256 seconds) |
| 04:03:25 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 04:05:31 | × | YuutaW quits (~YuutaW@mail.yuuta.moe) (Ping timeout: 256 seconds) |
| 04:06:40 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 04:13:19 | → | michalz joins (~michalz@185.246.207.215) |
| 04:29:37 | × | madeleine-sydney quits (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 04:39:46 | × | kmein quits (~weechat@user/kmein) (Ping timeout: 246 seconds) |
| 04:42:01 | <jackdk> | monochrom: TI Extended BASIC extended its `CALL` instruction to support calling into user-defined subprograms with arguments, including parameter passing |
| 04:45:39 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 252 seconds) |
| 04:53:40 | → | yeitrafferin joins (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) |
| 05:00:19 | → | kmein joins (~weechat@user/kmein) |
| 05:00:52 | <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 |
| 05:01:31 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:01:38 | <mauke> | but parameter/return value passing can be emulated with globals |
| 05:02:23 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 264 seconds) |
| 05:03:13 | × | philopsos quits (~caecilius@user/philopsos) (Ping timeout: 246 seconds) |
| 05:07:08 | → | danza joins (~francesco@ba-19-155-176.service.infuturo.it) |
| 05:14:57 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 05:17:42 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 05:19:28 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 260 seconds) |
| 05:21:31 | → | euleritian joins (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) |
| 05:22:51 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 272 seconds) |
| 05:25:16 | → | philopsos joins (~caecilius@user/philopsos) |
| 05:30:03 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:36:20 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 05:38:46 | → | xdminsy joins (~xdminsy@117.147.70.203) |
| 05:40:55 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 05:46:56 | → | zetef joins (~quassel@5.2.182.99) |
| 05:51:57 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 05:53:37 | <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. |
| 06:00:14 | → | mima joins (~mmh@aftr-62-216-211-171.dynamic.mnet-online.de) |
| 06:00:47 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:21:01 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 06:29:25 | → | julie_pilgrim joins (~julie_pil@user/julie-pilgrim/x-1240752) |
| 06:32:16 | × | danza quits (~francesco@ba-19-155-176.service.infuturo.it) (Ping timeout: 260 seconds) |
| 06:34:12 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 06:34:59 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 06:37:03 | × | yeitrafferin quits (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) (Quit: Leaving) |
| 06:37:26 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:40:28 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:42:42 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 06:43:16 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 06:51:18 | × | julie_pilgrim quits (~julie_pil@user/julie-pilgrim/x-1240752) (Ping timeout: 250 seconds) |
| 06:53:12 | × | kraftwerk28 quits (~kraftwerk@164.92.219.160) (Quit: *disconnects*) |
| 06:54:50 | × | ACuriousMoose quits (~ACuriousM@142.166.18.53) (Ping timeout: 256 seconds) |
| 06:55:21 | × | zetef quits (~quassel@5.2.182.99) (Ping timeout: 255 seconds) |
| 06:55:30 | → | ACuriousMoose joins (~ACuriousM@142.68.181.38) |
| 06:56:58 | → | acidjnk joins (~acidjnk@p200300d6e714dc20691c30fd92f896ed.dip0.t-ipconnect.de) |
| 07:05:15 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 07:05:44 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 07:07:59 | × | jle` quits (~jle`@2603-8001-3b02-84d4-a77f-f741-f7ec-5267.res6.spectrum.com) (Ping timeout: 256 seconds) |
| 07:08:48 | → | jle` joins (~jle`@2603:8001:3b02:84d4:9428:fb32:50c:b0cc) |
| 07:13:25 | × | jamesmartinez quits (uid6451@id-6451.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
| 07:15:49 | → | zetef joins (~quassel@5.2.182.99) |
| 07:20:06 | × | euleritian quits (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:20:23 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:22:01 | × | rosco quits (~rosco@2001:240:242c:d62d:115:791f:75e3:1c81) (Ping timeout: 256 seconds) |
| 07:22:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:29:47 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 07:29:47 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 07:35:26 | → | vglfr joins (~vglfr@185.124.31.142) |
| 07:40:43 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 07:43:06 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 07:44:12 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 07:47:42 | → | gmg joins (~user@user/gehmehgeh) |
| 07:51:15 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 07:53:14 | → | euleritian joins (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) |
| 07:57:10 | × | euleritian quits (~euleritia@dynamic-176-004-200-118.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:57:12 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Ping timeout: 260 seconds) |
| 07:57:27 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:58:03 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 07:58:04 | × | vglfr quits (~vglfr@185.124.31.142) (Read error: Connection reset by peer) |
| 07:58:23 | → | vglfr joins (~vglfr@158.red-81-45-80.staticip.rima-tde.net) |
| 07:59:57 | × | cheater quits (~Username@user/cheater) (Read error: Connection reset by peer) |
| 08:00:23 | → | danse-nr3 joins (~danse-nr3@151.37.230.221) |
| 08:00:46 | → | cheater joins (~Username@user/cheater) |
| 08:02:04 | × | danse-nr3 quits (~danse-nr3@151.37.230.221) (Remote host closed the connection) |
| 08:02:29 | → | danse-nr3 joins (~danse-nr3@151.37.230.221) |
| 08:17:27 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 08:18:49 | × | zetef quits (~quassel@5.2.182.99) (Ping timeout: 256 seconds) |
| 08:23:59 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 08:26:28 | × | tzh quits (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 08:27:45 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 08:33:58 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 08:34:22 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:44:53 | → | zetef joins (~quassel@5.2.182.99) |
| 08:45:14 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 08:47:59 | × | mima quits (~mmh@aftr-62-216-211-171.dynamic.mnet-online.de) (Ping timeout: 264 seconds) |
| 08:49:24 | → | chele joins (~chele@user/chele) |
| 08:50:46 | × | ft quits (~ft@p4fc2a20e.dip0.t-ipconnect.de) (Quit: leaving) |
| 08:59:51 | × | JimL quits (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 09:05:18 | → | random-jellyfish joins (~developer@2a02:2f04:11e:c600:5592:43e9:751e:c0fc) |
| 09:05:18 | × | random-jellyfish quits (~developer@2a02:2f04:11e:c600:5592:43e9:751e:c0fc) (Changing host) |
| 09:05:18 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 09:12:59 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 09:13:08 | × | demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 256 seconds) |
| 09:20:33 | → | JimL joins (~quassel@89.162.16.26) |
| 09:22:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:25:35 | × | JimL quits (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 09:25:52 | → | JimL joins (~quassel@89.162.16.26) |
| 09:28:06 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:30:32 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:31:21 | × | cfricke quits (~cfricke@user/cfricke) (Client Quit) |
| 09:32:20 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:1996:3c8e:f64b:a77b) |
| 09:34:20 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:38:11 | anon1123 | is now known as anon8697 |
| 09:38:43 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 255 seconds) |
| 09:45:03 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Ping timeout: 272 seconds) |
| 09:57:47 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 09:59:13 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 09:59:35 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 10:00:40 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 10:00:49 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 10:01:18 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 10:02:10 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 260 seconds) |
| 10:03:21 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 10:03:27 | × | JeremyB99 quits (~JeremyB99@2607:fb91:bc1:a006:8998:5e0a:9eb8:f34d) (Ping timeout: 260 seconds) |
| 10:03:54 | × | tv quits (~tv@user/tv) (Ping timeout: 255 seconds) |
| 10:04:06 | × | zetef quits (~quassel@5.2.182.99) (Ping timeout: 252 seconds) |
| 10:06:52 | → | JeremyB99 joins (~JeremyB99@208.64.173.20) |
| 10:10:53 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 240 seconds) |
| 10:17:05 | → | tv joins (~tv@user/tv) |
| 10:19:21 | → | zetef joins (~quassel@5.2.182.99) |
| 10:26:34 | × | danse-nr3 quits (~danse-nr3@151.37.230.221) (Remote host closed the connection) |
| 10:29:12 | <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? |
| 10:34:46 | → | danse-nr3 joins (~danse-nr3@151.37.230.221) |
| 10:35:03 | × | Inst quits (~Inst@user/Inst) (Read error: Connection reset by peer) |
| 10:37:19 | <masaeedu> | there's also `RawFilePath = ByteString` from `unix`... |
| 10:38:36 | <jackdk> | Not sure, but I am also aware of `path-io`, but I haven't considered its relative merits vs. `OsPath` |
| 10:39:15 | <haskellbridge> | <orbicularis> reminder this exists https://godbolt.org/noscript/haskell |
| 10:39:49 | <haskellbridge> | <orbicularis> i wish it had more IR and so on |
| 10:40:03 | <haskellbridge> | <orbicularis> like it would be super cool to have a version of this on steroids |
| 10:40:36 | <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 |
| 10:40:53 | × | danse-nr3 quits (~danse-nr3@151.37.230.221) (Ping timeout: 240 seconds) |
| 10:41:00 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 10:41:51 | → | danse-nr3 joins (~danse-nr3@151.37.230.221) |
| 10:42:35 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 10:45:21 | × | zetef quits (~quassel@5.2.182.99) (Remote host closed the connection) |
| 10:46:09 | → | zetef joins (~quassel@5.2.182.99) |
| 10:53:31 | × | destituion quits (~destituio@2a02:2121:107:22da:94a0:4297:56fa:10c9) (Ping timeout: 256 seconds) |
| 10:55:49 | × | YuutaW quits (~YuutaW@mail.yuuta.moe) (Read error: Connection reset by peer) |
| 10:55:56 | × | JeremyB99 quits (~JeremyB99@208.64.173.20) (Ping timeout: 268 seconds) |
| 10:56:11 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 11:04:41 | → | xff0x joins (~xff0x@2405:6580:b080:900:64dd:977c:c397:439c) |
| 11:06:12 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 11:06:27 | × | danse-nr3 quits (~danse-nr3@151.37.230.221) (Remote host closed the connection) |
| 11:06:51 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 11:07:26 | → | yeitrafferin joins (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) |
| 11:08:04 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 11:08:35 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 11:14:59 | × | zetef quits (~quassel@5.2.182.99) (Ping timeout: 272 seconds) |
| 11:15:02 | → | Inst joins (~Inst@user/Inst) |
| 11:16:32 | × | yeitrafferin quits (~user@2a04:4540:720f:7100:52ac:7ca7:64de:11a) (Remote host closed the connection) |
| 11:17:27 | → | JeremyB99 joins (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 11:17:49 | × | JeremyB99 quits (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 11:18:49 | → | alexherbo2 joins (~alexherbo@2a02-8440-3240-dc75-0888-f0c5-8353-6a7e.rev.sfr.net) |
| 11:19:56 | → | yeitrafferin joins (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) |
| 11:20:18 | × | masaeedu quits (~masaeedu@user/masaeedu) (Ping timeout: 268 seconds) |
| 11:24:47 | → | constxd joins (~constxd@user/constxd) |
| 11:24:53 | <constxd> | lads |
| 11:24:59 | <constxd> | https://www.cambridge.org/core/journals/journal-of-functional-programming/article/knuthmorrispratt-illustrated/8EFA77D663D585B68630E372BCE1EBA4 |
| 11:25:30 | <constxd> | if you scroll down a bit to the `verticalSet` function definition |
| 11:26:30 | → | JeremyB99 joins (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 11:26:32 | <constxd> | am i missing something or should it say ([x] `isPrefixOf`) instead of (isPrefixOf [x]) |
| 11:29:03 | <constxd> | (isPrefixOf [x]) seems like it will only ever match [] or [x] |
| 11:30:05 | <[Leary]> | constxd: They're the same thing, the first is just clearer in its meaning. |
| 11:30:47 | <constxd> | oh right lol |
| 11:31:12 | <constxd> | (isPrefixOf [x]) does not mean what you'd think it means if you read it out loud |
| 11:31:35 | <constxd> | thanks i thought i was going crazy |
| 11:34:46 | × | JeremyB99 quits (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 11:39:50 | → | JeremyB99 joins (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 11:40:59 | → | zetef joins (~quassel@5.2.182.99) |
| 11:41:33 | × | JeremyB99 quits (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 11:46:35 | × | puke quits (~puke@user/puke) (Ping timeout: 260 seconds) |
| 11:47:08 | → | puke joins (~puke@user/puke) |
| 11:48:46 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 11:50:01 | → | JeremyB99 joins (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 11:50:33 | × | JeremyB99 quits (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Read error: Connection reset by peer) |
| 11:58:45 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 11:58:46 | → | JeremyB99 joins (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) |
| 12:00:58 | × | zetef quits (~quassel@5.2.182.99) (Remote host closed the connection) |
| 12:01:35 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 12:02:05 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 12:04:23 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Client Quit) |
| 12:06:14 | × | ddellacosta quits (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 12:11:43 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 256 seconds) |
| 12:12:40 | → | danse-nr3 joins (~danse-nr3@151.35.170.130) |
| 12:13:22 | × | alexherbo2 quits (~alexherbo@2a02-8440-3240-dc75-0888-f0c5-8353-6a7e.rev.sfr.net) (Remote host closed the connection) |
| 12:13:34 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:17:16 | × | danse-nr3 quits (~danse-nr3@151.35.170.130) (Remote host closed the connection) |
| 12:21:09 | × | JeremyB99 quits (~JeremyB99@2607:fb90:f2e0:46a4:ec80:d6c8:47e7:f1af) (Ping timeout: 255 seconds) |
| 12:23:51 | → | danse-nr3 joins (~danse-nr3@151.35.170.130) |
| 12:26:38 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 12:26:48 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 12:31:53 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 12:37:24 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 12:37:25 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 12:42:32 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Remote host closed the connection) |
| 12:42:49 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 12:52:31 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 13:03:04 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 13:03:54 | × | n8n quits (n8n@user/n8n) (Quit: WeeChat 4.2.2) |
| 13:05:30 | → | mei joins (~mei@user/mei) |
| 13:05:44 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 13:09:33 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 13:12:53 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 13:13:12 | → | euleritian joins (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) |
| 13:13:13 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 13:14:29 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 13:14:47 | → | Guest3 joins (~Guest3@2400:1a00:bd11:3bf8:2e0:4cff:fefc:a34d) |
| 13:14:47 | × | Guest3 quits (~Guest3@2400:1a00:bd11:3bf8:2e0:4cff:fefc:a34d) (Client Quit) |
| 13:18:44 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 13:19:23 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 13:23:15 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 13:23:21 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 13:25:51 | → | mima joins (~mmh@aftr-62-216-211-171.dynamic.mnet-online.de) |
| 13:27:43 | × | euleritian quits (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 13:28:00 | → | euleritian joins (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) |
| 13:29:12 | × | euleritian quits (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 13:29:29 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 13:31:29 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 13:37:24 | <danse-nr3> | <3 ghcup |
| 13:37:25 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 13:44:27 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 13:45:39 | → | euleritian joins (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) |
| 13:47:47 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 13:53:04 | × | causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1) |
| 13:53:33 | × | qqq quits (~qqq@92.43.167.61) (Quit: Lost terminal) |
| 13:57:39 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 13:58:15 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 13:59:43 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 14:03:46 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 14:09:29 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 14:10:22 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 14:10:49 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 14:10:56 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 14:14:19 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 14:14:49 | × | danse-nr3 quits (~danse-nr3@151.35.170.130) (Ping timeout: 246 seconds) |
| 14:15:11 | → | noumenon joins (~noumenon@113.51-175-156.customer.lyse.net) |
| 14:15:47 | → | rosco joins (~rosco@2001:240:242f:d6eb:22d4:a19b:ae5c:b29d) |
| 14:18:03 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 14:20:16 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 14:20:56 | → | qqq joins (~qqq@92.43.167.61) |
| 14:27:48 | → | danse-nr3 joins (~danse-nr3@151.35.170.130) |
| 14:28:04 | <Inst> | with Cont monad |
| 14:28:38 | <Inst> | *> / >> is just, have the next line take its previous line as a continuation? |
| 14:29:21 | <Inst> | a >> b, b is the continuation of a? |
| 14:29:28 | <Inst> | but that's also interesting, there's also a backwards cont monad :3 |
| 14:29:40 | → | masaeedu joins (~masaeedu@user/masaeedu) |
| 14:30:17 | <Inst> | and discarding the result of the previous cont monad? |
| 14:30:24 | <Inst> | *cont monadic value, sigh |
| 14:31:35 | <Inst> | besides AccumT, SelectT, and ContT, are there any important monads to know about? |
| 14:32:00 | <Inst> | Monad zoo is, afaik, Maybe / Either, IO, State, Reader, Writer, List / List-like |
| 14:33:01 | <Inst> | Identity, ST is just IO rigged up to give access to STRef and no other IO |
| 14:33:02 | <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? |
| 14:33:37 | <raehik> | (use case, these functions return TypeError on failures, but that results in non-pretty errors at usage sites) |
| 14:45:46 | × | Arsen quits (~arsen@gentoo/developer/managarm.dev.Arsen) (Quit: Quit.) |
| 14:47:57 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 14:50:21 | → | JeremyB99 joins (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) |
| 14:51:27 | <EvanR> | you mean, you want type level do-notation? |
| 14:54:27 | → | Arsen joins (~arsen@gentoo/developer/managarm.dev.Arsen) |
| 15:01:42 | × | euleritian quits (~euleritia@dynamic-176-004-212-186.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:01:59 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:02:27 | × | guygastineau quits (~guygastin@137.184.131.156) (Quit: ZNC - https://znc.in) |
| 15:02:53 | <dmj`> | Inst: (->) and (,) |
| 15:04:18 | <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 |
| 15:04:45 | <Inst> | in the same way, say, uncurry (*>) (a,b) is smelly |
| 15:05:16 | <Inst> | erm, uncurry ($>) (a, functor b) |
| 15:05:20 | → | RMSBach joins (~guygastin@137.184.131.156) |
| 15:05:27 | × | JeremyB99 quits (~JeremyB99@2607:fb91:22c8:a27b:d5f4:6885:4d82:7ed4) (Read error: Connection reset by peer) |
| 15:07:24 | <Inst> | (,) primitive writer monad |
| 15:09:09 | <Inst> | (,(,)) etc is fun, albeit unergonomic, and (,) iirc space leaks as non-CPS writer monads leak |
| 15:09:44 | <Inst> | (,) also has a monoid instance, awesome |
| 15:11:29 | <Inst> | (a :: a -> b -> c) <*> (b :: a -> b) = \u -> a u (b u) iirc |
| 15:14:05 | <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 |
| 15:14:38 | <Inst> | i would like some help, though, with the weirdness of liftIO |
| 15:15:00 | <Inst> | oh, I think I understand now |
| 15:15:02 | <Inst> | https://hackage.haskell.org/package/transformers-0.6.1.1/docs/src/Control.Monad.Trans.Maybe.html#MaybeT |
| 15:15:20 | <Inst> | the first liftIO just ids on an IO type, then lifts into the monad transformer |
| 15:16:12 | <raehik> | EvanR: sure, or any libraries that might support a similar pattern |
| 15:16:59 | <raehik> | (I am thinking purely of the latter) |
| 15:18:19 | <EvanR> | using operators instead of do notation turns out to not harm the syntax much |
| 15:20:23 | <EvanR> | but you can't do lambda at type level |
| 15:20:26 | → | eron joins (~eron@168.196.116.143) |
| 15:20:53 | <EvanR> | (in haskell) |
| 15:21:47 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 15:24:49 | × | eron quits (~eron@168.196.116.143) (Client Quit) |
| 15:29:58 | × | qqq quits (~qqq@92.43.167.61) (Read error: Connection reset by peer) |
| 15:30:46 | → | qqq joins (~qqq@92.43.167.61) |
| 15:31:54 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds) |
| 15:35:52 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 15:37:20 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 256 seconds) |
| 15:37:29 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 15:38:09 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 15:38:53 | <Inst> | this is now in... https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/required_type_arguments.html#:~:text=A%20required%20type%20argument%20is,required%20type%20arguments%2C%20if%20any. |
| 15:39:12 | <Inst> | I suspect there's fundamental reasons type lambdas won't be included, but one day... your types will be written in do notation! |
| 15:40:02 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 15:41:19 | <cheater> | so what would a simple type look like in do notation? |
| 15:41:29 | <cheater> | like foo :: Bar -> Baz -> Quux |
| 15:41:40 | <cheater> | what does that look like in do notation? |
| 15:41:52 | <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 |
| 15:42:44 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:42:58 | <EvanR> | cheater, imagine datakinds, where the constructors of a type like Either are promoted to types themselves |
| 15:43:17 | <EvanR> | function types are not a good example for this |
| 15:43:19 | <cheater> | unable to |
| 15:43:30 | JuanDaugherty | is now known as Lycurgus |
| 15:43:48 | × | Lycurgus quits (~juan@user/JuanDaugherty) (Changing host) |
| 15:43:48 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 15:43:51 | × | kimiamania quits (~671c7418@user/kimiamania) (Quit: PegeLinux) |
| 15:44:29 | × | EvanR quits (~EvanR@user/evanr) (Quit: Leaving) |
| 15:44:36 | → | kimiamania joins (~76637481@user/kimiamania) |
| 15:45:23 | × | kimiamania quits (~76637481@user/kimiamania) (Client Quit) |
| 15:45:28 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 255 seconds) |
| 15:47:58 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 15:48:42 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 15:49:02 | → | kimiamania joins (~76637481@user/kimiamania) |
| 15:50:15 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 15:50:45 | → | EvanR joins (~EvanR@user/evanr) |
| 15:50:58 | × | nschoe quits (~nschoe@2a01:e0a:8e:a190:aa00:da1d:4eed:33ec) (Quit: ZNC 1.8.2 - https://znc.in) |
| 15:51:15 | → | nschoe joins (~nschoe@2a01:e0a:8e:a190:1a14:5923:b0ce:d13e) |
| 15:53:21 | <Inst> | cheater: (do Bar) -> do foo <- Baz; Quux foo? |
| 15:53:41 | <cheater> | i don't know |
| 15:53:46 | <cheater> | are you asking me? |
| 15:54:00 | <Inst> | It's a suggestion |
| 15:54:20 | <Inst> | actually, that doesn't even work out |
| 15:54:20 | <Inst> | :( |
| 15:54:41 | <Inst> | would be closer to |
| 15:54:43 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 15:54:54 | <Inst> | ehhh, probably not |
| 15:55:09 | <Inst> | I am really not versed on dependent types |
| 15:55:43 | <Inst> | but how far does -XRequiredTypeArguments bring us to DTs? |
| 15:59:24 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 255 seconds) |
| 16:00:03 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: Lycurgus) |
| 16:01:28 | <ncf> | sounds like it has nothing to do with it |
| 16:01:36 | <ncf> | this is just a matter of implicit vs explicit? |
| 16:02:44 | × | esph quits (~weechat@user/esph) (Ping timeout: 268 seconds) |
| 16:03:21 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:03:29 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 16:04:08 | × | haocrcmt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 16:04:14 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 16:04:16 | × | danse-nr3 quits (~danse-nr3@151.35.170.130) (Ping timeout: 268 seconds) |
| 16:05:27 | <raehik> | Inst: no closer, it's just handy for certain type-to-term code |
| 16:05:47 | <Inst> | it's technically bringing type level down to term level |
| 16:06:11 | <raehik> | sometimes you still need to use Proxy#, but in many cases where you're spamming TypeApplications, RequiredTypeArguments can simplify your syntax |
| 16:06:20 | <Inst> | also, iirc, my usage of typeapplications has been wonky :( |
| 16:06:23 | <raehik> | (and clarify how functions should be used) |
| 16:06:23 | <ncf> | no it's not?? it's just syntax |
| 16:06:57 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 16:07:00 | <raehik> | Inst: it might appear so but it's really just a special way to specify typevars in a function! |
| 16:07:29 | → | euphores joins (~SASL_euph@user/euphores) |
| 16:09:41 | <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 |
| 16:09:42 | <Inst> | <3 |
| 16:11:30 | × | euphores quits (~SASL_euph@user/euphores) (Client Quit) |
| 16:11:45 | <raehik> | (typeclasses can be polymorphic over kind btw) |
| 16:11:49 | <raehik> | https://github.com/raehik/binrep/blob/8d10873c0416e8785e55c205559a8c0b0ade05ae/src/Binrep/BLen.hs#L54 |
| 16:12:02 | <Inst> | erm, should have done a :: type |
| 16:12:38 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 16:16:48 | → | esph joins (~weechat@user/esph) |
| 16:17:59 | <raehik> | i didn't realize for a very long time GHC is auto-polymorphic on typeclass args |
| 16:18:05 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 16:18:31 | <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 |
| 16:18:44 | <Inst> | also wtf |
| 16:19:05 | <Inst> | instance GenericFoldMap BLen where |
| 16:19:11 | <Inst> | a class is an instance of a class? |
| 16:19:37 | <raehik> | yeah xD since `BLen :: Type -> Constraint`! |
| 16:19:59 | → | greenflower joins (~greenflow@2409:4071:4d4b:d3ae:27cf:a6f5:bf97:a564) |
| 16:19:59 | → | euphores joins (~SASL_euph@user/euphores) |
| 16:20:12 | <raehik> | and GenericFoldMap only uses its type as a tag/index, never instantiates it, so it can be any kind haha |
| 16:22:17 | Inst | 's brain explodes |
| 16:22:28 | <Inst> | phantom-typed typeclasses |
| 16:23:02 | <raehik> | pretty much exactly where you'd want RequiredTypeArguments, because they're inherently ambiguous |
| 16:23:32 | <Inst> | the typedef inside the instance dec is also blowing my mind |
| 16:23:43 | <Inst> | what don't I know about typeclasses and instances (without extensions)? |
| 16:23:46 | <Inst> | probably a hell of a lot :( |
| 16:24:00 | <raehik> | That's an associated type family. Nothing special, just a type family that belongs to a class |
| 16:24:09 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 252 seconds) |
| 16:24:42 | <Inst> | oh, so it's defined as a type family |
| 16:24:53 | <Inst> | i got confused because i didn't see any extensions on top |
| 16:25:16 | <raehik> | I use a long list of default extensions (i am one of "those" haskellers) |
| 16:29:06 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 16:32:53 | <kuribas> | Who doesn't? |
| 16:33:12 | × | greenflower quits (~greenflow@2409:4071:4d4b:d3ae:27cf:a6f5:bf97:a564) (Quit: Client closed) |
| 16:34:00 | × | vglfr quits (~vglfr@158.red-81-45-80.staticip.rima-tde.net) (Ping timeout: 256 seconds) |
| 16:34:02 | → | tzh joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 16:34:45 | <raehik> | I wouldn't know since any codebase I tread I leave behind a wake of GHC2021 and more >:) |
| 16:34:57 | → | vglfr joins (~vglfr@185.124.31.115) |
| 16:35:11 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 16:40:47 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:41:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:44:37 | × | yeitrafferin quits (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) (Quit: Leaving) |
| 16:45:28 | → | Core4466 joins (~rosco@2001:240:242f:d6eb:20db:887f:8f97:4055) |
| 16:48:22 | × | rosco quits (~rosco@2001:240:242f:d6eb:22d4:a19b:ae5c:b29d) (Ping timeout: 268 seconds) |
| 16:48:27 | × | Nixkernal quits (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch) (Ping timeout: 255 seconds) |
| 16:49:21 | × | Eoco quits (~ian@128.101.131.218) (Ping timeout: 255 seconds) |
| 16:49:55 | → | Eoco joins (~ian@128.101.131.218) |
| 16:51:58 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 16:57:27 | × | Eoco quits (~ian@128.101.131.218) (Remote host closed the connection) |
| 16:58:05 | → | Eoco joins (~ian@128.101.131.218) |
| 16:58:16 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 17:02:02 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 17:02:23 | × | Square2 quits (~Square4@user/square) (Ping timeout: 264 seconds) |
| 17:03:25 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 17:14:08 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 17:15:25 | × | vglfr quits (~vglfr@185.124.31.115) (Read error: Connection reset by peer) |
| 17:15:50 | → | vglfr joins (~vglfr@139.47.115.46) |
| 17:20:13 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 17:21:06 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Read error: Connection reset by peer) |
| 17:22:43 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:23:11 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 17:25:31 | × | Inst quits (~Inst@user/Inst) (Read error: Connection reset by peer) |
| 17:26:33 | → | ph88 joins (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 17:27:05 | <ph88> | Does someone know a good termination checker library? Not necessarily to check haskell itself, preferably language agnostic |
| 17:30:13 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 17:33:14 | → | Inst joins (~Inst@user/Inst) |
| 17:33:56 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 17:36:28 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 17:38:21 | <glguy> | Agda, Coq, Isabelle. Any interactive theorem prover is probably going to have something |
| 17:44:41 | <Inst> | raehik: not sure if that's healthy, but I don't care that much anymore |
| 17:44:46 | <Inst> | at least on Tiobe Haskell is clearly ahead of Scala |
| 17:48:15 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 17:49:33 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 272 seconds) |
| 17:50:36 | × | vglfr quits (~vglfr@139.47.115.46) (Read error: Connection reset by peer) |
| 17:50:50 | → | vglfr joins (~vglfr@139.47.115.46) |
| 17:51:00 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 17:51:38 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:51:46 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 17:52:39 | <ph88> | glguy, ye that's good though a bit hard to incorporate into another project i suppose |
| 17:53:33 | <glguy> | Termination checking tends to depend deeply on the thing you're termination checking |
| 17:53:45 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 17:54:05 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 17:54:10 | <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 |
| 17:56:15 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 17:57:57 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 17:58:15 | → | euleritian joins (~euleritia@dynamic-176-004-192-223.176.4.pool.telefonica.de) |
| 18:00:09 | × | p3n quits (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (Quit: ZNC 1.8.2 - https://znc.in) |
| 18:00:13 | <ph88> | glguy, you mean like svb / z3 ? |
| 18:00:25 | <glguy> | yeah |
| 18:01:13 | <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 |
| 18:01:30 | → | p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 18:04:00 | × | euleritian quits (~euleritia@dynamic-176-004-192-223.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:04:18 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 18:05:23 | <monochrom> | That is like what I saw in a math channel a long time ago. Someone asked "Hi how do I solve equations?" |
| 18:05:41 | <glguy> | monochrom: was the answer also SMT? |
| 18:05:41 | <monochrom> | Yeah, how do you solve equations? |
| 18:06:15 | <monochrom> | No one answered. The asker eventually confessed they had merely things like "5x+4=6" in mind. |
| 18:08:26 | <monochrom> | Or maybe I answered. "It depends on the equation." |
| 18:08:50 | <monochrom> | No, I was not that kind. I answered "it is undecidable". |
| 18:10:09 | → | ft joins (~ft@p4fc2a20e.dip0.t-ipconnect.de) |
| 18:11:35 | <monochrom> | Now, let's look at how that actually is equivalent to termination checking, even in practice, even bullet-point-by-bullet-point. |
| 18:13:53 | <monochrom> | The most common cases that average programmers have in mind are like "for (i = 0; i < n; i++)". |
| 18:14:24 | <dolio> | Well, all termination checkers report false results, yeah. |
| 18:14:49 | <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. |
| 18:15:10 | <glguy> | dolio: because all programs eventually terminate even if due to environmental factors? |
| 18:15:22 | <monochrom> | That class just requires solving linear inequalities and is a solved problem. |
| 18:15:34 | <c_wraith> | That usually terminates. if n is not the max int. and nothing in the loop body is mutating i or n. |
| 18:15:45 | <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. |
| 18:16:17 | <c_wraith> | actually, I guess n being the max int *shouldn't* break that, since it's a < |
| 18:16:39 | <dolio> | Because some of its, "this is a smaller value," inferences are wrong depending on how you instantiate the quantifier. |
| 18:17:13 | <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 |
| 18:17:15 | <dolio> | So, you probably can't just use Agda's checker on GHC. |
| 18:17:22 | <c_wraith> | glguy: hah |
| 18:17:47 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Ping timeout: 256 seconds) |
| 18:17:48 | <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. |
| 18:18:57 | <c_wraith> | monochrom: and imagine thinking like a C programmer trying to envision how to get something to prove their huffman tree construction terminates! |
| 18:19:20 | <c_wraith> | (ok, you can cheat and know it needs n-1 merges and therefore use a for loop. but the naive while loop!) |
| 18:19:55 | <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. |
| 18:21:20 | <EvanR> | ph88, and all languages where that is the case have undecidable termination checking, making the question super easy! |
| 18:21:24 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 18:21:38 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 18:21:41 | <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 |
| 18:21:49 | <glguy> | or at least that's why I figure they were doing that |
| 18:22:03 | <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. |
| 18:22:13 | <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. |
| 18:22:46 | <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" |
| 18:22:46 | <glguy> | dolio: doesn't the current checker rely on such properties of (co)data to do termination checking already? |
| 18:22:52 | <dolio> | Because the way you handle finitary data is distinct from infinitary codata. |
| 18:23:06 | <cheater> | glguy: no. it's loop unrolling. |
| 18:23:16 | <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. |
| 18:23:21 | <dolio> | glguy: Yeah, but the new one is better. |
| 18:23:33 | <glguy> | cheater: you have to know how to write a loop to call what you're doing unrolling |
| 18:23:57 | <cheater> | c_wraith: i do a similar thing when auditing software |
| 18:24:02 | <cheater> | i forgot what i called it but |
| 18:24:04 | <glguy> | dolio: any pointer you can recommend if I'm curious to see what changes are coming? |
| 18:24:18 | <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! |
| 18:24:22 | <dolio> | glguy: https://github.com/agda/agda/pull/7152 |
| 18:24:40 | <c_wraith> | monochrom: pfft. *my* BFS can run forever just fine! |
| 18:24:47 | <monochrom> | haha |
| 18:25:19 | <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? |
| 18:25:26 | <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) |
| 18:25:38 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 18:25:59 | <cheater> | you prune calls to unimportant functions like eg logging |
| 18:26:33 | <cheater> | you're left with the actual code of what's happening, hopefully limited to a single screen or two |
| 18:27:13 | <glguy> | dolio: easy: there are two cases so you try one and then the other *nod* |
| 18:27:24 | <EvanR> | data Program = Syscall Argument Program |
| 18:27:27 | <c_wraith> | ... And then my coworker takes every line and puts it at a different place in an inheritance hierarchy before leaving the company. |
| 18:28:20 | <cheater> | obviously |
| 18:28:32 | <dolio> | Anyhow, that's why you use agda2hs. :þ |
| 18:28:42 | <cheater> | what about hs2agda? |
| 18:29:41 | × | xdminsy quits (~xdminsy@117.147.70.203) (Read error: Connection reset by peer) |
| 18:32:02 | <ph88> | EvanR, where -what- exactly is the case? |
| 18:33:06 | <ph88> | dolio, do you have a sources about Agda is (hopefully) soon getting a new termination checker ?? |
| 18:33:26 | <dolio> | ph88: Yeah, see the issue I linked to glguy above. |
| 18:33:28 | → | yeitrafferin joins (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) |
| 18:33:51 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Quit: segfaultfizzbuzz) |
| 18:34:12 | <EvanR> | ph88, "every language is just block entry, block exit, function call, function return" |
| 18:34:27 | <ph88> | dolio, thanks |
| 18:35:01 | <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 |
| 18:35:20 | <EvanR> | can blocks be nested? |
| 18:35:24 | <cheater> | EvanR: why block entry. who are you trying to keep out |
| 18:35:44 | <EvanR> | anyway, halting problems |
| 18:35:49 | <ph88> | EvanR, not sure what you mean by nested. Blocks can be jumped from many other blocks and jump to many other blocks |
| 18:35:56 | <cheater> | what's the deal with halting, anyways? |
| 18:36:01 | <monochrom> | and why block exit, who are you trying to keep in! >:) |
| 18:36:24 | <ph88> | termination checking is more difficult than the halting problem (according to wikipedia) yet there are termination checkers that can check things |
| 18:36:52 | <EvanR> | it's much easier in languages which have sensible structure and not algol style |
| 18:36:55 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 18:37:15 | × | sammelweis quits (~quassel@96.76.243.253) (Ping timeout: 252 seconds) |
| 18:37:15 | → | JeremyB99 joins (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) |
| 18:37:21 | <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" |
| 18:37:40 | <cheater> | and then you have to have an hour long conversation about how they're missing imagination |
| 18:38:02 | <dolio> | Termination checkers that actually get used rule out programs that actually halt, usually. |
| 18:38:03 | × | JeremyB99 quits (~JeremyB99@2607:fb90:2c60:c23b:71e6:b175:b2a9:d342) (Read error: Connection reset by peer) |
| 18:38:05 | <cheater> | missing? lacking |
| 18:38:06 | <EvanR> | you gotta think outside the box, and by outside the box, I mean within the constraints of the problem xD |
| 18:38:16 | <cheater> | precisely. |
| 18:38:30 | <cheater> | to think outside the box, first create a very tiny box, so tiny that only you can crawl into it. |
| 18:38:43 | <cheater> | and within that tiny box, you are unbounded in your freedom. |
| 18:38:47 | <EvanR> | lol |
| 18:38:56 | <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 |
| 18:38:57 | <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. |
| 18:39:11 | <monochrom> | Well the converse holds too. There are other noobs who can solve one special case and dances up and think it generalizes. |
| 18:39:49 | <cheater> | stop throwing shade on AI |
| 18:40:15 | <monochrom> | No I'm throwing shade on humanity itself. AIs are doing great. |
| 18:40:20 | <cheater> | and that "Al", is he in the room with us right now? |
| 18:40:26 | <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) ? |
| 18:41:01 | <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 |
| 18:41:48 | <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. |
| 18:44:03 | <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 ? |
| 18:46:47 | <mauke> | https://www.youtube.com/watch?v=uq-gYOrU8bA |
| 18:47:51 | <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. |
| 18:51:14 | <cheater> | ph88: i would say grow with your checker |
| 18:51:22 | <cheater> | trying to roll your own will teach you a lot of stuff |
| 18:51:31 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 18:51:32 | <cheater> | you'll be able to appreciate more advanced tools better |
| 18:51:47 | <ph88> | thanks monochrom , cheater |
| 18:52:34 | → | JeremyB99 joins (~JeremyB99@208.64.173.20) |
| 18:53:00 | <masaeedu> | ph88: is your goal to implement termination checking for a language implemented in Haskell? |
| 18:56:03 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 272 seconds) |
| 18:57:01 | <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) |
| 18:57:04 | × | dcoutts quits (~duncan@cpc69400-oxfd27-2-0-cust750.4-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 18:57:28 | <monochrom> | :( |
| 18:58:10 | <monochrom> | But you can make it even better with "terminates :: Program -> ()" >:) |
| 18:58:35 | <EvanR> | semi decidable |
| 18:59:09 | <ph88> | masaeedu, ye |
| 18:59:48 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:59:51 | <ph88> | probie, how do you know which things always terminate though? |
| 19:00:09 | × | yeitrafferin quits (~user@2a04:4540:720f:7100:2e2a:b597:1ea7:2921) (Quit: Leaving) |
| 19:00:47 | <monochrom> | We know that primitive recursive functions terminate. We know that System F programs terminate. There are other examples. |
| 19:01:09 | <monochrom> | We know that VCR programs terminate if you don't enable "repeat". |
| 19:01:27 | <ph88> | VCR programs? |
| 19:01:45 | <monochrom> | https://en.wikipedia.org/wiki/Videocassette_recorder |
| 19:01:49 | <ph88> | lol |
| 19:02:09 | <monochrom> | You can tell it "start recording on Tuesday 2PM-3PM" |
| 19:02:27 | <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 |
| 19:02:56 | <monochrom> | What if 99% of your actual programs convert to the unknown case? |
| 19:03:52 | <monochrom> | Or you may reply "no, only 1%". |
| 19:04:01 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 19:04:05 | <monochrom> | Either way, it again proves "it depends". |
| 19:04:26 | <EvanR> | you could interpret the terminatingness using quantum mechanics |
| 19:04:37 | <EvanR> | 99% terminating 1% not |
| 19:04:39 | <probie> | That's an interesting spin on things |
| 19:04:54 | <EvanR> | lol |
| 19:04:58 | <monochrom> | haha |
| 19:05:17 | <monochrom> | Was that "spin" intended pun? :) |
| 19:05:45 | <ph88> | monochrom, i know there is a "a depends". I'm looking for the practical simplest approach to get going |
| 19:05:57 | × | JeremyB99 quits (~JeremyB99@208.64.173.20) (Ping timeout: 256 seconds) |
| 19:06:05 | <probie> | yes, that was the intention |
| 19:07:08 | <mauke> | charming |
| 19:07:20 | <masaeedu> | ph88: a really simple solution is to simply banish direct recursion from your language. |
| 19:08:27 | <masaeedu> | whether this is feasible depends on what your language is used for |
| 19:08:34 | <masaeedu> | but e.g. Dhall uses this approach to great effect |
| 19:08:53 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 19:09:01 | → | JeremyB99 joins (~JeremyB99@208.64.173.20) |
| 19:11:05 | <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) |
| 19:12:36 | <ph88> | oh lambda cube, i saw that before ^^ |
| 19:13:08 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:13:54 | × | JeremyB99 quits (~JeremyB99@208.64.173.20) (Ping timeout: 268 seconds) |
| 19:15:15 | <masaeedu> | yeah, Dhall implements a lot of really cool ideas |
| 19:15:29 | <masaeedu> | in this case what's relevant is the absence of a feature |
| 19:15:58 | <ph88> | related http://neilmitchell.blogspot.com/2020/11/turing-incomplete-languages.html |
| 19:16:08 | <masaeedu> | i.e. you just can't do the direct recursion that makes termination checking necessary |
| 19:17:26 | <monochrom> | I am not thrilled at guaranteed-termination languages in the context of "I want to learn/build termination checking"> |
| 19:18:08 | <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". |
| 19:19:34 | <int-e> | . o O ( https://xkcd.com/246/ ) |
| 19:20:12 | <masaeedu> | I'm not meaning to suggest you'd prohibit direct recursion and then build a termination checker anyway |
| 19:21:15 | → | Rodney_ joins (~Rodney@176.254.244.83) |
| 19:21:53 | <masaeedu> | Only to say that, depending on your needs, you can go quite a long ways without direct recursion |
| 19:23:52 | × | tv quits (~tv@user/tv) (Ping timeout: 246 seconds) |
| 19:25:43 | <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. |
| 19:28:09 | → | rosco joins (~rosco@2001:240:242f:d6eb:ca19:e23f:936a:839f) |
| 19:29:16 | <masaeedu> | the only question is how to limit the progam's use of direct recursion so that termination is still guaranteed. |
| 19:29:26 | <masaeedu> | and the simplest limitation i can think of is to just ban it |
| 19:30:46 | × | Core4466 quits (~rosco@2001:240:242f:d6eb:20db:887f:8f97:4055) (Ping timeout: 256 seconds) |
| 19:30:49 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:32:16 | → | dispater- joins (~dispater@217.155.58.82) |
| 19:32:45 | → | orcus joins (~orcus@217.155.58.82) |
| 19:35:10 | × | orcus quits (~orcus@217.155.58.82) (Remote host closed the connection) |
| 19:35:10 | × | dispater- quits (~dispater@217.155.58.82) (Remote host closed the connection) |
| 19:37:33 | → | tv joins (~tv@user/tv) |
| 19:38:19 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:38:37 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 19:39:41 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 19:41:45 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 19:41:47 | → | dcoutts joins (~duncan@cpc69400-oxfd27-2-0-cust750.4-3.cable.virginm.net) |
| 19:41:58 | → | dispater- joins (~dispater@217.155.58.82) |
| 19:42:25 | × | jinsun quits (~jinsun@user/jinsun) (Read error: Connection reset by peer) |
| 19:42:28 | → | orcus joins (~orcus@217.155.58.82) |
| 19:43:11 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 19:44:09 | → | JeremyB99 joins (~JeremyB99@208.64.173.20) |
| 19:44:30 | <monochrom> | Or the goal is to learn termination checking. |
| 19:46:43 | <masaeedu> | that could be. iirc they were asking for a library that implements termination checking that could be dropped into their project |
| 19:46:59 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 19:47:12 | <monochrom> | Then perhaps too late to rewrite the project. |
| 19:48:33 | → | cheater_ joins (~Username@user/cheater) |
| 19:48:52 | <monochrom> | But let's talk about interesting normal forms! |
| 19:49:51 | × | cheater_ quits (~Username@user/cheater) (Read error: Connection reset by peer) |
| 19:50:04 | × | cheater quits (~Username@user/cheater) (Ping timeout: 256 seconds) |
| 19:50:30 | <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") |
| 19:50:35 | → | cheater_ joins (~Username@user/cheater) |
| 19:50:35 | cheater_ | is now known as cheater |
| 19:52:26 | <monochrom> | In von Neumann computing, every program is interpreted by the CPU, i.e., one "simple" loop over a manifestly terminating loop body. |
| 19:53:44 | <monochrom> | Some programmers even emulate a version of that by hand (CPS transform then trampolining) in Javascript and Python to support unlimited recursion depth. |
| 19:53:52 | <int-e> | this may take a WHILE |
| 19:55:29 | <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. |
| 19:58:10 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:59:15 | <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. |
| 19:59:29 | <monochrom> | err s/computing/computable/ |
| 20:02:30 | <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. |
| 20:02:33 | <int-e> | There's also the logical version where you need exactly one unbounded existential quantifier to describe a r.e. set. |
| 20:02:57 | <monochrom> | Yeah, that one. |
| 20:05:05 | × | JeremyB99 quits (~JeremyB99@208.64.173.20) (Ping timeout: 272 seconds) |
| 20:05:35 | → | JeremyB99 joins (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 20:06:15 | <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". |
| 20:07:13 | × | dispater- quits (~dispater@217.155.58.82) (Remote host closed the connection) |
| 20:07:14 | × | orcus quits (~orcus@217.155.58.82) (Remote host closed the connection) |
| 20:08:04 | <monochrom> | Oh yeah and of course every monad factorable to right.left :) |
| 20:11:04 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:11:43 | → | orcus joins (~orcus@217.155.58.82) |
| 20:11:47 | × | orcus quits (~orcus@217.155.58.82) (Client Quit) |
| 20:14:53 | <masaeedu> | > Every total computing function equals (some catamorphism) . (some anamorphism) |
| 20:14:55 | <lambdabot> | error: |
| 20:14:55 | <lambdabot> | Data constructor not in scope: |
| 20:14:55 | <lambdabot> | Every |
| 20:14:59 | <masaeedu> | that's interesting. do you have a reference for that? |
| 20:15:01 | <masaeedu> | whoops |
| 20:15:52 | → | Square joins (~Square@user/square) |
| 20:16:59 | × | JeremyB99 quits (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 20:18:26 | × | rosco quits (~rosco@2001:240:242f:d6eb:ca19:e23f:936a:839f) (Read error: Connection reset by peer) |
| 20:18:34 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:18:41 | → | rosco joins (~rosco@aq028228.dynamic.ppp.asahi-net.or.jp) |
| 20:18:41 | <monochrom> | I forgot. Maybe one of those recursion scheme papers. |
| 20:19:09 | → | JeremyB99 joins (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 20:22:09 | → | n8n joins (n8n@user/n8n) |
| 20:23:44 | × | JeremyB99 quits (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 20:26:45 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 20:27:14 | → | JeremyB99 joins (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 20:27:15 | × | JeremyB99 quits (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 20:27:37 | <probie> | :t \h -> let hylo f g = let go = f . fmap go . g in go in hylo (uncurry (.)) (\x -> (x,x)) h () |
| 20:27:38 | <lambdabot> | (b -> b) -> b |
| 20:28:46 | → | dispater- joins (~dispater@217.155.58.82) |
| 20:29:22 | × | ph88 quits (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Quit: Leaving) |
| 20:30:46 | → | orcus joins (~orcus@217.155.58.82) |
| 20:31:08 | <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 |
| 20:31:09 | <lambdabot> | 120 |
| 20:32:03 | × | orcus quits (~orcus@217.155.58.82) (Remote host closed the connection) |
| 20:32:03 | × | dispater- quits (~dispater@217.155.58.82) (Remote host closed the connection) |
| 20:37:29 | → | JeremyB99 joins (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 20:37:54 | × | JeremyB99 quits (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 20:38:53 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:39:20 | × | phma quits (phma@2001:5b0:215a:e298:fd17:443b:b4a0:861c) (Read error: Connection reset by peer) |
| 20:40:13 | → | phma joins (phma@2001:5b0:210d:72b8:fcdc:5db1:5990:c6e2) |
| 20:40:19 | <Inst> | question: is it me, or did, in the past few months, Haskell give up? |
| 20:40:37 | <Rembane> | Inst: It's you |
| 20:40:47 | <probie> | What does it mean for a programming language to "give up"? |
| 20:41:12 | <Inst> | i'll drop it, it's silly |
| 20:41:23 | <Inst> | just seems as though there's nothing fun happening these days |
| 20:41:47 | <int-e> | that's totally you |
| 20:42:16 | <Inst> | https://downloads.haskell.org/ghc/latest/docs/users_guide/9.8.1-notes.html |
| 20:42:28 | <monochrom> | That's a sign of a language actually used in anger. |
| 20:43:03 | <monochrom> | You don't hear C, an actually used language, go "we have a new type system extension!" even every year. |
| 20:44:03 | <probie> | C may have avoided that, but languages seem to bolt on new features at an alarming rate these days |
| 20:44:12 | <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 |
| 20:44:23 | <Inst> | i guess he forgot :( |
| 20:44:24 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:44:34 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:44:52 | <Inst> | let's see, while i was busy |
| 20:44:53 | <Inst> | https://downloads.haskell.org/ghc/latest/docs/users_guide/9.8.1-notes.html |
| 20:46:15 | <int-e> | so "nothing fun is happening" means "nobody's implementing the one feature I currently care about in this moment"? |
| 20:46:25 | <Inst> | i don't even care about it |
| 20:46:29 | <Inst> | i'm not on windows anymore |
| 20:46:39 | → | JeremyB99 joins (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 20:46:44 | <Inst> | 9.8 is sort of boring, no new extensions |
| 20:47:00 | <Inst> | https://downloads.haskell.org/ghc/9.10.1-alpha2/docs/users_guide/9.10.1-notes.html |
| 20:47:07 | <Inst> | GHC2024 is a big improvement |
| 20:48:17 | <monochrom> | Actually C regresses: https://queue.acm.org/detail.cfm?id=3588242 then look for "incendiary realloc" |
| 20:49:47 | → | random-jellyfish joins (~developer@2a02:2f04:11e:c600:71fb:90e9:99e2:5642) |
| 20:49:47 | × | random-jellyfish quits (~developer@2a02:2f04:11e:c600:71fb:90e9:99e2:5642) (Changing host) |
| 20:49:47 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 20:49:51 | <monochrom> | The sign of an actually used language: The standard committee is so bored, they start to take away prior guarantees that users need. >:) |
| 20:50:55 | <Inst> | is that actually a bad thing? :) |
| 20:50:59 | <probie> | > C23 declares realloc(ptr,0) to be undefined behavior |
| 20:51:01 | <monochrom> | Oh wait GHC2024 has dropped? |
| 20:51:32 | <Inst> | lambdacase finally made the cut |
| 20:51:34 | <probie> | Inst: An idiom for `free` now no longer promises to free for no good reason? That seems rather dangerous |
| 20:51:36 | <Inst> | well, technically no |
| 20:51:56 | <Inst> | 9.10.1 hasn't hit rc1 status yet |
| 20:52:07 | <monochrom> | It's why the article says this new standard sets the whole world on fire. |
| 20:53:08 | <monochrom> | I feel like not enough people make this drama go viral on social media and cause an uproar. |
| 20:53:52 | <monochrom> | Then again who has time for social media drama with a actual programming job. Like I said, sign of a language actually used. |
| 20:54:04 | <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. |
| 20:54:16 | <monochrom> | heh |
| 20:54:53 | <c_wraith> | "Developers who manage to figure out what the standard actually means are frequently appalled." truer words never spoken of C |
| 20:54:57 | <mauke> | finally I can zero-initialize my variables with = {} |
| 20:55:01 | <mauke> | = {0} was just too long |
| 20:55:07 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 272 seconds) |
| 20:55:09 | <Inst> | isn't there a substantial population of developers for which writing everything in C isn't a major loss? |
| 20:55:42 | <cheater> | mauke thinking like a true C-nile |
| 20:55:43 | <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++. |
| 20:56:02 | <int-e> | monochrom: How have I not heard of this C23 insanity. |
| 20:56:32 | <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'. |
| 20:56:35 | <monochrom> | Then again I do the same, just with Haskell instead, or sometimes Lean when in the right context. :) |
| 20:56:42 | <int-e> | I guess it's fine since nobody is using C in 2024, right... *cries into a pillow* |
| 20:56:46 | <probie> | monochrom: I avoid this problem by just hating all languages |
| 20:57:09 | <Inst> | i'm guessing the fun stuff right now is GHCJS and Asterius (wasm) backends |
| 20:57:37 | <cheater> | probie: me, but programmers |
| 20:57:48 | <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. |
| 20:58:00 | <EvanR> | people who say everything should be written in C are ridiculous. Obviously everything should be written in rust |
| 20:58:20 | <cheater> | he said the r-word |
| 20:58:24 | <Inst> | i'm just saying meeting julia community it's obvious that different programmers have different use cases for programming languages |
| 20:58:26 | <int-e> | EvanR: what are you using as flame repellent? |
| 20:58:38 | <Inst> | i'm hypothesizing there exists a group of developers for which C covers all of their needs |
| 20:58:44 | <EvanR> | tellurium |
| 20:58:50 | <jle`> | arduino programmers |
| 20:58:52 | <mauke> | "it's impossible to implement the standard memmove() function efficiently in standard C" - how is that an issue? |
| 20:59:24 | <jle`> | actually i take that back, arduiono programmers need better than C |
| 20:59:35 | <mauke> | (also, depends on your definition of "efficiently") |
| 21:01:41 | <c_wraith> | jle`: I seem to recall a lot of discussion of python on arduino |
| 21:01:53 | <monochrom> | Actually the other angle is that whatever C23 decrees is becoming irrelevant anyway. |
| 21:02:10 | <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 |
| 21:02:45 | → | dispater- joins (~dispater@217.155.58.82) |
| 21:02:47 | × | JeremyB99 quits (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 21:03:14 | → | orcus joins (~orcus@217.155.58.82) |
| 21:03:19 | <benjaminl> | I mostly write new stuff in rust, but there's a *huge* body of existing C code that needs to be maintained |
| 21:03:53 | <Inst> | iirc Haskell can FFI effortlessly into C, but it can only FFI into Rust with difficulty |
| 21:04:02 | <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. |
| 21:04:03 | × | motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 255 seconds) |
| 21:04:19 | <c_wraith> | "effortlessly" is an exaggeration if the C api is complicated at all... |
| 21:04:33 | <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. |
| 21:04:34 | <benjaminl> | yeah, C is basically the only cross-language ABI |
| 21:04:35 | <monochrom> | And in the case of embedded systems, you are wedded to the extra guarantees of the compiler and platform anyway. |
| 21:04:48 | <benjaminl> | if you want to FFI into not-C stuff, you have to lower the not-C to the C ABI first |
| 21:05:04 | <dolio> | What does this have to do with writing every program in C? |
| 21:05:05 | <int-e> | probie: I'm also certainly not one of the people who's advocating to use Rust for everything. |
| 21:05:19 | <monochrom> | And finally in the case of school assignments (which is what I actually know professionally), you just use C as an Algol. |
| 21:05:25 | <Inst> | well my point is that writing every program in C is correct |
| 21:05:36 | <Inst> | if you are a programmer for which every program you need to write is best written in C |
| 21:05:49 | × | orcus quits (~orcus@217.155.58.82) (Remote host closed the connection) |
| 21:05:49 | × | dispater- quits (~dispater@217.155.58.82) (Remote host closed the connection) |
| 21:05:50 | <dolio> | Your point is that you didn't read what I wrote? |
| 21:05:53 | <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...) |
| 21:06:22 | <int-e> | I get what all the lifetimes are for, but they can be a burden. |
| 21:06:37 | <benjaminl> | monochrom: IME most C implementations that exist don't define enough of the UB from the standard to really make a dent |
| 21:06:43 | <Inst> | well we got on a tangent from "write it in c" |
| 21:07:27 | <benjaminl> | like... pretty sure gcc still treats side-effect-free infinite loops as UB, for example |
| 21:07:55 | → | JeremyB99 joins (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) |
| 21:08:03 | × | JeremyB99 quits (~JeremyB99@2607:fb90:d3e2:c1c0:d8ad:9a0c:599d:8ce5) (Read error: Connection reset by peer) |
| 21:08:03 | <Inst> | EvanR: how's the macro community in Rust? |
| 21:08:09 | → | dispater- joins (~dispater@217.155.58.82) |
| 21:08:18 | × | michalz quits (~michalz@185.246.207.215) (Quit: ZNC 1.8.2 - https://znc.in) |
| 21:08:18 | <Inst> | afaik the problem with Rust is ergonomics, but it seems as though their macros can fix all their ergo needs |
| 21:08:24 | × | dispater- quits (~dispater@217.155.58.82) (Remote host closed the connection) |
| 21:09:07 | <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... |
| 21:09:53 | <monochrom> | Quickly I realized how much I have presumed either GC or malloc/free all my life subconsciously. |
| 21:11:49 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 21:12:26 | → | zetef joins (~quassel@5.2.182.98) |
| 21:12:47 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 21:12:57 | <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. |
| 21:16:24 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:18:52 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 21:20:57 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 21:21:11 | → | gorignak joins (~gorignak@user/gorignak) |
| 21:21:20 | × | gorignak quits (~gorignak@user/gorignak) (Client Quit) |
| 21:25:15 | × | flukiluke quits (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Ping timeout: 268 seconds) |
| 21:25:34 | → | flukiluke joins (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
| 21:25:42 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 21:26:25 | <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. |
| 21:26:52 | × | noumenon quits (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 21:28:17 | → | madeleine-sydney joins (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 21:28:34 | → | Square2 joins (~Square4@user/square) |
| 21:31:58 | × | Square quits (~Square@user/square) (Ping timeout: 255 seconds) |
| 21:32:18 | <monochrom> | OK GHC2024. I don't like DataKinds, GADTs, MonoLocalBinds. :( |
| 21:32:35 | <c_wraith> | wait. MonoLocalBinds should never be on by default :( |
| 21:33:09 | <monochrom> | There is consolation in "GHC2021 remains the default langauge" even for 9.10. |
| 21:33:23 | <int-e> | monochrom: do DataKinds or GADTs actively hurt you? |
| 21:33:35 | <c_wraith> | GADTs turns on MonoLocalBinds |
| 21:33:38 | <int-e> | (Also GADTs are nice, but obviously that's an opinion.) |
| 21:33:56 | <int-e> | Ah. That's fair I guess. |
| 21:33:59 | <monochrom> | IIRC IIUC GADTs is better with MonoLocalBinds, so that's why. Blame it on GADTs. >:( |
| 21:34:31 | <monochrom> | int-e, I am just being right-wing conservative. :) |
| 21:34:44 | <monochrom> | reactionary actually :D |
| 21:35:12 | <monochrom> | But I'm happy with LambdaCase. But I'm unhappy with how MultiwayIf is still out. |
| 21:35:36 | <monochrom> | Do people really hate anything remotely resembling if-then-else that much? |
| 21:36:09 | <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 |
| 21:36:41 | <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". |
| 21:37:22 | <monochrom> | And each of the two "..."s contain one more genuine if-then-else i.e. inequalities not reducible to pattern matching. |
| 21:37:53 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 21:37:57 | <int-e> | I usually find a way to write that with guards |
| 21:37:58 | <monochrom> | Hot take unpopular opinion: Pattern matching is overrated. There is such a thing as pattern matching blindness, too. |
| 21:38:36 | <monochrom> | MultiwayIf is just guards without needing a declaration. Why not admit it into GHC2024. |
| 21:39:31 | <dolio> | Isn't multiway if kind of gnarly? |
| 21:39:40 | <monochrom> | I say no! |
| 21:39:55 | <dolio> | Like, if you end up nesting them it's difficult to parse or something. |
| 21:40:31 | <dolio> | Like, the feature is fine, but the syntax is bad, or something. |
| 21:40:39 | <monochrom> | Hrm. I wouldn't mind being forced to add parentheses to help both computer and humans. |
| 21:40:52 | <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 |
| 21:41:17 | <monochrom> | But I understand that this is another unpopular opinion. People irrationally hate parentheses too. |
| 21:41:37 | × | it_ quits (~quassel@v2202212189510211193.supersrv.de) (Quit: No Ping reply in 180 seconds.) |
| 21:41:54 | <Inst> | if you're inline nesting with multiway if / guards you're doing it wrong |
| 21:42:07 | <Inst> | this is haskell, just stuff some stuff in let expression / where clause and call it a day |
| 21:42:12 | <monochrom> | Oh they have a layout rule for that. So yeah problem solved? (OK I admit lack of imagination.) |
| 21:42:48 | <monochrom> | But I haven't actually needed nesting in my use case. |
| 21:43:32 | <monochrom> | Like I said I wouldn't even mind banning nesting, requiring me to add parentheses. |
| 21:44:03 | <int-e> | I guess I just don't find `case () of` too onerous so I never went looking for MultiWayIf |
| 21:44:21 | <monochrom> | :( |
| 21:44:48 | <int-e> | I do agree that it looks harmless enough so it could've been included in GHC2024 |
| 21:45:10 | <monochrom> | BTW it is `case () of _` to be complete. >:) |
| 21:45:11 | <int-e> | So maybe nobody asked |
| 21:45:18 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:45:20 | <int-e> | monochrom: yes I know |
| 21:45:39 | <int-e> | monochrom: the _ needs to be repeated for every case too |
| 21:45:42 | <int-e> | err |
| 21:45:44 | <yushyin> | the examples from the \cases proposal suggests that you can often use it instead of MultiWayIf |
| 21:45:54 | <int-e> | no... |
| 21:46:00 | int-e | is just stupid |
| 21:46:09 | <int-e> | (you /can/ repeat it of course) |
| 21:46:12 | <monochrom> | I will wait for GHC2050ArcticIcesheetAllMeltedEdition" |
| 21:46:55 | <monochrom> | yushyin, my said use case does not want a lambda either. |
| 21:46:56 | → | it_ joins (~quassel@v2202212189510211193.supersrv.de) |
| 21:47:30 | <monochrom> | I already know how to encode everything in terms of everything else stop telling me I could have written it in Core heh |
| 21:48:17 | <int-e> | Haskell isn't reductive. It's part of its charm. |
| 21:48:48 | <Inst> | btw, pattern guards doesn't support ;, right? |
| 21:49:59 | <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 |
| 21:50:28 | <int-e> | monochrom: at least your comments have a point |
| 21:50:38 | <monochrom> | Right, pattern guards don't have a notion of ; or layout at all. |
| 21:50:49 | <Inst> | no, because , is a substitute for && |
| 21:50:57 | <Inst> | ; could be a substitute for or |
| 21:51:01 | <Inst> | || |
| 21:51:10 | <monochrom> | Ugh how could anyone guess that. |
| 21:51:18 | <Inst> | only if they prolog too much |
| 21:51:32 | <monochrom> | You need to hear my favourite true story. |
| 21:51:57 | <Inst> | Seems like I do. |
| 21:52:07 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:52:12 | <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. |
| 21:52:14 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 21:52:37 | <monochrom> | The people in the small office kept asking him "Will it support 1048"? |
| 21:52:46 | <monochrom> | Can you guess what "1048" meant? |
| 21:53:24 | <c_wraith> | some local version of y2k? |
| 21:53:29 | <monochrom> | How is any outsider supposed to guess a homebrew insider abbreviation from an echo chamber? |
| 21:53:42 | <monochrom> | Answer: 1024x768 resolution. |
| 21:54:03 | <c_wraith> | I thought about that, but rejected it because 24 /= 48 |
| 21:55:07 | <Inst> | uhhh, where did the 48 come from? |
| 21:55:45 | <int-e> | . o O ( XGA ) |
| 21:55:47 | <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. |
| 21:56:50 | × | orcus- quits (~orcus@mail.brprice.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 21:56:50 | × | dispater quits (~dispater@mail.brprice.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 21:57:31 | <Inst> | btw, you can inject layout into pattern guards :) |
| 21:57:48 | × | it_ quits (~quassel@v2202212189510211193.supersrv.de) (Quit: No Ping reply in 180 seconds.) |
| 21:58:27 | <Inst> | foo | True, Nothing <- do {Just 5; Nothing} = 5 |
| 21:58:39 | → | dispater joins (~dispater@mail.brprice.uk) |
| 21:59:03 | → | it_ joins (~quassel@v2202212189510211193.supersrv.de) |
| 21:59:09 | → | orcus joins (~orcus@mail.brprice.uk) |
| 21:59:20 | <monochrom> | Supporting "or" in pattern guards is as hard as supporting "or" patterns in general. I say this to mean no one has really worked out all the details and written up a complete proposal. |
| 22:00:09 | <monochrom> | So it remains one of those "every 3 months someone adds it to their wish list, but don't hold your breath". |
| 22:00:22 | <Inst> | yeah, because foo | True, Nothing <- do; Just 5; Nothing = 5 is valid, so you'd have issues figuring out whether the semicolon belongs to the injected layout or the top-level layout. |
| 22:00:29 | <monochrom> | And that brings us to: You need to hear my favourite Aesop fable, too. |
| 22:01:58 | <Inst> | okay |
| 22:02:15 | <monochrom> | At the international conference of mice, to add an early warning system against cat attacks, they passed two resolutions uanimously. 1. Someone should put a bell on the cat's neck. 2. Someone else should do it. |
| 22:02:34 | × | it_ quits (~quassel@v2202212189510211193.supersrv.de) (Client Quit) |
| 22:03:56 | → | it_ joins (~quassel@v2202212189510211193.supersrv.de) |
| 22:05:45 | <ncf> | ocaml folks figured it out, it can't be rocket science :) |
| 22:06:28 | <monochrom> | They solved that by selling their souls to Jane Street, no? |
| 22:06:51 | <monochrom> | in which case it's financial quant science, which is harder :) |
| 22:07:29 | <monochrom> | That option trading equation I saw on that Veritasium video is certainly much harder than the rocket equation :) |
| 22:07:32 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:07:36 | <Inst> | | is reserved, but here's a different question: do you discard the bindings from previous or do you keep them? |
| 22:08:01 | × | remmie quits (ianremsen@tilde.team) (Ping timeout: 246 seconds) |
| 22:08:22 | <monochrom> | On the "bright" side it also earned someone a lot more money and enabled him to be a charity for science research and the Quanta Magazine. |
| 22:09:04 | × | orcus quits (~orcus@mail.brprice.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:09:24 | → | orcus joins (~orcus@mail.brprice.uk) |
| 22:10:21 | <monochrom> | Well SPJ tried the finance quant way too. He wrote papers on how to write convoluted bond contracts in Haskell do-notation. |
| 22:10:46 | <monochrom> | But it was the same kind of contracts that brought down everything, remember? >:) |
| 22:11:25 | <Inst> | we're sort of unlucky in that way; OCaml survives because of Jane Street picking it on a whim |
| 22:11:33 | <duncan> | ML.mwwwrrrrreoooow |
| 22:11:34 | <monochrom> | I almost could credibly spread the rumour "you can blame it on SPJ" >:) |
| 22:12:34 | <Inst> | well you can also blame F# on SPJ |
| 22:12:42 | <monochrom> | I am actually ready to agree that for the purpose of number crunching, laziness gets in the way, so yeah don't pick Haskell for that actually. |
| 22:13:35 | <monochrom> | But laziness would be right for do-notation kind of things. |
| 22:14:45 | <monochrom> | You use it when you write like "foo = xxx >> foo" for a toy example. |
| 22:15:32 | → | sprout_ joins (~quassel@2a02-a448-3a80-0-d844-6577-cb5e-d92a.fixed6.kpn.net) |
| 22:16:57 | <int-e> | @quote DSL.*CPU |
| 22:16:57 | <lambdabot> | Jafet says: Javascript is pretty much a DSL for making your web browser take up more CPU |
| 22:17:16 | <int-e> | (I was checking whether lambdabot had one about Haskell being a DSL for writing compilers, but it doesn't) |
| 22:17:56 | → | Athas_ joins (athas@sigkill.dk) |
| 22:18:20 | <Inst> | \\\\\/join ##polotics |
| 22:18:30 | <monochrom> | Inst: Do you mean like this? | Just x <- foo -> this branch can use x | [y] <- bar -> this branch can use y but not x |
| 22:18:55 | <monochrom> | Then the answer is like that, the 2nd branch cannot use the x from the 1st branch. |
| 22:19:11 | × | sprout quits (~quassel@84-80-106-227.fixed.kpn.net) (Ping timeout: 264 seconds) |
| 22:19:47 | × | Athas quits (athas@sigkill.dk) (Ping timeout: 264 seconds) |
| 22:20:35 | <Inst> | if yoou're doing or patterns on a single guard, it could be useful, but it'd cause confusion |
| 22:20:36 | <geekosaur> | #polotics? arguments about little wooden balls that are swatted from horseback? 😛 |
| 22:20:43 | <Inst> | guards are already quite cryptic enough already |
| 22:21:15 | × | zetef quits (~quassel@5.2.182.98) (Remote host closed the connection) |
| 22:23:27 | <Inst> | sorry, mistell |
| 22:26:06 | <monochrom> | Oh here is how I remember it's <- not ->. It is either <- or ->, but -> is already taken ("case foo of Just x ->"), so it can only be <- |
| 22:26:38 | <monochrom> | I think someone also mentioned that "Just x <- foo" is also what you would write in list comprehension. |
| 22:27:28 | → | remmie joins (ianremsen@tilde.team) |
| 22:28:15 | <monochrom> | Oh and my favourite BlockArguments did not make it into GHC2024 either. |
| 22:31:36 | × | caubert quits (~caubert@user/caubert) (Read error: Connection reset by peer) |
| 22:31:54 | → | caubert joins (~caubert@user/caubert) |
| 22:34:29 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 22:49:40 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 22:53:31 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 22:54:40 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 22:57:54 | <EvanR> | Inst, sorry. "the macro community"? I guess I should scroll up |
| 22:58:12 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 22:58:21 | × | trev quits (~trev@user/trev) (Ping timeout: 255 seconds) |
| 22:58:28 | × | PiDelport quits (uid25146@id-25146.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 22:58:32 | <Inst> | Oh, sorry for the question, I was just surprised how nice they got things by abusing macros. I'm curious as to what the limits of macro-driven Rust looks like |
| 22:59:22 | <monochrom> | Everyone absues everything in sight. |
| 22:59:34 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 23:00:09 | → | trev joins (~trev@user/trev) |
| 23:00:25 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 23:01:23 | <monochrom> | I was also planning to comment that DataKinds and GADTs (and not quality-of-lift improvements for vanilla functional programming) making it into GHC2024 is a sign that it is popular to abuse GHC extensions to emulate dependent typing. (Who/Why else would add GADTs to the next generation default?) |
| 23:01:40 | <monochrom> | s/quality-of-lift/quality-of-life/ |
| 23:06:41 | <ski> | (not sure i'd conclude that from that alone. as opposed to singleton stuff, say. or `reflection') |
| 23:07:12 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 23:09:51 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 23:11:23 | <monochrom> | Ah but singleton and reflection are currently libraries instead of language extensions :) |
| 23:13:03 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 23:14:42 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 268 seconds) |
| 23:16:25 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
| 23:17:10 | → | beka joins (~beka@2607:f598:bd4a:80:30ba:2fe6:f77e:af55) |
| 23:19:01 | beka | is now known as augur |
| 23:19:23 | augur | is now known as beka |
| 23:20:00 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 23:21:55 | × | acidjnk quits (~acidjnk@p200300d6e714dc20691c30fd92f896ed.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 23:22:34 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 23:26:19 | × | qqq quits (~qqq@92.43.167.61) (Remote host closed the connection) |
| 23:30:24 | sprout_ | is now known as sprout |
| 23:37:05 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 23:38:27 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 23:40:53 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 23:49:28 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) |
| 23:52:28 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:2bf1:bd3e:81f0:ed26) (Read error: Connection reset by peer) |
| 23:53:22 | × | caubert quits (~caubert@user/caubert) (Quit: WeeChat 4.0.4) |
| 23:55:53 | → | caubert joins (~caubert@user/caubert) |
| 23:56:56 | × | caubert quits (~caubert@user/caubert) (Client Quit) |
| 23:57:06 | → | caubert joins (~caubert@user/caubert) |
| 23:58:13 | × | phma quits (phma@2001:5b0:210d:72b8:fcdc:5db1:5990:c6e2) (Read error: Connection reset by peer) |
| 23:59:19 | → | phma joins (phma@2001:5b0:211f:3948:fcc0:5fe2:5111:f5f6) |
All times are in UTC on 2024-04-16.