Newest at the top
| 2025-04-28 09:33:05 +0200 | img | (~img@user/img) img |
| 2025-04-28 09:32:53 +0200 | akegalj | (~akegalj@144-188.dsl.iskon.hr) |
| 2025-04-28 09:31:45 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-04-28 09:28:55 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 09:23:12 +0200 | akegalj | (~akegalj@83-131-242-128.adsl.net.t-com.hr) (Ping timeout: 252 seconds) |
| 2025-04-28 09:23:05 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-04-28 09:22:43 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving) |
| 2025-04-28 09:22:34 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 2025-04-28 09:22:08 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 09:21:51 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 09:21:42 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-04-28 09:19:10 +0200 | <c_wraith> | length-indexed vectors are very easy to understand, but actually quite awkward to use. Like... filter can have a ton of different types, and it turns out all of them are a pain to work with. |
| 2025-04-28 09:17:29 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 245 seconds) |
| 2025-04-28 09:11:51 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) |
| 2025-04-28 09:09:07 +0200 | <haskellbridge> | <hellwolf> Also, I think length-indexed vector is the most practical everyday stuff DT should sell hard. Like selling ADT and pattern matching to mainstream languages. |
| 2025-04-28 09:07:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 09:07:34 +0200 | <haskellbridge> | <hellwolf> But rust also shows that some technique of better managing runtime system behaviour can be appreciated. Do you consider DT and LinearTypes are orthogonal to each other as researches? |
| 2025-04-28 09:07:33 +0200 | <haskellbridge> | <geekosaur> oh, they weren't, you were just catching up while the bot was down (system upgrade) |
| 2025-04-28 09:07:29 +0200 | akegalj | (~akegalj@83-131-242-128.adsl.net.t-com.hr) akegalj |
| 2025-04-28 09:05:40 +0200 | <haskellbridge> | <hellwolf> Heh, yea, selling DT is hard because people are lazy and handwave the proofs a way by doing it on paper or simply yolo |
| 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 |