Logs: liberachat/#haskell
| 2026-01-17 23:24:10 | <EvanR> | makeF add x = add (x - 1) (x + 1) |
| 2026-01-17 23:24:20 | <EvanR> | let f = makeF (+) |
| 2026-01-17 23:24:38 | <EvanR> | this might not apply exactly, I'm not sure I totally understand the situation |
| 2026-01-17 23:24:38 | <Leary> | Man of Letters (Mikolaj): Re monomorphising, I see, that's a bit unfortunate. You can perhaps get rid of those existentials by using suitable heterogeneous types instead. |
| 2026-01-17 23:24:53 | → | ethantwardy joins (~user@user/ethantwardy) |
| 2026-01-17 23:25:34 | <haskellbridge> | <Man of Letters (Mikolaj)> Leary: where can I see an example of something like that? |
| 2026-01-17 23:27:55 | → | troydm joins (~troydm@user/troydm) |
| 2026-01-17 23:28:07 | <haskellbridge> | <Man of Letters (Mikolaj)> some of the existential types arise naturally from AST GADTs (I have multiple interpreters of deeply embedded DLS in the implementation) |
| 2026-01-17 23:29:01 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-17 23:30:01 | <Leary> | The classic example is `data HList f xs where { Nil :: HList f '[]; Cons :: f x -> HList f xs -> HList f (x:xs) }`, but you can do similarly for arbitrary ASTs by duplicating some of their structure on the type level in the same way. |
| 2026-01-17 23:30:03 | <haskellbridge> | <Man of Letters (Mikolaj)> e.g., I can't think how to get rid of the existentially bound types in the node |
| 2026-01-17 23:30:03 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/QetWxmpnbhshlldjxsPntKNj/OFJ7l1DSftE (5 lines) |
| 2026-01-17 23:30:32 | <haskellbridge> | <Man of Letters (Mikolaj)> ok, thank you, I will think about this |
| 2026-01-17 23:31:55 | × | ethantwardy quits (~user@user/ethantwardy) (Quit: WeeChat 4.4.2) |
| 2026-01-17 23:32:18 | <haskellbridge> | <Man of Letters (Mikolaj)> EvanR: right, so that's precisely the purpose of my crude hack with duplicating functions (or function calls) and so helping GHC specialize each call at a concrete known type; let me explain: |
| 2026-01-17 23:33:13 | <haskellbridge> | <Man of Letters (Mikolaj)> in your example, by the well placed "let", you avoid one of the two applications of subtraction |
| 2026-01-17 23:33:51 | <haskellbridge> | <Man of Letters (Mikolaj)> in my case, by specializing/monomorphising, I get rid of more than one dictionary lookup/passing |
| 2026-01-17 23:34:08 | <EvanR> | that was monochroms version |
| 2026-01-17 23:34:21 | <haskellbridge> | <Man of Letters (Mikolaj)> oh, yes, right |
| 2026-01-17 23:34:33 | × | Inline quits (~User@2001-4dd6-dd24-0-d5a6-802e-e6e6-ce59.ipv6dyn.netcologne.de) (Ping timeout: 256 seconds) |
| 2026-01-17 23:34:55 | → | ethantwardy joins (~user@user/ethantwardy) |
| 2026-01-17 23:35:20 | <EvanR> | I was thinking that, for a given properly constructed implementation, you only do look ups into any implementation once per call to the API |
| 2026-01-17 23:35:43 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-17 23:35:44 | <EvanR> | for any of the types that have this api |
| 2026-01-17 23:35:47 | <haskellbridge> | <Man of Letters (Mikolaj)> anyway, sadly, while "let" can cache values, it can't cache the determination which dictionary to look up into and how to combine whatever has been obtained from the dictionary --- only the GHC magic can do that |
| 2026-01-17 23:36:01 | <EvanR> | :thonk: |
| 2026-01-17 23:36:28 | → | Zemy_ joins (~Zemy@2600:100c:b04a:cc3c:2826:1bff:fef2:30a6) |
| 2026-01-17 23:37:22 | <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-17 23:37:38 | → | Core3498 joins (~Zemy@72.178.108.235) |
| 2026-01-17 23:37:40 | <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-17 23:38:03 | <haskellbridge> | <Man of Letters (Mikolaj)> oh, yes, sure, e.g., you can manually write monomorphic code from the start |
| 2026-01-17 23:38:17 | <haskellbridge> | <Man of Letters (Mikolaj)> and I actually like that a lot |
| 2026-01-17 23:38:30 | <EvanR> | not monomorphic |
| 2026-01-17 23:39:01 | <EvanR> | polymorphic types can satisfy the same API as monomorphic types |
| 2026-01-17 23:39:02 | × | trickard quits (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-17 23:39:14 | → | Core4452 joins (~Zemy@2600:100c:b04a:cc3c:ac56:f4ff:fe3c:1c26) |
| 2026-01-17 23:39:15 | → | trickard_ joins (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-17 23:39:42 | × | Zemy_ quits (~Zemy@2600:100c:b04a:cc3c:2826:1bff:fef2:30a6) (Read error: Connection reset by peer) |
| 2026-01-17 23:39:44 | <EvanR> | e.g. addition interface could be implemented by Word8 or Complex a where a implements addition interface |
| 2026-01-17 23:40:04 | <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-17 23:40:12 | × | Zemy quits (~Zemy@72.178.108.235) (Ping timeout: 256 seconds) |
| 2026-01-17 23:41:10 | <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-17 23:41:26 | <haskellbridge> | <Man of Letters (Mikolaj)> yes, I fully agree |
| 2026-01-17 23:41:45 | × | bgamari quits (~bgamari@64.223.170.198) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2026-01-17 23:41:49 | × | Core3498 quits (~Zemy@72.178.108.235) (Ping timeout: 246 seconds) |
| 2026-01-17 23:43:32 | <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-17 23:44:07 | × | ethantwardy quits (~user@user/ethantwardy) (Quit: WeeChat 4.4.2) |
| 2026-01-17 23:44:15 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2026-01-17 23:44:27 | → | bgamari joins (~bgamari@64.223.173.201) |
| 2026-01-17 23:44:29 | <geekosaur> | enh, you can enable GADTSyntax without enabling GADTs |
| 2026-01-17 23:45:40 | <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-17 23:46:18 | <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-17 23:46:36 | <haskellbridge> | <Man of Letters (Mikolaj)> in many plausible ways, preferably |
| 2026-01-17 23:46:52 | <haskellbridge> | <Man of Letters (Mikolaj)> with similar correctness guarantees |
| 2026-01-17 23:47:03 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-17 23:47:58 | <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-17 23:48:07 | <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-17 23:48:08 | <geekosaur> | I'm confused. Doesn't that extra correctness come specifically from the embedded existentials, which are exposed by scrutinizing constructors? |
| 2026-01-17 23:48:10 | <EvanR> | in cases where you use existentials |
| 2026-01-17 23:49:00 | <haskellbridge> | <Man of Letters (Mikolaj)> geekosaur: I'm afraid so, but maybe there is another way? |
| 2026-01-17 23:49:15 | <EvanR> | doing existentials without existentials sounds tricky |
| 2026-01-17 23:49:25 | <EvanR> | (and what's the point) |
| 2026-01-17 23:49:30 | <haskellbridge> | <Man of Letters (Mikolaj)> :D |
| 2026-01-17 23:50:23 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2026-01-17 23:50:59 | → | ethantwardy joins (~user@user/ethantwardy) |
| 2026-01-17 23:51:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-17 23:52:51 | <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-17 23:53:47 | <haskellbridge> | <Man of Letters (Mikolaj)> and being so handy, they easily pollute the performance-sensitive parts of the application |
| 2026-01-17 23:55:03 | catties | is now known as kitties |
| 2026-01-17 23:55:27 | <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-17 23:56:30 | <haskellbridge> | <Man of Letters (Mikolaj)> ;< |
| 2026-01-17 23:57:23 | × | trickard_ quits (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-17 23:57:37 | → | trickard_ joins (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-17 23:58:10 | <geekosaur> | (GADT-style, at least) |
| 2026-01-17 23:58:18 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2026-01-18 00:02:47 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-18 00:07:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-18 00:08:00 | <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 00:10:55 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2026-01-18 00:14:31 | × | qqq quits (~qqq@185.54.21.105) (Quit: Lost terminal) |
| 2026-01-18 00:17:09 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-18 00:18:32 | <haskellbridge> | <Man of Letters (Mikolaj)> oh wow, thank you, that's interesting |
| 2026-01-18 00:20:00 | × | mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.10.1+deb1 - https://znc.in) |
| 2026-01-18 00:20:19 | <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 00:21:35 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 245 seconds) |
| 2026-01-18 00:22:14 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-18 00:24:23 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 2026-01-18 00:25:43 | → | mhatta joins (~mhatta@www21123ui.sakura.ne.jp) |
| 2026-01-18 00:27:33 | → | poscat joins (~poscat@user/poscat) |
| 2026-01-18 00:31:08 | trickard_ | is now known as trickard |
| 2026-01-18 00:32:56 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-18 00:38:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-18 00:38:48 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 2026-01-18 00:43:04 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 246 seconds) |
| 2026-01-18 00:43:05 | × | droideqa quits (uid499291@user/droideqa) (Quit: Connection closed for inactivity) |
| 2026-01-18 00:43:25 | → | Zemy joins (~Zemy@72.178.108.235) |
| 2026-01-18 00:44:59 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2026-01-18 00:47:16 | × | Core4452 quits (~Zemy@2600:100c:b04a:cc3c:ac56:f4ff:fe3c:1c26) (Ping timeout: 246 seconds) |
| 2026-01-18 00:48:43 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-18 00:50:11 | <monochrom> | Existentials are zero-cost iff unusable. |
All times are in UTC.