Newest at the top
| 2024-10-09 15:24:45 +0200 | <kuribas> | And in idris you have nice ways to program with types, like typed holes. |
| 2024-10-09 15:19:58 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) alexherbo2 |
| 2024-10-09 15:17:04 +0200 | Digitteknohippie | Digit |
| 2024-10-09 15:13:13 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-09 15:11:17 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2024-10-09 15:07:05 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-09 15:06:34 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-10-09 15:04:15 +0200 | Digit | (~user@user/digit) (Ping timeout: 265 seconds) |
| 2024-10-09 15:03:59 +0200 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-10-09 15:03:55 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-09 14:53:33 +0200 | <kuribas> | I am happier with a type error, that I can disentangle, that a big stacktrace, which may not even have the answer. |
| 2024-10-09 14:53:08 +0200 | <dminuoso> | :-) |
| 2024-10-09 14:53:07 +0200 | <dminuoso> | You trade time spend in debugging.. for time spend in debugging. |
| 2024-10-09 14:53:01 +0200 | <kuribas> | But not everyone does, I know... |
| 2024-10-09 14:52:49 +0200 | <kuribas> | I am glad to take that trade-off. |
| 2024-10-09 14:52:49 +0200 | <dminuoso> | In Haskell anyway. |
| 2024-10-09 14:52:27 +0200 | <dminuoso> | All that perceived time saved in debugging, is wasted again troubleshooting illegible type errors, or fighting strange type mismatches because there's an extra type tag here and there. |
| 2024-10-09 14:52:06 +0200 | <kuribas> | It's much less of a risk in a production environment. |
| 2024-10-09 14:51:55 +0200 | <kuribas> | Well, one justification is the maturity of the compiler and the ecosystem. |
| 2024-10-09 14:51:39 +0200 | <dminuoso> | To the point where I think its very hard to justify it. |
| 2024-10-09 14:51:29 +0200 | <dminuoso> | Sure they should. This is not an argument about whether dependent types are good, but in Haskell they just overcomplicate interfaces. |
| 2024-10-09 14:51:19 +0200 | <kuribas> | It's so much more ergonomic on idris. |
| 2024-10-09 14:51:10 +0200 | <kuribas> | they should :) |
| 2024-10-09 14:51:02 +0200 | <dminuoso> | And yet people rather pick up Idris when they want dependent types. :-) |
| 2024-10-09 14:50:48 +0200 | <kuribas> | Type level strings, lists, Nats... |
| 2024-10-09 14:50:40 +0200 | <kuribas> | It emulates it. |
| 2024-10-09 14:50:22 +0200 | <dminuoso> | You dont need a dependent type system, which Haskell does not even have. |
| 2024-10-09 14:49:59 +0200 | <kuribas> | ? |
| 2024-10-09 14:49:51 +0200 | <kuribas> | dminuoso: sure, but how is that different from a dependent type. |
| 2024-10-09 14:49:30 +0200 | <kuribas> | In an adhoc way I mean. |
| 2024-10-09 14:49:27 +0200 | <dminuoso> | Like I said, I think if we were able to tag/add metadata to data types and constructors, I think that would be much more useful and easier to work with. |
| 2024-10-09 14:49:17 +0200 | <kuribas> | Not production outages, just a lot of work debugging code. |
| 2024-10-09 14:48:54 +0200 | <kuribas> | Or you have a constraint (HasColumn "foobar"). |
| 2024-10-09 14:48:50 +0200 | <dminuoso> | I'm slowly starting to wonder whether some of those "lets encode it into the type system for safety" is solving problems as an excuse to just explore some funky ideas, rather than it stemming from a series of production outages due to some impedance mismatching. |
| 2024-10-09 14:48:35 +0200 | <kuribas> | Yeah, but that's the idea. |
| 2024-10-09 14:48:02 +0200 | <dminuoso> | And those type level lists will propagate through your entire code, or you have to erase them. |
| 2024-10-09 14:46:22 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-10-09 14:45:25 +0200 | <kuribas> | dminuoso: I don't mean it's very ergonomic, but it's possible with type level lists. |
| 2024-10-09 14:44:44 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-b033-f4f9-ddc1-450a.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-09 14:41:33 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-b033-f4f9-ddc1-450a.rev.sfr.net) alexherbo2 |
| 2024-10-09 14:41:05 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-b599-5e37-bcaf-ea15.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-09 14:37:11 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-b599-5e37-bcaf-ea15.rev.sfr.net) alexherbo2 |
| 2024-10-09 14:36:28 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-5144-54d3-aa36-e8c9.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-09 14:33:39 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-10-09 14:32:03 +0200 | codaraxis | (~codaraxis@user/codaraxis) (Ping timeout: 244 seconds) |
| 2024-10-09 14:27:32 +0200 | mari-estel | (~mari-este@2a02:3032:30b:ae0c:216:3eff:fe65:4eef) (Quit: errands) |
| 2024-10-09 14:26:35 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-5144-54d3-aa36-e8c9.rev.sfr.net) alexherbo2 |
| 2024-10-09 14:26:15 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-5144-54d3-aa36-e8c9.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-09 14:18:55 +0200 | <hseg> | going through the botan devlog, I see reference to a crypto-schemes repo, but can't find it anywhere atm. Anyone know where it vanished off to? Also, I suppose the "cryptographic typeclasses" refered to are in the various Botan.*.Class modules? |
| 2024-10-09 14:17:28 +0200 | billchenchina- | (~billchenc@103.152.35.21) billchenchina |