Newest at the top
| 2025-04-28 06:29:30 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
| 2025-04-28 06:27:48 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2025-04-28 06:27:36 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2025-04-28 06:18:55 +0200 | <ames> | i think some emoji should be uppercase so we can use them as constructors |
| 2025-04-28 06:16:56 +0200 | <haskellbridge> | <Liamzee> if you want an operator version of go, emojis actually suffice since they have no collisions and are single characters. They also brighten up your day. :) |
| 2025-04-28 06:16:16 +0200 | <haskellbridge> | <Liamzee> you know how emojis are actually part of the haskell operator namespace? |
| 2025-04-28 06:16:01 +0200 | <haskellbridge> | <Liamzee> huh, that's interesting, and probably extremely degenerate |
| 2025-04-28 06:11:35 +0200 | <haskellbridge> | <Bowuigi> Ah, sorry, that's not what I meant. I mean that one should resist the temptation to add a lot of shiny new features, as with any software project |
| 2025-04-28 06:10:18 +0200 | <ames> | but you're talking about these things as if there's a "universal dependently-typed language" that everyone's converging to. this is nonsense. idris people are not interested in "more complex equality" or "cubical stuff" and lean people are outright hostile towards these things |
| 2025-04-28 06:06:25 +0200 | <haskellbridge> | <Bowuigi> I should take more notes |
| 2025-04-28 06:06:13 +0200 | <haskellbridge> | <Bowuigi> Can't find the IIT/IRT stuff on the Coq issues but I remember some talk about supporting them exists lol |
| 2025-04-28 06:05:30 +0200 | <haskellbridge> | <Bowuigi> Yeah that's the idea |
| 2025-04-28 06:03:40 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) (Quit: Client closed) |
| 2025-04-28 06:00:37 +0200 | <ames> | "previous steps" - those are completely orthogonal features. |
| 2025-04-28 05:59:56 +0200 | <haskellbridge> | <Bowuigi> The previous steps (inductive-inductive and inductive-recursive stuff) were added / are in progress because of user demand in Coq AFAIU |
| 2025-04-28 05:58:54 +0200 | <ames> | "make three to throw away" and all that |
| 2025-04-28 05:58:05 +0200 | <ames> | coq does not have anything approaching a cubical mode and jon's proof assistants are basically proofs-of-concept |
| 2025-04-28 05:57:59 +0200 | <haskellbridge> | <Bowuigi> It isn't that big of a problem for theorem provers because well, they exist to prove theorems, but Haskell is not a theorem prover |
| 2025-04-28 05:55:42 +0200 | <haskellbridge> | <Bowuigi> As for the "I want to prove more" thing, Agda is the prime example, but Coq and the Red* family (tho that's many languages, so not that big of an issue) are following suit. The rest are kinda on the same path, but moving more slowly |
| 2025-04-28 05:54:58 +0200 | <haskellbridge> | <Bowuigi> I see |
| 2025-04-28 05:54:36 +0200 | <ames> | it's erasing the things that *aren't* types e.g. lengths of vectors that's complicated |
| 2025-04-28 05:54:01 +0200 | <ames> | also erasing types is very easy. code generators for languages that aren't Idris2 simply do not include a way to generate code for types |
| 2025-04-28 05:52:25 +0200 | <ames> | seems very strange to assume that this is a common thing to do when there's exactly one language that's done that |
| 2025-04-28 05:52:23 +0200 | <haskellbridge> | <Bowuigi> Suddenly to get a chance of using the newest features you need a PhD because progress is not quite there yet |
| 2025-04-28 05:51:02 +0200 | <haskellbridge> | ... extension types, then you take a Higher Observational detour aaaand you've reached current research and are stuck with a very complex system that's too hard to verify properly. |
| 2025-04-28 05:50:57 +0200 | <haskellbridge> | <Bowuigi> Also, opening the door to dependent types means allowing the "I want to prove more and more" philosophy. First one adds the base constructs because deriving the eta laws for the rest of things is harder with just pi types (unless you use a novel trick from a random thesis I read and forgot about), then dependent ADTs, then slightly more complex equality, then HITs, then IRTs, then IITs, then cubical stuff, then... |
| 2025-04-28 05:45:42 +0200 | <haskellbridge> | <Bowuigi> Another big reason was hinted at here too: Dependent types + unrestricted effects = magic. You can get something with a random type or with a type you read from stdin. Dependent types in Haskell aren't just about the proofs, it's about making a stupidly powerful language for everyone |
| 2025-04-28 05:43:53 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-28 05:42:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 05:41:51 +0200 | <haskellbridge> | <Bowuigi> Also that's partly why dependent haskell takes so much effort |
| 2025-04-28 05:41:32 +0200 | <haskellbridge> | <Bowuigi> EvanR type erasure is part of standard optimization in any functional lang. Dependently typed langs get a "cut-down" version of it that requires complex algorithms to work properly (not sure if it's actually decidable). It's a problem on dependently typed langs, but a given on the rest |
| 2025-04-28 05:38:38 +0200 | <haskellbridge> | <Bowuigi> loonycyborg if your pi type acts as a forall, you can erase it safely. There's more conditions but that's the most intuitive one |
| 2025-04-28 05:36:08 +0200 | cbs | (df2953d28a@2a03:6000:1812:100::1451) () |
| 2025-04-28 05:35:16 +0200 | cbs | (df2953d28a@2a03:6000:1812:100::1451) cbs |
| 2025-04-28 05:32:37 +0200 | koz | (~koz@121.99.240.58) |
| 2025-04-28 05:31:45 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 05:30:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-28 05:12:38 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 05:12:21 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 05:03:56 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 05:03:40 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 05:01:43 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-28 04:56:45 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-04-28 04:51:08 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 04:50:18 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-28 04:50:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 04:49:47 +0200 | Square | (~Square@user/square) (Ping timeout: 265 seconds) |
| 2025-04-28 04:49:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 04:48:47 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 04:45:25 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |