Newest at the top
| 2026-01-18 00:58:18 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2026-01-18 00:58:10 +0100 | <geekosaur> | (GADT-style, at least) |
| 2026-01-18 00:57:37 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-18 00:57:23 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-18 00:56:30 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> ;< |
| 2026-01-18 00:55:27 +0100 | <geekosaur> | I think the only other alternative isn't here yet: dependent type witnesses of some kind. Which are also not zero cost, and I suspect end up being just a different way to encode existentials |
| 2026-01-18 00:55:03 +0100 | catties | kitties |
| 2026-01-18 00:53:47 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> and being so handy, they easily pollute the performance-sensitive parts of the application |
| 2026-01-18 00:52:51 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> well, the point is, they are not a zero-cost abstraction unlike, in principle, most of other abstractions Haskell provides |
| 2026-01-18 00:51:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-18 00:50:59 +0100 | ethantwardy | (~user@user/ethantwardy) ethantwardy |
| 2026-01-18 00:50:23 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-18 00:49:30 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> :D |
| 2026-01-18 00:49:25 +0100 | <EvanR> | (and what's the point) |
| 2026-01-18 00:49:15 +0100 | <EvanR> | doing existentials without existentials sounds tricky |
| 2026-01-18 00:49:00 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> geekosaur: I'm afraid so, but maybe there is another way? |
| 2026-01-18 00:48:10 +0100 | <EvanR> | in cases where you use existentials |
| 2026-01-18 00:48:08 +0100 | <geekosaur> | I'm confused. Doesn't that extra correctness come specifically from the embedded existentials, which are exposed by scrutinizing constructors? |
| 2026-01-18 00:48:07 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> for a non-trivial AST (I don't remember Peano arithmetic or lambda calculus already have existential types in the classic encoding) |
| 2026-01-18 00:47:58 +0100 | <EvanR> | the GADTsyntax is besides the point, since the key thing is case analyzing to introduce the forgotten now unknown type... however it was defined and constructed |
| 2026-01-18 00:47:03 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-18 00:46:52 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> with similar correctness guarantees |
| 2026-01-18 00:46:36 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> in many plausible ways, preferably |
| 2026-01-18 00:46:18 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> I'd love to read some functional pearl that rewrites the classic GADT AST examples without existentials in some fancy way |
| 2026-01-18 00:45:40 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> oh no, but the sweet reward is in the extra type correctness real GADTs ensure, unlike GADTSyntax, especially for syntax-like things |
| 2026-01-18 00:44:29 +0100 | <geekosaur> | enh, you can enable GADTSyntax without enabling GADTs |
| 2026-01-18 00:44:27 +0100 | bgamari | (~bgamari@64.223.173.201) |
| 2026-01-18 00:44:15 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-01-18 00:44:07 +0100 | ethantwardy | (~user@user/ethantwardy) (Quit: WeeChat 4.4.2) |
| 2026-01-18 00:43:32 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> but once you start writing GADTs it's so hard to avoid existentials; I tried for a while, marked each one in the source code, but quickly gave up --- too many :) |
| 2026-01-18 00:41:49 +0100 | Core3498 | (~Zemy@72.178.108.235) (Ping timeout: 246 seconds) |
| 2026-01-18 00:41:45 +0100 | bgamari | (~bgamari@64.223.170.198) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2026-01-18 00:41:26 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> yes, I fully agree |
| 2026-01-18 00:41:10 +0100 | <EvanR> | aiui typeclasses shine in cases where you can get away without talking about explicit dictionaries, since it will be passed automagically around |
| 2026-01-18 00:40:12 +0100 | Zemy | (~Zemy@72.178.108.235) (Ping timeout: 256 seconds) |
| 2026-01-18 00:40:04 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> yes, you are right, code without existentials, plus "-fexpose-overloaded-unfoldings" and "-fspecialise-aggressively" should in theory be just as good at avoiding runtime lookups |
| 2026-01-18 00:39:44 +0100 | <EvanR> | e.g. addition interface could be implemented by Word8 or Complex a where a implements addition interface |
| 2026-01-18 00:39:42 +0100 | Zemy_ | (~Zemy@2600:100c:b04a:cc3c:2826:1bff:fef2:30a6) (Read error: Connection reset by peer) |
| 2026-01-18 00:39:15 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-18 00:39:14 +0100 | Core4452 | (~Zemy@2600:100c:b04a:cc3c:ac56:f4ff:fe3c:1c26) |
| 2026-01-18 00:39:02 +0100 | trickard | (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-18 00:39:01 +0100 | <EvanR> | polymorphic types can satisfy the same API as monomorphic types |
| 2026-01-18 00:38:30 +0100 | <EvanR> | not monomorphic |
| 2026-01-18 00:38:17 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> and I actually like that a lot |
| 2026-01-18 00:38:03 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> oh, yes, sure, e.g., you can manually write monomorphic code from the start |
| 2026-01-18 00:37:40 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> and the same regarding knots --- Haskell recursion doesn't cut it, something involving GHC internals would be needed (or something totally out of the box like maybe the heterogeneous types idea once I understand it) |
| 2026-01-18 00:37:38 +0100 | Core3498 | (~Zemy@72.178.108.235) |
| 2026-01-18 00:37:22 +0100 | <EvanR> | I would guess whatever ghc magic that is can be "manually" coded into the implementations, but no bearing on how the effort compares |
| 2026-01-18 00:36:28 +0100 | Zemy_ | (~Zemy@2600:100c:b04a:cc3c:2826:1bff:fef2:30a6) |
| 2026-01-18 00:36:01 +0100 | <EvanR> | :thonk: |