2025/01/12

Newest at the top

2025-01-12 15:44:16 +0100tnt2tnt1
2025-01-12 15:44:16 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 252 seconds)
2025-01-12 15:43:39 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-12 15:43:02 +0100dysthesis(~dysthesis@user/dysthesis) (Remote host closed the connection)
2025-01-12 15:42:04 +0100todi(~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2025-01-12 15:39:21 +0100wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2025-01-12 15:37:49 +0100tnt2tnt1
2025-01-12 15:37:49 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 265 seconds)
2025-01-12 15:37:12 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-12 15:36:39 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2025-01-12 15:32:08 +0100merijn(~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 +0100acidjnk_new(~acidjnk@p200300d6e7283f06145d2259bf66d21b.dip0.t-ipconnect.de)
2025-01-12 15:27:33 +0100dysthesis(~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 +0100merijn(~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 +0100merijn(~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 +0100wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-01-12 15:06:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-12 15:05:42 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-12 15:02:49 +0100supercode(~supercode@user/supercode) (Quit: Client closed)
2025-01-12 15:01:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-12 14:56:44 +0100tnt2tnt1
2025-01-12 14:56:44 +0100tnt1(~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 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2025-01-12 14:54:44 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-12 14:50:26 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-12 14:47:04 +0100tnt2tnt1