Newest at the top
| 2024-10-09 16:16:42 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-10-09 16:07:06 +0200 | Batzy_ | (~quassel@user/batzy) (Ping timeout: 246 seconds) |
| 2024-10-09 16:06:55 +0200 | codaraxis | (~codaraxis@user/codaraxis) Codaraxis |
| 2024-10-09 16:04:20 +0200 | Batzy | (~quassel@user/batzy) Batzy |
| 2024-10-09 15:54:20 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-09 15:49:58 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2024-10-09 15:47:43 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-09 15:46:52 +0200 | petrichor | (~znc-user@user/petrichor) petrichor |
| 2024-10-09 15:46:02 +0200 | euleritian | (~euleritia@dynamic-176-006-139-018.176.6.pool.telefonica.de) |
| 2024-10-09 15:45:41 +0200 | <kuribas> | But you don't want to have too much complexity in the types. |
| 2024-10-09 15:45:34 +0200 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-10-09 15:45:27 +0200 | <kuribas> | complex types don't necessarily mean a lot of type level debugging IMO. |
| 2024-10-09 15:44:50 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-10-09 15:44:26 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) alexherbo2 |
| 2024-10-09 15:43:17 +0200 | alexherbo2 | (~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-09 15:29:56 +0200 | identity | (~identity@user/ZharMeny) identity |
| 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. |