| 2025-08-14 00:09:15 +0200 | Igloo | (~ian@81.2.99.210) (Ping timeout: 252 seconds) |
| 2025-08-14 00:09:48 +0200 | Lycurgus | (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2025-08-14 00:10:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 00:11:17 +0200 | Igloo | (~ian@45.130.105.70) Igfoo |
| 2025-08-14 00:16:49 +0200 | Igloo | (~ian@45.130.105.70) (Ping timeout: 248 seconds) |
| 2025-08-14 00:17:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-14 00:17:36 +0200 | Igloo | (~ian@81.2.99.210) |
| 2025-08-14 00:24:53 +0200 | batbyte | (~batbyte@172-79-46-231.nrwc.ny.frontiernet.net) |
| 2025-08-14 00:25:57 +0200 | Igloo | (~ian@81.2.99.210) (Ping timeout: 260 seconds) |
| 2025-08-14 00:26:44 +0200 | rvalue | (~rvalue@about/hackers/rvalue) (Remote host closed the connection) |
| 2025-08-14 00:27:09 +0200 | pera | (~pera@user/pera) (Quit: leaving) |
| 2025-08-14 00:27:10 +0200 | rvalue | (~rvalue@about/hackers/rvalue) rvalue |
| 2025-08-14 00:27:53 +0200 | Igloo | (~ian@45.130.105.70) Igfoo |
| 2025-08-14 00:28:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 00:33:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 00:34:08 +0200 | Igloo | (~ian@45.130.105.70) (Ping timeout: 245 seconds) |
| 2025-08-14 00:36:16 +0200 | Igloo | (~ian@81.2.99.210) Igfoo |
| 2025-08-14 00:38:17 +0200 | davidlbowman | (~dlb@user/davidlbowman) davidlbowman |
| 2025-08-14 00:40:38 +0200 | rvalue- | (~rvalue@about/hackers/rvalue) rvalue |
| 2025-08-14 00:41:32 +0200 | rvalue | (~rvalue@about/hackers/rvalue) (Read error: Connection reset by peer) |
| 2025-08-14 00:44:58 +0200 | jreicher | (~user@user/jreicher) jreicher |
| 2025-08-14 00:47:40 +0200 | rvalue- | rvalue |
| 2025-08-14 00:51:54 +0200 | batbyte_ | (~batbyte@52.sub-174-215-208.myvzw.com) |
| 2025-08-14 00:56:17 +0200 | batbyte | (~batbyte@172-79-46-231.nrwc.ny.frontiernet.net) (Ping timeout: 260 seconds) |
| 2025-08-14 01:03:09 +0200 | batbyte_ | (~batbyte@52.sub-174-215-208.myvzw.com) (Read error: Connection reset by peer) |
| 2025-08-14 01:05:55 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Ping timeout: 255 seconds) |
| 2025-08-14 01:06:03 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-08-14 01:08:49 +0200 | yangby | (~secret@115.205.231.82) yangby |
| 2025-08-14 01:13:01 +0200 | DragonMaus | (~dragonmau@user/dragonmaus) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2025-08-14 01:13:51 +0200 | DragonMaus | (~dragonmau@user/dragonmaus) DragonMaus |
| 2025-08-14 01:19:48 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-08-14 01:23:45 +0200 | weary-traveler | (~user@user/user363627) (Client Quit) |
| 2025-08-14 01:24:07 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-08-14 01:34:33 +0200 | davidlbowman | (~dlb@user/davidlbowman) (Quit: WeeChat 4.1.1) |
| 2025-08-14 01:46:19 +0200 | user363627 | (~user@user/user363627) user363627 |
| 2025-08-14 01:48:21 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 2025-08-14 01:48:34 +0200 | davidlbowman | (~dlb@user/davidlbowman) davidlbowman |
| 2025-08-14 01:49:41 +0200 | weary-traveler | (~user@user/user363627) (Ping timeout: 248 seconds) |
| 2025-08-14 01:52:27 +0200 | sprotte24 | (~sprotte24@p200300d16f078c0059c6348cdb3f9f36.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-08-14 01:56:17 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 240 seconds) |
| 2025-08-14 01:57:14 +0200 | acidjnk | (~acidjnk@p200300d6e7171939495adaceecd6b03f.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-08-14 01:57:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 01:57:38 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-08-14 02:00:56 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection) |
| 2025-08-14 02:01:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 02:03:52 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-08-14 02:12:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 02:20:46 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2025-08-14 02:21:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 02:21:38 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-08-14 02:22:37 +0200 | xff0x | (~xff0x@2405:6580:b080:900:c488:ca49:9294:78c2) (Ping timeout: 260 seconds) |
| 2025-08-14 02:24:55 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Client Quit) |
| 2025-08-14 02:32:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 02:33:21 +0200 | yo | (~yo@178.42.40.158.ipv4.supernova.orange.pl) (Ping timeout: 252 seconds) |
| 2025-08-14 02:34:44 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-08-14 02:35:27 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 260 seconds) |
| 2025-08-14 02:37:49 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2025-08-14 02:37:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-08-14 02:38:11 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-08-14 02:38:35 +0200 | batbyte_ | (~batbyte@172-79-46-231.nrwc.ny.frontiernet.net) |
| 2025-08-14 02:42:57 +0200 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) werneta |
| 2025-08-14 02:48:05 +0200 | yo | (~yo@178.42.38.149.ipv4.supernova.orange.pl) ayu |
| 2025-08-14 02:48:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 02:52:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 03:03:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 03:08:39 +0200 | user363627 | (~user@user/user363627) (Remote host closed the connection) |
| 2025-08-14 03:09:40 +0200 | batbyte_ | (~batbyte@172-79-46-231.nrwc.ny.frontiernet.net) (Read error: Connection reset by peer) |
| 2025-08-14 03:10:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-14 03:21:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 03:21:55 +0200 | jackdk | (uid373013@cssa/life/jackdk) jackdk |
| 2025-08-14 03:24:57 +0200 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2025-08-14 03:26:10 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-08-14 03:26:46 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-08-14 03:32:19 +0200 | ft | (~ft@p508dbd8e.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2025-08-14 03:33:04 +0200 | sixteenrats | (~emelia@user/sixteenrats) (Quit: WeeChat 4.7.0) |
| 2025-08-14 03:34:56 +0200 | arandombit | (~arandombi@2603:7000:4600:ffbe:a130:33a0:f4b6:f889) |
| 2025-08-14 03:34:56 +0200 | arandombit | (~arandombi@2603:7000:4600:ffbe:a130:33a0:f4b6:f889) (Changing host) |
| 2025-08-14 03:34:56 +0200 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2025-08-14 03:36:58 +0200 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-08-14 03:37:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 03:39:37 +0200 | ystael | (~ystael@user/ystael) ystael |
| 2025-08-14 03:41:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-08-14 03:42:04 +0200 | <haskellbridge> | <Axman6> Has there ever been a proposal for an alternative to "fromInteger" which also accepts the input as a Nat? Something like "fromInteger' :: Num a => Proxy (n :: Nat) -> Integer -> a" (though I guess it also needs a sign, but ignoring that). GHC warns for overflowed literals for types like Word8, but it's not really accessible to mere mortals right? |
| 2025-08-14 03:47:12 +0200 | <EvanR> | greetings Axman6, may the grass be greener on the other side of the bridge |
| 2025-08-14 03:47:52 +0200 | <EvanR> | why does your fromInteger have 2 numeric inputs |
| 2025-08-14 03:48:45 +0200 | <haskellbridge> | <Axman6> Hmm, that's a point. I guess it could be something like "fromInteger' :: Num a => Proxy (Bool,n :: Nat) -> a" |
| 2025-08-14 03:52:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 03:53:37 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 2025-08-14 03:54:12 +0200 | ft | (~ft@p508dba54.dip0.t-ipconnect.de) ft |
| 2025-08-14 03:56:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 03:58:29 +0200 | <Leary> | You can write `data SomeInt = Neg SomeNat | Pos SomeNat; instance Num SomeInt where { ... }`. |
| 2025-08-14 03:59:11 +0200 | Wanderer | (~wanderer@user/wanderer) (Server closed connection) |
| 2025-08-14 03:59:15 +0200 | phma | (~phma@host-67-44-208-71.hnremote.net) (Read error: Connection reset by peer) |
| 2025-08-14 04:00:00 +0200 | Wanderer | (~wanderer@user/wanderer) Wanderer |
| 2025-08-14 04:00:04 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 255 seconds) |
| 2025-08-14 04:02:12 +0200 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 2025-08-14 04:02:50 +0200 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2025-08-14 04:07:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 04:09:57 +0200 | davidlbowman | (~dlb@user/davidlbowman) (Ping timeout: 260 seconds) |
| 2025-08-14 04:11:07 +0200 | td_ | (~td@i5387090d.versanet.de) (Ping timeout: 260 seconds) |
| 2025-08-14 04:12:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 04:13:00 +0200 | td_ | (~td@i53870938.versanet.de) |
| 2025-08-14 04:22:41 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 2025-08-14 04:23:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 04:24:32 +0200 | sprout | (~sprout@2a02-a448-3a80-0-c61c-b515-5509-58e7.fixed6.kpn.net) sprout |
| 2025-08-14 04:26:25 +0200 | down200 | (~down200@shell.lug.mtu.edu) (Ping timeout: 248 seconds) |
| 2025-08-14 04:28:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 04:28:09 +0200 | down200 | (~down200@shell.lug.mtu.edu) down200 |
| 2025-08-14 04:38:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 04:45:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 04:49:52 +0200 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2025-08-14 04:53:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 04:57:50 +0200 | arandombit | (~arandombi@user/arandombit) (Remote host closed the connection) |
| 2025-08-14 04:58:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 05:01:36 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-08-14 05:02:06 +0200 | weary-traveler | (~user@user/user363627) (Client Quit) |
| 2025-08-14 05:02:22 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-08-14 05:03:31 +0200 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 2025-08-14 05:04:33 +0200 | phma | (~phma@2001:5b0:210b:ad88:aa04:c457:74b0:5887) |
| 2025-08-14 05:09:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 05:09:33 +0200 | phma_ | (phma@2001:5b0:211f:2bc8:578f:fe26:99a2:5bbd) |
| 2025-08-14 05:10:06 +0200 | phma | (~phma@2001:5b0:210b:ad88:aa04:c457:74b0:5887) (Read error: Connection reset by peer) |
| 2025-08-14 05:13:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-14 05:14:34 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2025-08-14 05:15:48 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-08-14 05:16:29 +0200 | aforemny_ | (~aforemny@2001:9e8:6ce8:1800:d6a7:aaeb:8c84:6bc7) aforemny |
| 2025-08-14 05:17:00 +0200 | aforemny | (~aforemny@i59F4C4EA.versanet.de) (Ping timeout: 252 seconds) |
| 2025-08-14 05:19:09 +0200 | Square2 | (~Square@user/square) Square |
| 2025-08-14 05:19:58 +0200 | phma_ | (phma@2001:5b0:211f:2bc8:578f:fe26:99a2:5bbd) (Read error: Connection reset by peer) |
| 2025-08-14 05:21:28 +0200 | phma_ | (phma@2001:5b0:211b:d038:6b7f:3fe1:de35:dfff) |
| 2025-08-14 05:22:52 +0200 | Square | (~Square4@user/square) (Ping timeout: 252 seconds) |
| 2025-08-14 05:24:35 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 05:25:39 +0200 | phma_ | (phma@2001:5b0:211b:d038:6b7f:3fe1:de35:dfff) (Read error: Connection reset by peer) |
| 2025-08-14 05:29:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 05:33:35 +0200 | phma_ | (~phma@host-67-44-208-76.hnremote.net) |
| 2025-08-14 05:35:58 +0200 | ycp | (~znc@user/dragestil) (Server closed connection) |
| 2025-08-14 05:36:19 +0200 | ycp | (~znc@user/dragestil) dragestil |
| 2025-08-14 05:40:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 05:44:30 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 05:46:56 +0200 | phma_ | (~phma@host-67-44-208-76.hnremote.net) (Read error: Connection reset by peer) |
| 2025-08-14 05:52:03 +0200 | feetwind | (~mike@user/feetwind) (Server closed connection) |
| 2025-08-14 05:52:21 +0200 | feetwind | (~mike@user/feetwind) feetwind |
| 2025-08-14 05:55:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 05:59:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-08-14 06:04:58 +0200 | Square2 | (~Square@user/square) (Ping timeout: 245 seconds) |
| 2025-08-14 06:06:08 +0200 | Lycurgus | (~juan@user/Lycurgus) (Ping timeout: 252 seconds) |
| 2025-08-14 06:10:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 06:15:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 06:18:50 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 06:19:03 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 06:24:30 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 06:26:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 06:29:12 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 06:33:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 06:40:09 +0200 | haritz | (~hrtz@user/haritz) (Remote host closed the connection) |
| 2025-08-14 06:41:36 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 272 seconds) |
| 2025-08-14 06:44:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 06:48:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 06:53:46 +0200 | <haskellbridge> | <Axman6> Leary The idea was to be able to support types whose valid values are limited, in this particular case the "Index (n :: Nat)" type in Clash, which represents values [0..n-1] |
| 2025-08-14 06:54:17 +0200 | <haskellbridge> | <Axman6> so writing "32 :: Index 32" should fail at compile time/GHCi |
| 2025-08-14 06:54:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 06:54:43 +0200 | <haskellbridge> | <Axman6> I'm wondering if it's possible to make writing "32 :: Index 32" a type error |
| 2025-08-14 06:55:46 +0200 | phma_ | (~phma@2001:5b0:2172:ba18:237a:adb:9a49:b97a) |
| 2025-08-14 06:55:52 +0200 | phma_ | phma |
| 2025-08-14 06:57:53 +0200 | jespada | (~jespada@2800:a4:2247:2400:386f:f20:8fc5:23de) (Ping timeout: 248 seconds) |
| 2025-08-14 06:58:53 +0200 | michalz | (~michalz@185.246.207.218) |
| 2025-08-14 06:59:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 06:59:39 +0200 | <Leary> | Perhaps you can write something like `instance n < 32 => Num (Index n)`, then `fromInteger @(Index _) :: n < 32 => Int -> Index n`. |
| 2025-08-14 06:59:48 +0200 | <Leary> | Otherwise, there's validated-literals. |
| 2025-08-14 07:00:27 +0200 | jespada | (~jespada@2800:a4:2225:9000:913:54f8:4fc8:5494) jespada |
| 2025-08-14 07:00:28 +0200 | <Leary> | Integer* |
| 2025-08-14 07:02:58 +0200 | <Leary> | Err, ignore that first suggestion, I had a thinko. |
| 2025-08-14 07:03:44 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-08-14 07:05:16 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Quit: You) |
| 2025-08-14 07:07:55 +0200 | trickard_ | trickard |
| 2025-08-14 07:08:42 +0200 | finsternis | (~X@23.226.237.192) finsternis |
| 2025-08-14 07:10:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 07:14:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 07:15:27 +0200 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 2025-08-14 07:24:06 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-08-14 07:25:12 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 07:25:25 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 07:25:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 07:30:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 07:40:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 07:45:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 07:55:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 07:56:55 +0200 | smalltalkman | (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-08-14 07:59:55 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-08-14 08:00:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 08:11:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 08:17:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 08:28:55 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2025-08-14 08:29:10 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 08:33:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-14 08:38:53 +0200 | Katarushisu | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Read error: Connection reset by peer) |
| 2025-08-14 08:40:04 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-08-14 08:40:32 +0200 | trickard_ | trickard |
| 2025-08-14 08:40:47 +0200 | Katarushisu | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) Katarushisu |
| 2025-08-14 08:41:21 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2025-08-14 08:42:32 +0200 | whereiseveryone | (206ba86c98@2a03:6000:1812:100::2e4) (Server closed connection) |
| 2025-08-14 08:42:41 +0200 | whereiseveryone | (206ba86c98@2a03:6000:1812:100::2e4) whereiseveryone |
| 2025-08-14 08:44:04 +0200 | smalltalkman | (uid545680@id-545680.hampstead.irccloud.com) smalltalkman |
| 2025-08-14 08:44:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 08:48:03 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-08-14 08:48:36 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-08-14 08:48:42 +0200 | ft | (~ft@p508dba54.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-08-14 08:48:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 08:50:48 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
| 2025-08-14 08:54:37 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 260 seconds) |
| 2025-08-14 08:56:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 09:00:04 +0200 | caconym747 | (~caconym@user/caconym) (Quit: bye) |
| 2025-08-14 09:00:45 +0200 | caconym747 | (~caconym@user/caconym) caconym |
| 2025-08-14 09:01:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 09:02:24 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 09:03:23 +0200 | takuan | (~takuan@d8d86b9e9.access.telenet.be) |
| 2025-08-14 09:05:41 +0200 | jreicher | (~user@user/jreicher) (Quit: In transit) |
| 2025-08-14 09:06:28 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-08-14 09:06:37 +0200 | acidjnk | (~acidjnk@p200300d6e7171985495adaceecd6b03f.dip0.t-ipconnect.de) acidjnk |
| 2025-08-14 09:07:48 +0200 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2025-08-14 09:09:09 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-08-14 09:11:32 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-08-14 09:12:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-14 09:16:30 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 09:22:09 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-08-14 09:35:58 +0200 | jreicher | (~user@user/jreicher) jreicher |
| 2025-08-14 09:39:18 +0200 | <haskellbridge> | <Axman6> Yeah, that's kind of the opposite of what I want. I want "instance (n' < n) => Num' (Index n) where fromInteger' :: Proxy n' -> Index n" - I want to pass in the literal the user has written, so "40 :: Index 32" means "fromInteger' (Proxy @40) :: Index 32" which would fail to compile because there's no instance for "40 < 32 => Num' (Index 32)" |
| 2025-08-14 09:42:15 +0200 | jreicher | (~user@user/jreicher) (Ping timeout: 244 seconds) |
| 2025-08-14 09:44:05 +0200 | jreicher | (~user@user/jreicher) jreicher |
| 2025-08-14 09:46:27 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 09:46:48 +0200 | fp | (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) fp |
| 2025-08-14 10:01:42 +0200 | chele | (~chele@user/chele) chele |
| 2025-08-14 10:02:43 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-08-14 10:11:03 +0200 | DragonMaus | (~dragonmau@user/dragonmaus) (Ping timeout: 252 seconds) |
| 2025-08-14 10:11:35 +0200 | DragonMaus | (~dragonmau@user/dragonmaus) DragonMaus |
| 2025-08-14 10:20:23 +0200 | fizbin | (~fizbin@user/fizbin) fizbin |
| 2025-08-14 10:24:44 +0200 | ol0ck | (~quassel@user/ol0ck) (Ping timeout: 260 seconds) |
| 2025-08-14 10:27:57 +0200 | fizbin | (~fizbin@user/fizbin) (Ping timeout: 276 seconds) |
| 2025-08-14 10:28:41 +0200 | j0lol | (~j0lol@132.145.17.236) (Server closed connection) |
| 2025-08-14 10:28:55 +0200 | j0lol | (~j0lol@132.145.17.236) j0lol |
| 2025-08-14 10:51:20 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 11:07:02 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 11:07:16 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 11:09:17 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 11:27:10 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-08-14 11:29:39 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-08-14 11:30:53 +0200 | michalz | (~michalz@185.246.207.218) (Remote host closed the connection) |
| 2025-08-14 11:30:58 +0200 | Miroboru | (~myrvoll@84.215.249.36) (Ping timeout: 255 seconds) |
| 2025-08-14 11:33:28 +0200 | michalz | (~michalz@185.246.207.221) |
| 2025-08-14 11:34:20 +0200 | Miroboru | (~myrvoll@84.215.249.36) Miroboru |
| 2025-08-14 11:35:02 +0200 | fp | (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) (Ping timeout: 260 seconds) |
| 2025-08-14 11:42:00 +0200 | Miroboru | (~myrvoll@84.215.249.36) (Ping timeout: 252 seconds) |
| 2025-08-14 11:43:07 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 255 seconds) |
| 2025-08-14 11:45:06 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-08-14 11:52:02 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 11:57:46 +0200 | tremon | (~tremon@83.80.159.219) tremon |
| 2025-08-14 12:03:18 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 12:10:46 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 12:10:59 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 12:13:09 +0200 | trickard_ | trickard |
| 2025-08-14 12:14:10 +0200 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2025-08-14 12:16:14 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-08-14 12:17:46 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 255 seconds) |
| 2025-08-14 12:23:57 +0200 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 240 seconds) |
| 2025-08-14 12:25:33 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-08-14 12:27:02 +0200 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2025-08-14 12:29:43 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-08-14 12:30:02 +0200 | juri_ | (~juri@implicitcad.org) (Ping timeout: 252 seconds) |
| 2025-08-14 12:30:55 +0200 | dutchie | (~dutchie@user/dutchie) (Server closed connection) |
| 2025-08-14 12:31:09 +0200 | dutchie | (~dutchie@user/dutchie) dutchie |
| 2025-08-14 12:32:17 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2025-08-14 12:32:17 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2025-08-14 12:32:17 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-08-14 12:34:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 245 seconds) |
| 2025-08-14 12:42:07 +0200 | juri_ | (~juri@implicitcad.org) juri_ |
| 2025-08-14 12:42:21 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-08-14 12:44:01 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-08-14 12:45:50 +0200 | fp | (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) fp |
| 2025-08-14 12:47:04 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-08-14 12:54:46 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Read error: Connection reset by peer) |
| 2025-08-14 12:56:37 +0200 | jackdk | (uid373013@cssa/life/jackdk) (Quit: Connection closed for inactivity) |
| 2025-08-14 13:00:05 +0200 | caconym747 | (~caconym@user/caconym) (Quit: bye) |
| 2025-08-14 13:02:09 +0200 | caconym747 | (~caconym@user/caconym) caconym |
| 2025-08-14 13:15:02 +0200 | jreicher | (~user@user/jreicher) (Quit: In transit) |
| 2025-08-14 13:20:46 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) (Ping timeout: 255 seconds) |
| 2025-08-14 13:21:09 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 13:24:06 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-08-14 13:24:13 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-08-14 13:24:40 +0200 | xff0x | (~xff0x@2405:6580:b080:900:86d4:8706:5c5f:d5c) |
| 2025-08-14 13:25:30 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-08-14 13:32:31 +0200 | Lycurgus | (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2025-08-14 13:33:36 +0200 | davidlbowman | (~dlb@user/davidlbowman) davidlbowman |
| 2025-08-14 13:41:53 +0200 | jreicher | (~user@user/jreicher) jreicher |
| 2025-08-14 13:54:44 +0200 | dhil | (~dhil@5.151.29.141) dhil |
| 2025-08-14 13:57:47 +0200 | trickard_ | trickard |
| 2025-08-14 14:00:38 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 14:00:52 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 14:06:00 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 14:07:23 +0200 | fp | (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) (Quit: fp) |
| 2025-08-14 14:10:27 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-08-14 14:11:42 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 14:18:33 +0200 | fp | (~Thunderbi@2001:708:150:10::72df) fp |
| 2025-08-14 14:20:17 +0200 | lisq | (~quassel@lis.moe) (Server closed connection) |
| 2025-08-14 14:20:26 +0200 | lisq | (~quassel@lis.moe) lisq |
| 2025-08-14 14:21:29 +0200 | fp | (~Thunderbi@2001:708:150:10::72df) (Remote host closed the connection) |
| 2025-08-14 14:22:15 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-08-14 14:23:55 +0200 | Miroboru | (~myrvoll@46.249.255.58) Miroboru |
| 2025-08-14 14:29:15 +0200 | trickard_ | trickard |
| 2025-08-14 14:32:04 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 14:32:31 +0200 | fp | (~Thunderbi@2001:708:150:10::72df) fp |
| 2025-08-14 14:42:10 +0200 | Square2 | (~Square@user/square) Square |
| 2025-08-14 14:44:35 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 14:45:44 +0200 | troydm | (~troydm@user/troydm) (Server closed connection) |
| 2025-08-14 14:46:06 +0200 | troydm | (~troydm@user/troydm) troydm |
| 2025-08-14 14:50:27 +0200 | trickard | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 14:50:42 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 15:04:22 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 15:04:35 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 15:08:15 +0200 | ruvam | (~ruvam@user/ruvam) (Server closed connection) |
| 2025-08-14 15:08:30 +0200 | ruvam | (~ruvam@user/ruvam) ruvam |
| 2025-08-14 15:12:19 +0200 | raym | (~ray@user/raym) (Ping timeout: 260 seconds) |
| 2025-08-14 15:14:00 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 252 seconds) |
| 2025-08-14 15:17:56 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 15:17:59 +0200 | yo | (~yo@178.42.38.149.ipv4.supernova.orange.pl) (Quit: Leaving.) |
| 2025-08-14 15:19:40 +0200 | Square | (~Square4@user/square) Square |
| 2025-08-14 15:22:12 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 15:22:58 +0200 | Square2 | (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-08-14 15:27:33 +0200 | qqe | (~qqq@185.54.20.59) (Server closed connection) |
| 2025-08-14 15:27:53 +0200 | qqe | (~qqq@185.54.20.59) |
| 2025-08-14 15:30:29 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 248 seconds) |
| 2025-08-14 15:30:51 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 15:35:19 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Ping timeout: 255 seconds) |
| 2025-08-14 15:44:41 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 15:47:38 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 15:52:38 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-08-14 15:53:14 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 272 seconds) |
| 2025-08-14 16:05:34 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 16:09:04 +0200 | yangby | (~secret@115.205.231.82) (Ping timeout: 260 seconds) |
| 2025-08-14 16:13:11 +0200 | <yin> | is exhaustiveness in haskell decideable? |
| 2025-08-14 16:13:32 +0200 | <ncf> | yin: what do you mean by exhaustiveness? |
| 2025-08-14 16:15:25 +0200 | <yin> | checking exhaustive case handling in pattern matches |
| 2025-08-14 16:17:37 +0200 | <ncf> | presumably no if you include guards or view patterns, and yes otherwise |
| 2025-08-14 16:20:37 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 248 seconds) |
| 2025-08-14 16:24:37 +0200 | <int-e> | GADTs (or even just existentials) add complications too (a constraint embedded in a constructor may be unsatisfiable) |
| 2025-08-14 16:25:40 +0200 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
| 2025-08-14 16:28:33 +0200 | <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 16:28:57 +0200 | <ncf> | are existentials really problematic already? i don't immediately see how they could lead to undecidable unification problems |
| 2025-08-14 16:30:05 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 16:31:29 +0200 | <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 16:32:48 +0200 | <int-e> | You may still be right... |
| 2025-08-14 16:33:07 +0200 | <ncf> | oh yeah i'm just not sure i would call that an existential |
| 2025-08-14 16:34:25 +0200 | <ncf> | like the source of undecidability here is the equality constraint |
| 2025-08-14 16:35:04 +0200 | <ncf> | (which i guess is the quintessential GADT) |
| 2025-08-14 16:38:23 +0200 | <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 16:38:26 +0200 | <int-e> | tricky |
| 2025-08-14 16:45:35 +0200 | ft | (~ft@p508dba54.dip0.t-ipconnect.de) ft |
| 2025-08-14 16:46:38 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 245 seconds) |
| 2025-08-14 16:48:10 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Ping timeout: 252 seconds) |
| 2025-08-14 16:48:34 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 16:51:08 +0200 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2025-08-14 16:51:42 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 16:52:31 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-08-14 16:55:52 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 2025-08-14 16:58:38 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 17:02:41 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 17:02:55 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-08-14 17:10:18 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 17:11:08 +0200 | fp | (~Thunderbi@2001:708:150:10::72df) (Ping timeout: 272 seconds) |
| 2025-08-14 17:17:44 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 260 seconds) |
| 2025-08-14 17:18:37 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 260 seconds) |
| 2025-08-14 17:18:37 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-08-14 17:18:49 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 2025-08-14 17:20:38 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 17:24:07 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Quit: You) |
| 2025-08-14 17:24:42 +0200 | ashkan81 | (~ashkan81@147.161.173.107) |
| 2025-08-14 17:25:20 +0200 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2025-08-14 17:25:32 +0200 | <ashkan81> | Hello everyone. Shouldn't this be impossible : `instance (MonadReader a m, MonadReader b m) => ... ` due to `m -> r` in `MonadReader` ? |
| 2025-08-14 17:26:25 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-08-14 17:26:58 +0200 | <ashkan81> | Looks like my ghc-9.6.7 is more than happy to compile this (to me) impossible constraint and even run the code. I'm wondering what am I missing here ... |
| 2025-08-14 17:26:58 +0200 | jbalint_ | (~jbalint@syn-071-090-116-115.res.spectrum.com) (Ping timeout: 240 seconds) |
| 2025-08-14 17:27:14 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 17:27:28 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 17:30:49 +0200 | jbalint | (~jbalint@2600:6c44:117f:e98a:40bb:52ad:62b8:5122) |
| 2025-08-14 17:30:50 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 17:31:52 +0200 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2025-08-14 17:31:53 +0200 | <ashkan81> | Actually got my answer from Claude: in case `a ~ b` this can be satisfied so ghc compiles this but if you actually try to call it (I haven't yet) in a way that can't satisfy the constraint, then it complains. Makes sense +1 |
| 2025-08-14 17:33:13 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 17:36:38 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 2025-08-14 17:39:02 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 260 seconds) |
| 2025-08-14 17:40:15 +0200 | <ncf> | another way to say this is that the constraint is equivalent to (MonadReader a m, a ~ b) |
| 2025-08-14 17:42:29 +0200 | trickard__ | (~trickard@cpe-88-98-47-163.wireline.com.au) |
| 2025-08-14 17:43:34 +0200 | trickard_ | (~trickard@cpe-86-98-47-163.wireline.com.au) (Ping timeout: 255 seconds) |
| 2025-08-14 17:49:38 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 17:50:33 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-08-14 17:54:01 +0200 | <dolio> | I don't know if things have changed in this regard, but it used to be the case that they would not work quite the same. |
| 2025-08-14 17:54:53 +0200 | <dolio> | Like, you would not be able to write `foo :: (MonadReader a m, MonadReader b m) => a -> m b ; foo x = pure x` |
| 2025-08-14 18:02:53 +0200 | trickard__ | (~trickard@cpe-88-98-47-163.wireline.com.au) (Ping timeout: 245 seconds) |
| 2025-08-14 18:04:21 +0200 | trickard_ | (~trickard@cpe-88-98-47-163.wireline.com.au) |
| 2025-08-14 18:04:37 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 248 seconds) |
| 2025-08-14 18:07:58 +0200 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-08-14 18:11:16 +0200 | yangby | (~secret@115.205.231.82) yangby |
| 2025-08-14 18:11:43 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-08-14 18:13:01 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 18:14:46 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-08-14 18:16:04 +0200 | <ncf> | huh |
| 2025-08-14 18:20:37 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-08-14 18:24:28 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) (Server closed connection) |
| 2025-08-14 18:25:11 +0200 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale |
| 2025-08-14 18:27:58 +0200 | SoF | (~skius@user/skius) (Server closed connection) |
| 2025-08-14 18:28:33 +0200 | SoF | (~skius@user/skius) skius |
| 2025-08-14 18:28:37 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 260 seconds) |
| 2025-08-14 18:32:43 +0200 | trickard_ | (~trickard@cpe-88-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 18:32:57 +0200 | trickard_ | (~trickard@cpe-88-98-47-163.wireline.com.au) |
| 2025-08-14 18:33:41 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 18:35:09 +0200 | <monochrom> | I can see that 99% of the time the programmer intends a and b to be different, so warning/erring early is more helpful than logicing it out. |
| 2025-08-14 18:35:45 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 18:35:48 +0200 | <monochrom> | But I'm a logician, so if someone says "everyone loves my baby, but my baby loves only me" then I deduce "so you are your baby, what's the problem?" :) |
| 2025-08-14 18:40:38 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-08-14 18:41:18 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 276 seconds) |
| 2025-08-14 18:42:04 +0200 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 255 seconds) |
| 2025-08-14 18:42:37 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 260 seconds) |
| 2025-08-14 18:43:31 +0200 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2025-08-14 18:44:21 +0200 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-08-14 18:47:43 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 18:48:38 +0200 | trickard_ | (~trickard@cpe-88-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 18:48:52 +0200 | trickard_ | (~trickard@cpe-88-98-47-163.wireline.com.au) |
| 2025-08-14 18:49:46 +0200 | <ncf> | ... that doesn't follow, does it |
| 2025-08-14 18:51:32 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 18:53:06 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 272 seconds) |
| 2025-08-14 18:53:17 +0200 | <monochrom> | 0. forall x. x loves baby. So baby loves baby. 1. forall x. if baby loves x, x = me. |
| 2025-08-14 18:56:32 +0200 | <ncf> | oh |
| 2025-08-14 18:58:30 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-08-14 18:58:48 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-08-14 19:01:21 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-08-14 19:05:21 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 19:08:00 +0200 | jespada | (~jespada@2800:a4:2225:9000:913:54f8:4fc8:5494) (Ping timeout: 244 seconds) |
| 2025-08-14 19:10:38 +0200 | jespada | (~jespada@2800:a4:221c:d00:54c4:d919:36f:30dc) jespada |
| 2025-08-14 19:11:11 +0200 | trickard_ | trickard |
| 2025-08-14 19:12:08 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 19:15:30 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2025-08-14 19:17:01 +0200 | AlexZenon | (~alzenon@178.34.150.240) (Ping timeout: 252 seconds) |
| 2025-08-14 19:18:35 +0200 | AlexZenon | (~alzenon@178.34.150.240) |
| 2025-08-14 19:21:46 +0200 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-08-14 19:21:53 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 248 seconds) |
| 2025-08-14 19:22:39 +0200 | karenw_ | (~karenw@user/karenw) karenw |
| 2025-08-14 19:26:22 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |