Newest at the top
2024-10-09 16:18:50 +0200 | vektor | (~vektor@IP-149249145126.pools.medianet-world.de) |
2024-10-09 16:17:25 +0200 | simendsjo | (~user@79.161.5.185) (Ping timeout: 248 seconds) |
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. |