Logs: liberachat/#haskell
| 2025-08-14 04:53:46 | <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 04:54:17 | <haskellbridge> | <Axman6> so writing "32 :: Index 32" should fail at compile time/GHCi |
| 2025-08-14 04:54:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 04:54:43 | <haskellbridge> | <Axman6> I'm wondering if it's possible to make writing "32 :: Index 32" a type error |
| 2025-08-14 04:55:46 | → | phma_ joins (~phma@2001:5b0:2172:ba18:237a:adb:9a49:b97a) |
| 2025-08-14 04:55:52 | phma_ | is now known as phma |
| 2025-08-14 04:57:53 | × | jespada quits (~jespada@2800:a4:2247:2400:386f:f20:8fc5:23de) (Ping timeout: 248 seconds) |
| 2025-08-14 04:58:53 | → | michalz joins (~michalz@185.246.207.218) |
| 2025-08-14 04:59:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 04:59:39 | <Leary> | Perhaps you can write something like `instance n < 32 => Num (Index n)`, then `fromInteger @(Index _) :: n < 32 => Int -> Index n`. |
| 2025-08-14 04:59:48 | <Leary> | Otherwise, there's validated-literals. |
| 2025-08-14 05:00:27 | → | jespada joins (~jespada@2800:a4:2225:9000:913:54f8:4fc8:5494) |
| 2025-08-14 05:00:28 | <Leary> | Integer* |
| 2025-08-14 05:02:58 | <Leary> | Err, ignore that first suggestion, I had a thinko. |
| 2025-08-14 05:03:44 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2025-08-14 05:05:16 | × | amadaluzia quits (~amadaluzi@user/amadaluzia) (Quit: You) |
| 2025-08-14 05:07:55 | trickard_ | is now known as trickard |
| 2025-08-14 05:08:42 | → | finsternis joins (~X@23.226.237.192) |
| 2025-08-14 05:10:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 05:14:42 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 05:15:27 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 2025-08-14 05:24:06 | → | euphores joins (~SASL_euph@user/euphores) |
| 2025-08-14 05:25:12 | × | trickard quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 05:25:25 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 05:25:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 05:30:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 05:40:51 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 05:45:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 05:55:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 05:56:55 | × | smalltalkman quits (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-08-14 05:59:55 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-08-14 06:00:22 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-14 06:11:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 06:17:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 06:28:55 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2025-08-14 06:29:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 06:33:43 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-14 06:38:53 | × | Katarushisu quits (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Read error: Connection reset by peer) |
| 2025-08-14 06:40:04 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 2025-08-14 06:40:32 | trickard_ | is now known as trickard |
| 2025-08-14 06:40:47 | → | Katarushisu joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 2025-08-14 06:41:21 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2025-08-14 06:42:32 | × | whereiseveryone quits (206ba86c98@2a03:6000:1812:100::2e4) (Server closed connection) |
| 2025-08-14 06:42:41 | → | whereiseveryone joins (206ba86c98@2a03:6000:1812:100::2e4) |
| 2025-08-14 06:44:04 | → | smalltalkman joins (uid545680@id-545680.hampstead.irccloud.com) |
| 2025-08-14 06:44:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 06:48:03 | → | weary-traveler joins (~user@user/user363627) |
| 2025-08-14 06:48:36 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-08-14 06:48:42 | × | ft quits (~ft@p508dba54.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-08-14 06:48:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 06:50:48 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
| 2025-08-14 06:54:37 | × | AlexZenon quits (~alzenon@178.34.150.240) (Ping timeout: 260 seconds) |
| 2025-08-14 06:56:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 07:00:04 | × | caconym747 quits (~caconym@user/caconym) (Quit: bye) |
| 2025-08-14 07:00:45 | → | caconym747 joins (~caconym@user/caconym) |
| 2025-08-14 07:01:07 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-08-14 07:02:24 | → | AlexZenon joins (~alzenon@178.34.150.240) |
| 2025-08-14 07:03:23 | → | takuan joins (~takuan@d8d86b9e9.access.telenet.be) |
| 2025-08-14 07:05:41 | × | jreicher quits (~user@user/jreicher) (Quit: In transit) |
| 2025-08-14 07:06:28 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 2025-08-14 07:06:37 | → | acidjnk joins (~acidjnk@p200300d6e7171985495adaceecd6b03f.dip0.t-ipconnect.de) |
| 2025-08-14 07:07:48 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-08-14 07:09:09 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-08-14 07:11:32 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2025-08-14 07:12:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-14 07:16:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-14 07:22:09 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 2025-08-14 07:35:58 | → | jreicher joins (~user@user/jreicher) |
| 2025-08-14 07:39:18 | <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 07:42:15 | × | jreicher quits (~user@user/jreicher) (Ping timeout: 244 seconds) |
| 2025-08-14 07:44:05 | → | jreicher joins (~user@user/jreicher) |
| 2025-08-14 07:46:27 | → | tromp joins (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 07:46:48 | → | fp joins (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) |
| 2025-08-14 08:01:42 | → | chele joins (~chele@user/chele) |
| 2025-08-14 08:02:43 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-08-14 08:11:03 | × | DragonMaus quits (~dragonmau@user/dragonmaus) (Ping timeout: 252 seconds) |
| 2025-08-14 08:11:35 | → | DragonMaus joins (~dragonmau@user/dragonmaus) |
| 2025-08-14 08:20:23 | → | fizbin joins (~fizbin@user/fizbin) |
| 2025-08-14 08:24:44 | × | ol0ck quits (~quassel@user/ol0ck) (Ping timeout: 260 seconds) |
| 2025-08-14 08:27:57 | × | fizbin quits (~fizbin@user/fizbin) (Ping timeout: 276 seconds) |
| 2025-08-14 08:28:41 | × | j0lol quits (~j0lol@132.145.17.236) (Server closed connection) |
| 2025-08-14 08:28:55 | → | j0lol joins (~j0lol@132.145.17.236) |
| 2025-08-14 08:51:20 | × | tromp quits (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 09:07:02 | × | trickard quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-14 09:07:16 | → | trickard_ joins (~trickard@cpe-86-98-47-163.wireline.com.au) |
| 2025-08-14 09:09:17 | → | tromp joins (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 09:27:10 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-08-14 09:29:39 | → | __monty__ joins (~toonn@user/toonn) |
| 2025-08-14 09:30:53 | × | michalz quits (~michalz@185.246.207.218) (Remote host closed the connection) |
| 2025-08-14 09:30:58 | × | Miroboru quits (~myrvoll@84.215.249.36) (Ping timeout: 255 seconds) |
| 2025-08-14 09:33:28 | → | michalz joins (~michalz@185.246.207.221) |
| 2025-08-14 09:34:20 | → | Miroboru joins (~myrvoll@84.215.249.36) |
| 2025-08-14 09:35:02 | × | fp quits (~Thunderbi@wireless-86-50-140-217.open.aalto.fi) (Ping timeout: 260 seconds) |
| 2025-08-14 09:42:00 | × | Miroboru quits (~myrvoll@84.215.249.36) (Ping timeout: 252 seconds) |
| 2025-08-14 09:43:07 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 255 seconds) |
| 2025-08-14 09:45:06 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-08-14 09:52:02 | × | tromp quits (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-14 09:57:46 | → | tremon joins (~tremon@83.80.159.219) |
| 2025-08-14 10:03:18 | → | tromp joins (~textual@2001:1c00:3487:1b00:ad02:3d09:c5b5:9908) |
| 2025-08-14 10:10:46 | × | trickard_ quits (~trickard@cpe-86-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
All times are in UTC.