Newest at the top
| 2025-01-10 12:50:07 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-10 12:50:04 +0100 | <mari47944> | reorder or wrap it, not aware of anything better |
| 2025-01-10 12:49:23 +0100 | sprotte24 | (~sprotte24@p200300d16f053e00ccd1db6c99978e80.dip0.t-ipconnect.de) (Client Quit) |
| 2025-01-10 12:48:29 +0100 | sprotte24 | (~sprotte24@p200300d16f053e00ccd1db6c99978e80.dip0.t-ipconnect.de) |
| 2025-01-10 12:47:57 +0100 | <[exa]> | (background: I didn't write that type but it screams for a functor instance) |
| 2025-01-10 12:47:02 +0100 | <hellwolf> | Leary: thanks! |
| 2025-01-10 12:46:40 +0100 | <[exa]> | if I have a datatype with 2 arguments, say `X a b`, and I want to make a Functor instance so that the thing is functorial in the `a` variable (i.e, not the last one as usual), is there some kind of adaptor that would allow me to fit this somewhat nicely, or do I always have to reorder the type arguments? |
| 2025-01-10 12:46:09 +0100 | alist | (~alist@user/alist) (Quit: Leaving) |
| 2025-01-10 12:41:52 +0100 | TMA | (tma@twin.jikos.cz) (Ping timeout: 252 seconds) |
| 2025-01-10 12:41:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-10 12:34:01 +0100 | todi1 | todi |
| 2025-01-10 12:28:19 +0100 | notzmv | (~umar@user/notzmv) (Ping timeout: 245 seconds) |
| 2025-01-10 12:27:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-10 12:27:38 +0100 | <Leary> | (taking `D` as a type unrelated to the constructor) |
| 2025-01-10 12:26:34 +0100 | <Leary> | If you wish, you can encode the existential with `[forall r. (forall a. D a -> r) -> r]`, but I don't really think that's an improvement. |
| 2025-01-10 12:25:23 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-10 12:25:16 +0100 | <Leary> | hellwolf: You should regard the syntax `data AnyD = forall a. D a` as a mistake and not be misled by it. One list has a universally quantified type, the other existentially---they're very different. |
| 2025-01-10 12:24:09 +0100 | CiaoSen | (~Jura@2a05:5800:2e7:b00:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
| 2025-01-10 12:21:07 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-10 12:20:51 +0100 | g00gler | (uid125351@id-125351.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-10 12:19:32 +0100 | alist | (~alist@user/alist) alist |
| 2025-01-10 12:17:56 +0100 | son0p | (~ff@2800:e6:4001:6cc3:2e2c:4b4e:bc2a:6f17) (Ping timeout: 272 seconds) |
| 2025-01-10 12:15:49 +0100 | mari-estel | (~mari-este@user/mari-estel) (Ping timeout: 252 seconds) |
| 2025-01-10 12:15:15 +0100 | <hellwolf> | say [forall a. D a] vs. [AnyD] where data AnyD = forall a. D a |
| 2025-01-10 12:14:37 +0100 | <hellwolf> | They look very similar to me, in forms and shapes. But probably someone here knows more can answer immediately, is ImpredicativeType possible to replace the common usage of existential types? |
| 2025-01-10 12:13:45 +0100 | mari47944 | (~mari-este@user/mari-estel) mari-estel |
| 2025-01-10 12:07:46 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-10 11:58:33 +0100 | alist | (~alist@user/alist) (Quit: Leaving) |
| 2025-01-10 11:53:02 +0100 | <alist> | i think i can parse it but. idk sorry to flood the chat with like this one obsession i have |
| 2025-01-10 11:52:46 +0100 | <alist> | the paper is also sort of doubly confusing because it seems to use like an old version of set-builder notation? and it sometimes uses lambdas to describe set-theoretic functions haha |
| 2025-01-10 11:50:15 +0100 | <alist> | to be honest it seems to really have worked, ive been here for two days and both times people were able to answer really specific questions about this paper really quickly |
| 2025-01-10 11:49:26 +0100 | <haskellbridge> | <sm> haha, the old "hang out for a couple of decades" manouver eh |
| 2025-01-10 11:46:41 +0100 | <alist> | im hoping for the fast track |
| 2025-01-10 11:46:35 +0100 | <alist> | haha well i dont know if i have that kind of time |
| 2025-01-10 11:46:07 +0100 | <geekosaur> | that said, I got there by hanging out here for a couple decades 🙂 |
| 2025-01-10 11:45:41 +0100 | <geekosaur> | I'm fairly weak on type theory myself but can generally follow this stuff to some extent |
| 2025-01-10 11:45:13 +0100 | <alist> | geekosaur: right i understand this. i also understand how functions are relations. i have a mathematics background, but nothing related to type theory. |
| 2025-01-10 11:44:37 +0100 | <Athas> | merijn: yes, or just check for the Z and pick the right function. It feels a bit dumb, though. |
| 2025-01-10 11:44:27 +0100 | <geekosaur> | so, mathematically a function is exactly a mapping of values in the domain (input, with some handwaving) to values in the codomain (output, with similar handwaving) |
| 2025-01-10 11:44:18 +0100 | <alist> | geekosaur: ive been staring at what you wrote for like 10 minutes now and i think maybe im starting to get it? |
| 2025-01-10 11:43:44 +0100 | <alist> | merijn: i see. well thank you anyway, you have been very kind |
| 2025-01-10 11:43:19 +0100 | <merijn> | alist: That's beyond what I can skim from the paper and it's lunchtime |
| 2025-01-10 11:43:15 +0100 | <geekosaur> | probably easiest |
| 2025-01-10 11:43:11 +0100 | <geekosaur> | ^ |
| 2025-01-10 11:43:04 +0100 | <merijn> | Athas: Crazy talk: Why not replace Z with offset 0:00? :) |
| 2025-01-10 11:42:53 +0100 | <alist> | ah yes, but the advantage i guess is that they are not the same "kind" of set as the just collections of values. they are actual mappings? |
| 2025-01-10 11:42:47 +0100 | <geekosaur> | Athas, git is the one being annoying there, it should be consistent. I think the best you can do is try both and use the one that succeeds |
| 2025-01-10 11:42:04 +0100 | <merijn> | alist: Which, can be confusing, because in some sense relations are just "more sets" depending how you squint and how rigid you like your formalisms :p |
| 2025-01-10 11:41:24 +0100 | <merijn> | alist: we view types of functions as *relations* between sets, that's what that bit is about |
| 2025-01-10 11:39:48 +0100 | <Athas> | The ISO8601 instance for ZonedTime allows the offset (but not Z), while the instance for UTCTime allows Z (but not the offset). |