Logs: liberachat/#haskell
| 2025-08-14 10:10:59 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 10:13:09 | trickard_ | is now known as trickard |
| 2025-08-14 10:14:10 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 2025-08-14 10:16:14 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2025-08-14 10:17:46 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 255 seconds) |
| 2025-08-14 10:23:57 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 240 seconds) |
| 2025-08-14 10:25:33 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2025-08-14 10:27:02 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-08-14 10:29:43 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-08-14 10:30:02 | × | juri_ quits (~juri@implicitcad.org) (Ping timeout: 252 seconds) |
| 2025-08-14 10:30:55 | × | dutchie quits (~dutchie@user/dutchie) (Server closed connection) |
| 2025-08-14 10:31:09 | → | dutchie joins (~dutchie@user/dutchie) |
| 2025-08-14 10:32:17 | → | haritz joins (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2025-08-14 10:32:17 | × | haritz quits (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2025-08-14 10:32:17 | → | haritz joins (~hrtz@user/haritz) |
| 2025-08-14 10:34:08 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 245 seconds) |
| 2025-08-14 10:42:07 | → | juri_ joins (~juri@implicitcad.org) |
| 2025-08-14 10:42:21 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-08-14 10:44:01 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-08-14 10:45:50 | → | fp joins (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) |
| 2025-08-14 10:47:04 | → | poscat joins (~poscat@user/poscat) |
| 2025-08-14 10:54:46 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Read error: Connection reset by peer) |
| 2025-08-14 10:56:37 | × | jackdk quits (uid373013@cssa/life/jackdk) (Quit: Connection closed for inactivity) |
| 2025-08-14 11:00:05 | × | caconym747 quits (~caconym@user/caconym) (Quit: bye) |
| 2025-08-14 11:02:09 | → | caconym747 joins (~caconym@user/caconym) |
| 2025-08-14 11:15:02 | × | jreicher quits (~user@user/jreicher) (Quit: In transit) |
| 2025-08-14 11:20:46 | × | trickard quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Ping timeout: 255 seconds) |
| 2025-08-14 11:21:09 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 11:24:06 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-08-14 11:24:13 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2025-08-14 11:24:40 | → | xff0x joins (~xff0x@2405:6580:b080:900:86d4:8706:5c5f:d5c) |
| 2025-08-14 11:25:30 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2025-08-14 11:32:31 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2025-08-14 11:33:36 | → | davidlbowman joins (~dlb@user/davidlbowman) |
| 2025-08-14 11:41:53 | → | jreicher joins (~user@user/jreicher) |
| 2025-08-14 11:54:44 | → | dhil joins (~dhil@5.151.29.141) |
| 2025-08-14 11:57:47 | trickard_ | is now known as trickard |
| 2025-08-14 12:00:38 | × | trickard quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 12:00:52 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 12:06:00 | × | trickard_ quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 12:07:23 | × | fp quits (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) (Quit: fp) |
| 2025-08-14 12:10:27 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-08-14 12:11:42 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 12:18:33 | → | fp joins (~Thunderbi@2001:708:150:10::72df) |
| 2025-08-14 12:20:17 | × | lisq quits (~quassel@lis.moe) (Server closed connection) |
| 2025-08-14 12:20:26 | → | lisq joins (~quassel@lis.moe) |
| 2025-08-14 12:21:29 | × | fp quits (~Thunderbi@2001:708:150:10::72df) (Remote host closed the connection) |
| 2025-08-14 12:22:15 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 2025-08-14 12:23:55 | → | Miroboru joins (~myrvoll@46.249.255.58) |
| 2025-08-14 12:29:15 | trickard_ | is now known as trickard |
| 2025-08-14 12:32:04 | × | tromp quits (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 12:32:31 | → | fp joins (~Thunderbi@2001:708:150:10::72df) |
| 2025-08-14 12:42:10 | → | Square2 joins (~Square@user/square) |
| 2025-08-14 12:44:35 | → | tromp joins (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 12:45:44 | × | troydm quits (~troydm@user/troydm) (Server closed connection) |
| 2025-08-14 12:46:06 | → | troydm joins (~troydm@user/troydm) |
| 2025-08-14 12:50:27 | × | trickard quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 12:50:42 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 13:04:22 | × | trickard_ quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 13:04:35 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 13:08:15 | × | ruvam quits (~ruvam@user/ruvam) (Server closed connection) |
| 2025-08-14 13:08:30 | → | ruvam joins (~ruvam@user/ruvam) |
| 2025-08-14 13:12:19 | × | raym quits (~ray@user/raym) (Ping timeout: 260 seconds) |
| 2025-08-14 13:14:00 | × | AlexZenon quits (~alzenon@178.34.150.240) (Ping timeout: 252 seconds) |
| 2025-08-14 13:17:56 | × | trickard_ quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 13:17:59 | × | yo quits (~yo@178.42.38.149.ipv4.supernova.orange.pl) (Quit: Leaving.) |
| 2025-08-14 13:19:40 | → | Square joins (~Square4@user/square) |
| 2025-08-14 13:22:12 | → | AlexZenon joins (~alzenon@178.34.150.240) |
| 2025-08-14 13:22:58 | × | Square2 quits (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-08-14 13:27:33 | × | qqe quits (~qqq@185.54.20.59) (Server closed connection) |
| 2025-08-14 13:27:53 | → | qqe joins (~qqq@185.54.20.59) |
| 2025-08-14 13:30:29 | × | AlexZenon quits (~alzenon@178.34.150.240) (Ping timeout: 248 seconds) |
| 2025-08-14 13:30:51 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 13:35:19 | × | trickard_ quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Ping timeout: 255 seconds) |
| 2025-08-14 13:44:41 | → | AlexZenon joins (~alzenon@178.34.150.240) |
| 2025-08-14 13:47:38 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 13:52:38 | → | weary-traveler joins (~user@user/user363627) |
| 2025-08-14 13:53:14 | × | AlexZenon quits (~alzenon@178.34.150.240) (Ping timeout: 272 seconds) |
| 2025-08-14 14:05:34 | → | AlexZenon joins (~alzenon@178.34.150.240) |
| 2025-08-14 14:09:04 | × | yangby quits (~secret@115.205.231.82) (Ping timeout: 260 seconds) |
| 2025-08-14 14:13:11 | <yin> | is exhaustiveness in haskell decideable? |
| 2025-08-14 14:13:32 | <ncf> | yin: what do you mean by exhaustiveness? |
| 2025-08-14 14:15:25 | <yin> | checking exhaustive case handling in pattern matches |
| 2025-08-14 14:17:37 | <ncf> | presumably no if you include guards or view patterns, and yes otherwise |
| 2025-08-14 14:20:37 | × | AlexZenon quits (~alzenon@178.34.150.240) (Ping timeout: 248 seconds) |
| 2025-08-14 14:24:37 | <int-e> | GADTs (or even just existentials) add complications too (a constraint embedded in a constructor may be unsatisfiable) |
| 2025-08-14 14:25:40 | × | michalz quits (~michalz@185.246.207.221) (Remote host closed the connection) |
| 2025-08-14 14:28:33 | <ncf> | i guess this is agda's "i'm not sure if there should be a case for the constructor..." error message |
| 2025-08-14 14:28:57 | <ncf> | are existentials really problematic already? i don't immediately see how they could lead to undecidable unification problems |
| 2025-08-14 14:30:05 | → | AlexZenon joins (~alzenon@178.34.150.240) |
| 2025-08-14 14:31:29 | <int-e> | data Eq a b where CEq :: a ~ b => Eq gives you an arbitrary unification problem depending on what a and b are when matching CEq, no? |
| 2025-08-14 14:32:48 | <int-e> | You may still be right... |
| 2025-08-14 14:33:07 | <ncf> | oh yeah i'm just not sure i would call that an existential |
| 2025-08-14 14:34:25 | <ncf> | like the source of undecidability here is the equality constraint |
| 2025-08-14 14:35:04 | <ncf> | (which i guess is the quintessential GADT) |
| 2025-08-14 14:38:23 | <int-e> | Yeah I guess if all your constraints are ordinary typeclasses then the open nature of those saves you from having to unify anything... |
| 2025-08-14 14:38:26 | <int-e> | tricky |
| 2025-08-14 14:45:35 | → | ft joins (~ft@p508dba54.dip0.t-ipconnect.de) |
| 2025-08-14 14:46:38 | × | AlexZenon quits (~alzenon@178.34.150.240) (Ping timeout: 245 seconds) |
| 2025-08-14 14:48:10 | × | trickard_ quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Ping timeout: 252 seconds) |
All times are in UTC.