Newest at the top
| 2025-04-28 09:04:21 +0200 | geekosaur | wonders how long those were queued |
| 2025-04-28 09:04:18 +0200 | <haskellbridge> | <Bowuigi> "Everyone's bad at code" and "I like having a good mental health" are probably why we still have PL research lol |
| 2025-04-28 09:04:16 +0200 | <haskellbridge> | <hellwolf> what is that? |
| 2025-04-28 09:04:14 +0200 | <haskellbridge> | <Bowuigi> Also dependent types don't correspond to propositional logic, but rather to less mainstream logics that have more power in some places but less in others |
| 2025-04-28 09:04:12 +0200 | <haskellbridge> | <Bowuigi> Yeah that's the main idea, but formalizing/verifying stuff is optional, you can use a dependently typed lang without making use of any dependent types |
| 2025-04-28 09:04:10 +0200 | <haskellbridge> | <hellwolf> From logic's perspective, is dependent type to make the quantifiers more rigour vs. in Haskell usually you hand wave it or slap a quickcheck to it for the day? |
| 2025-04-28 09:04:08 +0200 | <haskellbridge> | <Bowuigi> Actually dependency in user-defined ADTs is good. With base constructs I mean pi and sigma types |
| 2025-04-28 09:04:07 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/UEPByodBGyiSVOqodXeCtYPh/LKR6AzyTcQ4 (3 lines) |
| 2025-04-28 09:04:05 +0200 | <haskellbridge> | <hellwolf> - propositional logic <-> static types (?) |
| 2025-04-28 09:04:04 +0200 | <haskellbridge> | <Bowuigi> Up to and including the base constructs seems good enough I guess |
| 2025-04-28 09:04:02 +0200 | <haskellbridge> | What's the healthy level of proofs that you would put in Haskell? |
| 2025-04-28 09:04:01 +0200 | <haskellbridge> | <hellwolf> interesting dependent types thread... |
| 2025-04-28 09:03:59 +0200 | <haskellbridge> | <hellwolf> "less run time error" is probably the "KPI" |
| 2025-04-28 09:03:57 +0200 | <haskellbridge> | <hellwolf> understand. i am the consumer of type systems, i try to use it for something. by too trivial proofs, i meant judging from the value where it is used |
| 2025-04-28 09:03:56 +0200 | <haskellbridge> | <Bowuigi> (Those are independent replies from 1 to 3, in order) |
| 2025-04-28 09:03:54 +0200 | <haskellbridge> | <Bowuigi> Other logics can be embedded on top by using the actual implementation as a framework, but it's not a full replacement yeah |
| 2025-04-28 09:03:52 +0200 | <haskellbridge> | <Bowuigi> Proofs about type systems are the proofs I read the most, I like how easy it is to do those in Twelf |
| 2025-04-28 09:03:50 +0200 | <haskellbridge> | <Bowuigi> If a proof is too trivial for you, it's probably also trivial on code. Some exceptions exist depending on what you consider trivial |
| 2025-04-28 09:03:49 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/crunkvuyNAgcnoaGKHVPavQw/HhaisemMfmk (5 lines) |
| 2025-04-28 09:03:47 +0200 | <haskellbridge> | <hellwolf> anyhow, not going to far, |
| 2025-04-28 09:03:45 +0200 | <haskellbridge> | <hellwolf> I actually don't have a clue what qualifies aslogic in the first place... I guess, something to do with formal way of describing"equality"? |
| 2025-04-28 09:03:36 +0200 | ChanServ | +v haskellbridge |
| 2025-04-28 09:03:36 +0200 | <haskellbridge> | <Bowuigi> As to which logics specifically, it actually depends on the features the type system has. Haven't read much on categorical logic yet but AFAIU you can use toposes to model dependently typed systems |
| 2025-04-28 09:03:36 +0200 | <haskellbridge> | <Bowuigi> Oh, mainstream here means popular, in a sense |
| 2025-04-28 09:03:36 +0200 | <haskellbridge> | <hellwolf> "less mainstream logics" |
| 2025-04-28 09:03:36 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) hackager |
| 2025-04-28 09:03:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 09:00:42 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-04-28 09:00:03 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-28 08:57:59 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-04-28 08:55:47 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk |
| 2025-04-28 08:55:41 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-28 08:51:39 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-04-28 08:50:29 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-04-28 08:48:18 +0200 | halloy3041 | (~halloy304@2001:569:76fd:b00:ada3:3d53:48e5:4f37) |
| 2025-04-28 08:44:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-28 08:34:23 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 08:29:55 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2025-04-28 08:27:18 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) |
| 2025-04-28 08:24:51 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 08:24:34 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2025-04-28 08:22:48 +0200 | chele | (~chele@user/chele) chele |
| 2025-04-28 08:22:35 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-28 08:20:40 +0200 | <Axman6> | I kind of wish there were better options these days, I'm sure there must be. There was some really cool work that went into the cborg and serialise packages to make it fast but it's specific to CBOR |
| 2025-04-28 08:18:13 +0200 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 276 seconds) |
| 2025-04-28 08:15:01 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2025-04-28 08:14:25 +0200 | <jco> | geekosaur: Thanks a lot. |
| 2025-04-28 08:13:16 +0200 | <lambdabot> | https://hackage.haskell.org/package/cereal |
| 2025-04-28 08:13:16 +0200 | <geekosaur> | @hackage cereal |
| 2025-04-28 08:13:12 +0200 | <lambdabot> | https://hackage.haskell.org/package/binary |