Logs: liberachat/#haskell
| 2021-08-03 06:03:46 | <shachaf> | If you know how you Church-encode (or whatever-encode) types, where the name of the type becomes an r, this is very similar. |
| 2021-08-03 06:04:13 | <shachaf> | Axman6: Well, it would be pretty useless to a caller. |
| 2021-08-03 06:04:31 | <shachaf> | Actually, I should've probably just started with that. |
| 2021-08-03 06:04:57 | <shachaf> | The way you encode (A,B) as (forall r. (A -> B -> r) -> r), and (Either A B) as (forall r. (A -> r) -> (B -> r) -> r) |
| 2021-08-03 06:05:03 | <kosmikus> | shachaf: UHC definitely supports / supported first-class existentials, although I'm not completely confident that it was free of any unexpected corner cases. |
| 2021-08-03 06:05:09 | <shachaf> | This is much more obvious in that context. |
| 2021-08-03 06:05:15 | <steven1> | Axman6: the example I found in the earlier paper is something like a state machine with a hidden state e.g. exists s. (s, s -> (s, something)) . |
| 2021-08-03 06:05:40 | <Axman6> | which we get with forall and not exposing s right? |
| 2021-08-03 06:05:45 | <shachaf> | kosmikus: I seem to remember that it didn't support class constraints, though (exists a. Show a *> a), which people complained about or something? |
| 2021-08-03 06:06:17 | <shachaf> | Axman6: A classic example is (exists s. (s, s -> Maybe s)) |
| 2021-08-03 06:06:22 | <Axman6> | data Foo a where Foo :: forall s. s -> (s -> (a,s) -> Foo a |
| 2021-08-03 06:06:25 | <shachaf> | Which represents conatural numbers. |
| 2021-08-03 06:06:27 | <steven1> | Axman6: yes, that's where my question came from, which was how we translated the exists into forall |
| 2021-08-03 06:06:48 | <kosmikus> | shachaf: I don't know. I could look it up. to be honest, I never used it, despite Atze and mostly Doaitse telling me I should :) |
| 2021-08-03 06:06:48 | <shachaf> | Axman6: Yes, that forall is the way you express existential types in GHC. |
| 2021-08-03 06:07:20 | <shachaf> | I never used it either. Not important. |
| 2021-08-03 06:07:21 | <steven1> | I figured there'd be some use in an exists syntax that internally does the translation to forall for you. Maybe it obscures too much though |
| 2021-08-03 06:07:48 | <shachaf> | I think people like to ask for super-convenient existentials, but actually figuring out what they should behave like is pretty tricky, especially if you want type inference. |
| 2021-08-03 06:07:59 | <shachaf> | And it's plausibly better for it to be explicit. |
| 2021-08-03 06:08:14 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-08-03 06:08:49 | <shachaf> | Maybe I'm the only person who doesn't think "data Thing = forall a. MkThing a" is a confusing syntax for existentials. |
| 2021-08-03 06:08:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 2021-08-03 06:09:22 | <kosmikus> | shachaf: I don't know how this conversation started. but I'm assuming you know about https://richarde.dev/papers/2021/exists/exists.pdf ?[5~[5~[5~ |
| 2021-08-03 06:09:25 | <shachaf> | It's pretty simple: If you have "data A = MkA Int", that means: If x :: Int, then MkA x :: A |
| 2021-08-03 06:09:47 | <shachaf> | And if you have "data A = forall t. MkA t", that means: For all t, if x :: t, then MkA x :: A |
| 2021-08-03 06:09:59 | <kosmikus> | shachaf: fwiw, I always thought that syntax is plausible, except that of course there's the obvious problem of people expecting to see an "exists" if the concept is called "existential types". |
| 2021-08-03 06:10:14 | <shachaf> | kosmikus: Oh, nope. I've been out of the loop for a long time. |
| 2021-08-03 06:11:52 | <kosmikus> | I haven't read the paper. so I don't how close to being implemented this is. |
| 2021-08-03 06:12:24 | <shachaf> | Note that you can write "data Exists f = forall a. Exists (f a)" in existing GHC Haskell. |
| 2021-08-03 06:12:40 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-08-03 06:12:46 | <shachaf> | And also "data k *> a = k => Foo a" for co-constraints. |
| 2021-08-03 06:13:09 | <shachaf> | I guess the paper calls that ∧? I'm a little skeptical, since it's not symmetric. |
| 2021-08-03 06:13:34 | <shachaf> | Oh, they say that right on the next page. |
| 2021-08-03 06:15:50 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 2021-08-03 06:16:46 | <shachaf> | So I guess their approach is semi-explicit but still has first-class existentials. Seems like a nice compromise! |
| 2021-08-03 06:17:41 | <shachaf> | Oh, this is from... This month? |
| 2021-08-03 06:18:38 | <shachaf> | Oh, that was just an example. |
| 2021-08-03 06:18:56 | <shachaf> | kosmikus: I guess I'll read this more carefully later. Thanks for the link! |
| 2021-08-03 06:21:38 | × | ziman quits (~ziman@c25-5.condornet.sk) (Changing host) |
| 2021-08-03 06:21:38 | → | ziman joins (~ziman@user/ziman) |
| 2021-08-03 06:22:44 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2021-08-03 06:24:00 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 256 seconds) |
| 2021-08-03 06:25:19 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 258 seconds) |
| 2021-08-03 06:25:19 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2021-08-03 06:25:23 | × | steven1 quits (~steven@172.92.136.203) (Quit: WeeChat 3.2) |
| 2021-08-03 06:25:54 | → | dschrempf joins (~dominik@070-207.dynamic.dsl.fonira.net) |
| 2021-08-03 06:26:22 | × | jespada quits (~jespada@90.254.247.46) (Ping timeout: 245 seconds) |
| 2021-08-03 06:27:14 | × | cjb quits (~cjb@user/cjb) (Quit: rcirc on GNU Emacs 28.0.50) |
| 2021-08-03 06:29:59 | × | Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-08-03 06:32:12 | × | hexeme_ quits (~hexeme@user/hexeme) (Quit: co'o ro do) |
| 2021-08-03 06:33:03 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-03 06:33:11 | → | hexeme joins (~hexeme@user/hexeme) |
| 2021-08-03 06:33:26 | → | jespada joins (~jespada@90.254.247.46) |
| 2021-08-03 06:35:51 | → | jjhoo joins (~jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) |
| 2021-08-03 06:36:09 | × | jjhoo quits (~jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) (Client Quit) |
| 2021-08-03 06:37:46 | → | jjhoo joins (~jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) |
| 2021-08-03 06:38:02 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 258 seconds) |
| 2021-08-03 06:45:42 | × | hexeme quits (~hexeme@user/hexeme) (Quit: co'o ro do) |
| 2021-08-03 06:48:48 | → | hexeme joins (~hexeme@user/hexeme) |
| 2021-08-03 06:48:57 | → | vysn joins (~vysn@user/vysn) |
| 2021-08-03 06:55:30 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:bab8:2602:a3cf:c129) |
| 2021-08-03 06:58:00 | × | curiousgay quits (~curiousga@77-120-186-48.kha.volia.net) (Ping timeout: 256 seconds) |
| 2021-08-03 06:59:11 | → | dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be) |
| 2021-08-03 07:00:21 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 2021-08-03 07:00:29 | → | chris joins (~chris@81.96.113.213) |
| 2021-08-03 07:00:34 | chris | is now known as Guest217 |
| 2021-08-03 07:01:22 | × | xff0x quits (~xff0x@2001:1a81:521f:1e00:cb93:2bda:b1c:f227) (Ping timeout: 240 seconds) |
| 2021-08-03 07:01:48 | → | michalz joins (~michalz@185.246.204.40) |
| 2021-08-03 07:02:27 | → | xff0x joins (~xff0x@2001:1a81:521f:1e00:df79:95ae:114:be51) |
| 2021-08-03 07:04:39 | → | chele joins (~chele@user/chele) |
| 2021-08-03 07:05:47 | → | fendor joins (~fendor@178.115.48.162.wireless.dyn.drei.com) |
| 2021-08-03 07:12:54 | × | ironsoba quits (~z@193.36.225.59) (Ping timeout: 272 seconds) |
| 2021-08-03 07:14:00 | → | acidjnk_new3 joins (~acidjnk@p200300d0c72b9591c199f99eb1b080aa.dip0.t-ipconnect.de) |
| 2021-08-03 07:18:39 | → | reumeth2 joins (~reumeth@user/reumeth) |
| 2021-08-03 07:18:45 | × | thyriaen quits (~thyriaen@dynamic-078-055-141-033.78.55.pool.telefonica.de) (Quit: Leaving) |
| 2021-08-03 07:20:02 | × | reumeth quits (~reumeth@user/reumeth) (Remote host closed the connection) |
| 2021-08-03 07:21:54 | <Hecate> | maralorn: hi! I don't quite understand how I can benefit from this PR https://github.com/nixos/nixpkgs/pull/125936 |
| 2021-08-03 07:22:06 | <Hecate> | because the nixpkgs search engine only shows to me 8104 |
| 2021-08-03 07:22:36 | → | ytg joins (~ytg@109-186-140-208.bb.netvision.net.il) |
| 2021-08-03 07:22:58 | × | ytg quits (~ytg@109-186-140-208.bb.netvision.net.il) (Client Quit) |
| 2021-08-03 07:24:10 | → | curiousgay joins (~curiousga@77-120-186-48.kha.volia.net) |
| 2021-08-03 07:28:08 | → | delYsid joins (~user@84-115-55-45.cable.dynamic.surfer.at) |
| 2021-08-03 07:29:34 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 2021-08-03 07:32:34 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-08-03 07:35:45 | × | m811 quits (~user@93-181-35-213.dyn.estpak.ee) (Quit: "If you put a million monkeys at a million keyboards, one of them will eventually write a Java program. The rest of them will write Perl programs.") |
| 2021-08-03 07:36:41 | → | cfricke joins (~cfricke@user/cfricke) |
| 2021-08-03 07:37:15 | → | zeenk joins (~zeenk@2a02:2f04:a211:a800:553b:3cb0:5ea1:7e83) |
| 2021-08-03 07:40:39 | × | Guest4278 quits (~yorick@pennyworth.yori.cc) (Changing host) |
| 2021-08-03 07:40:39 | → | Guest4278 joins (~yorick@user/yorick) |
| 2021-08-03 07:40:41 | Guest4278 | is now known as yorick |
| 2021-08-03 07:43:58 | → | Pickchea joins (~private@user/pickchea) |
| 2021-08-03 07:44:54 | → | kuribas joins (~user@ptr-25vy0i9yst6l4ryh82e.18120a2.ip6.access.telenet.be) |
| 2021-08-03 07:50:54 | × | dagit quits (~dagit@2601:1c2:1b7f:9fa0:5146:76a:259b:45c5) (Ping timeout: 272 seconds) |
| 2021-08-03 08:03:12 | → | CnnibisIndica joins (~herb@user/mesaboogie) |
| 2021-08-03 08:03:17 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-03 08:04:55 | CnnibisIndica | is now known as CannabisIndica |
| 2021-08-03 08:05:54 | → | hendursa1 joins (~weechat@user/hendursaga) |
| 2021-08-03 08:08:20 | → | mikoto-chan joins (~mikoto-ch@ip-193-121-10-50.dsl.scarlet.be) |
| 2021-08-03 08:08:54 | × | hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 244 seconds) |
| 2021-08-03 08:09:40 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
All times are in UTC.