Newest at the top
| 2024-10-30 11:13:54 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-30 11:13:28 +0100 | ggb | (a62ffbaf4f@2a03:6000:1812:100::3ac) ggb |
| 2024-10-30 11:12:51 +0100 | <ph88> | You mean this list? https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/existential_quantification.html#res… |
| 2024-10-30 11:12:37 +0100 | petrichor | (~znc-user@user/petrichor) petrichor |
| 2024-10-30 11:11:56 +0100 | <tomsmeding> | nice, this list is cool, I should have read it years ago |
| 2024-10-30 11:11:30 +0100 | <tomsmeding> | apparently this is not sufficient reason to lift the restricion :p |
| 2024-10-30 11:11:10 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800:c35a:a881:34b9:612a) ph88 |
| 2024-10-30 11:11:08 +0100 | <tomsmeding> | lol, re the third bullet point: the fact that newtypes cannot be existential leads to this data type https://hackage.haskell.org/package/some-1.0.6/docs/Data-Some.html having a very evil implementation |
| 2024-10-30 11:08:49 +0100 | <ph88^> | thanks! i'll see if i can understand it |
| 2024-10-30 11:08:47 +0100 | <tomsmeding> | apparently it's "otherwise the implementation gets even more complicated" :D |
| 2024-10-30 11:08:33 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800:3808:5ad1:785a:e722) (Ping timeout: 265 seconds) |
| 2024-10-30 11:08:27 +0100 | sus | (1b7af6299f@user/zeromomentum) zeromomentum |
| 2024-10-30 11:08:26 +0100 | bwolf | (c3bc363dd1@2a03:6000:1812:100::180) bwolf |
| 2024-10-30 11:08:21 +0100 | rselim | (ce261f06ff@user/milesrout) milesrout |
| 2024-10-30 11:08:19 +0100 | <tomsmeding> | ph88: second bullet point here https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/existential_quantification.html#res… |
| 2024-10-30 11:08:18 +0100 | RussetParrotBear | (45ce440a48@2a03:6000:1812:100::e2) |
| 2024-10-30 11:08:13 +0100 | ubert | (~Thunderbi@178.165.189.55.wireless.dyn.drei.com) ubert |
| 2024-10-30 11:08:11 +0100 | jleightcap | (7bc4014b62@user/jleightcap) jleightcap |
| 2024-10-30 11:08:09 +0100 | JoelMcCracken | (5ea8252fbb@2a03:6000:1812:100::10e3) JoelMcCracken |
| 2024-10-30 11:08:06 +0100 | samhh | (7569f027cf@2a03:6000:1812:100::e4) samhh |
| 2024-10-30 11:07:56 +0100 | whereiseveryone | (206ba86c98@2a03:6000:1812:100::2e4) whereiseveryone |
| 2024-10-30 11:07:53 +0100 | jakzale | (6291399afa@user/jakzale) jakzale |
| 2024-10-30 11:07:52 +0100 | evanrelf | (3addc196af@2a03:6000:1812:100::f0) evanrelf |
| 2024-10-30 11:07:52 +0100 | chaitlatte0 | (ea29c0bb16@user/chaitlatte0) chaitlatte0 |
| 2024-10-30 11:07:50 +0100 | bsima1 | (9d7e39c8ad@2a03:6000:1812:100::dd) |
| 2024-10-30 11:07:49 +0100 | jkoshy | (99b9359beb@user/jkoshy) jkoshy |
| 2024-10-30 11:07:49 +0100 | smiesner | (b0cf5acf8c@user/smiesner) smiesner |
| 2024-10-30 11:07:45 +0100 | Ankhers | (e99e97ef8e@2a03:6000:1812:100::2a2) Ankhers |
| 2024-10-30 11:07:44 +0100 | aniketd | (32aa4844cd@2a03:6000:1812:100::dcb) aniketd |
| 2024-10-30 11:07:43 +0100 | fn_lumi | (3d621153a5@2a03:6000:1812:100::df7) fn_lumi |
| 2024-10-30 11:07:43 +0100 | titibandit | (e33ffbab65@user/titibandit) titibandit |
| 2024-10-30 11:07:41 +0100 | ursa-major | (114efe6c39@2a03:6000:1812:100::11f3) ursa-major |
| 2024-10-30 11:07:39 +0100 | lane | (809450f172@2a03:6000:1812:100::1300) lane |
| 2024-10-30 11:07:39 +0100 | fvr | (ef3e56ca8b@2a03:6000:1812:100::3c4) fvr |
| 2024-10-30 11:06:38 +0100 | mesaoptimizer | (~mesaoptim@user/PapuaHardyNet) PapuaHardyNet |
| 2024-10-30 11:06:34 +0100 | ph88^ | (~ph88@2a02:8109:9e26:c800:ed53:7d07:6030:570a) |
| 2024-10-30 11:06:24 +0100 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 2024-10-30 11:06:24 +0100 | <tomsmeding> | but there are bits and pieces here and there |
| 2024-10-30 11:05:45 +0100 | <tomsmeding> | ph88: hm, seems the paper doesn't really explain the status quo |
| 2024-10-30 11:05:03 +0100 | <preflex> | 10 |
| 2024-10-30 11:05:03 +0100 | <mauke> | preflex: calc 2 3 *)+ 4 |
| 2024-10-30 11:03:58 +0100 | <tomsmeding> | ph88: yes, I think that's what's happening |
| 2024-10-30 11:03:50 +0100 | <tomsmeding> | (I read this a few years ago) |
| 2024-10-30 11:03:46 +0100 | <tomsmeding> | ph88: dunno, but this paper is related (it presents a generalisation to Haskell's type system that does allow more flexible existentials) and it's sure to include an explanation of the status quo :p https://dl.acm.org/doi/pdf/10.1145/3473569 |
| 2024-10-30 11:03:25 +0100 | <ph88> | you mentioned before that the let binding is lazy, thus not creating the suitable scope ? |
| 2024-10-30 11:02:50 +0100 | <tomsmeding> | 'let' doesn't make a suitable scope |
| 2024-10-30 11:02:37 +0100 | <tomsmeding> | and to preserve soundness, the external type of that construct cannot mention the existential type variable |
| 2024-10-30 11:02:35 +0100 | <ph88> | i had a feeling about scoping. Though i didn't realize it was because of the let-binding and a case would fix that. Is there any documentation to read about let-bindings and scoping issue? |
| 2024-10-30 11:02:24 +0100 | <tomsmeding> | this has to do with how haskell treats existential types; if you have an existential type variable, then such a thing is _scoped_: it's introduced by some scoping construct (a function argument, case, lambda, etc.), and has some unknown yet rigid meaning inside of that scope |
| 2024-10-30 11:02:15 +0100 | fgaz | (1ff9197ed6@2a03:6000:1812:100::11ea) fgaz |