Newest at the top
| 2025-01-12 15:50:04 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2025-01-12 15:47:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-12 15:44:16 +0100 | tnt2 | tnt1 |
| 2025-01-12 15:44:16 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-01-12 15:43:39 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-12 15:43:02 +0100 | dysthesis | (~dysthesis@user/dysthesis) (Remote host closed the connection) |
| 2025-01-12 15:42:04 +0100 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-01-12 15:39:21 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-01-12 15:37:49 +0100 | tnt2 | tnt1 |
| 2025-01-12 15:37:49 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-01-12 15:37:12 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-12 15:36:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2025-01-12 15:32:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-12 15:29:38 +0100 | <ncf> | data Exists t where pack :: forall a. t a → Exists t |
| 2025-01-12 15:28:23 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f06145d2259bf66d21b.dip0.t-ipconnect.de) |
| 2025-01-12 15:27:33 +0100 | dysthesis | (~dysthesis@user/dysthesis) dysthesis |
| 2025-01-12 15:23:12 +0100 | <hellwolf> | (forall a. (t a -> r)) ≅ ((exists a. t a) -> r) <-- this is what I know of. |
| 2025-01-12 15:23:06 +0100 | <hellwolf> | I have never heard of that |
| 2025-01-12 15:21:16 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-12 15:19:31 +0100 | <haskellbridge> | <Profpatsch> s/??/?/ |
| 2025-01-12 15:19:22 +0100 | <haskellbridge> | <Profpatsch> though GADTs are a superset of existential types right?? |
| 2025-01-12 15:18:55 +0100 | <hellwolf> | impredicative types I don't actively use, but passively use from a library that requiring it |
| 2025-01-12 15:18:51 +0100 | <haskellbridge> | <Profpatsch> (same as with GADTs, though people tell me they have their uses) |
| 2025-01-12 15:18:40 +0100 | <hellwolf> | oh, I meant existential types |
| 2025-01-12 15:18:28 +0100 | <haskellbridge> | <Profpatsch> esp. because error messages and inference becomes a joke with impredicative types |
| 2025-01-12 15:18:27 +0100 | <hellwolf> | okay, but I am not sure if were complicated in the first place |
| 2025-01-12 15:18:03 +0100 | <haskellbridge> | <Profpatsch> any time I thought I needed these, I could usually slightly redesign and vastly simplify |
| 2025-01-12 15:17:34 +0100 | <hellwolf> | yes, I use it in places |
| 2025-01-12 15:17:21 +0100 | <haskellbridge> | <Profpatsch> (that is not just a toy example I mean) |
| 2025-01-12 15:17:20 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-01-12 15:17:11 +0100 | <haskellbridge> | <Profpatsch> do you have an example? |
| 2025-01-12 15:16:55 +0100 | <haskellbridge> | <Profpatsch> I don’t really run into situations where I need that flexibility tbh |
| 2025-01-12 15:16:44 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-12 15:15:51 +0100 | <haskellbridge> | <Profpatsch> At least I don’t |
| 2025-01-12 15:15:48 +0100 | <haskellbridge> | <Profpatsch> no you don’t really need them usually |
| 2025-01-12 15:15:11 +0100 | <hellwolf> | I sometimes create an array of AnyX existential data types. |
| 2025-01-12 15:14:49 +0100 | <haskellbridge> | <Profpatsch> in what case? |
| 2025-01-12 15:14:05 +0100 | <hellwolf> | would you also need ImpredicativeTypes in that case? |
| 2025-01-12 15:08:48 +0100 | <haskellbridge> | <Profpatsch> usually RankN solves most things |
| 2025-01-12 15:08:40 +0100 | <haskellbridge> | <Profpatsch> bailsman: agree, I haven’t felt like I needed an existential type in a long time |
| 2025-01-12 15:07:00 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-01-12 15:06:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-12 15:05:42 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-12 15:02:49 +0100 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
| 2025-01-12 15:01:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-12 14:56:44 +0100 | tnt2 | tnt1 |
| 2025-01-12 14:56:44 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-01-12 14:56:20 +0100 | <bailsman> | ...yes I've found many cases in which I thought I needed an existential type. I'm glad this is a rite of passage. Although, I still often think I need it, so I'm not sure if I've fully completed the rite yet |
| 2025-01-12 14:54:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2025-01-12 14:54:44 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |