Newest at the top
| 2026-01-18 01:53:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-18 01:51:58 +0100 | <monochrom> | an easy corollary of information theory. For a value to be usable, you must pass around sufficient information, thus the non-zero cost. |
| 2026-01-18 01:50:11 +0100 | <monochrom> | Existentials are zero-cost iff unusable. |
| 2026-01-18 01:48:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-18 01:47:16 +0100 | Core4452 | (~Zemy@2600:100c:b04a:cc3c:ac56:f4ff:fe3c:1c26) (Ping timeout: 246 seconds) |
| 2026-01-18 01:44:59 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-01-18 01:43:25 +0100 | Zemy | (~Zemy@72.178.108.235) |
| 2026-01-18 01:43:05 +0100 | droideqa | (uid499291@user/droideqa) (Quit: Connection closed for inactivity) |
| 2026-01-18 01:43:04 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 246 seconds) |
| 2026-01-18 01:38:48 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2026-01-18 01:38:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-18 01:32:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-18 01:31:08 +0100 | trickard_ | trickard |
| 2026-01-18 01:27:33 +0100 | poscat | (~poscat@user/poscat) poscat |
| 2026-01-18 01:25:43 +0100 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) |
| 2026-01-18 01:24:23 +0100 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2026-01-18 01:22:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-18 01:21:35 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 245 seconds) |
| 2026-01-18 01:20:19 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> falls more into the category of "ways to make existential-like things zero-cost" than the category "an alternative but similarly handy abstraction mechanism" |
| 2026-01-18 01:20:00 +0100 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.10.1+deb1 - https://znc.in) |
| 2026-01-18 01:18:32 +0100 | <haskellbridge> | <Man of Letters (Mikolaj)> oh wow, thank you, that's interesting |
| 2026-01-18 01:17:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-18 01:14:31 +0100 | qqq | (~qqq@185.54.21.105) (Quit: Lost terminal) |
| 2026-01-18 01:10:55 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2026-01-18 01:08:00 +0100 | <Leary> | Man of Letters (Mikolaj): Re the heterogeneous types, it's basically just a matter of building a home for your discarded types to live in. In the simplest case where all those types have the same kind, you could literally just add a type level list to your AST: `AstCastS :: (NumScalar r1, RealFrac r1, NumScalar r2, RealFrac r2) => AstTensor discarded ms s (TKS sh r1) -> AstTensor (r1:discarded) ms s (TKS sh r2)` |
| 2026-01-18 01:07:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-18 01:02:47 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 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 |