2024/10/09

Newest at the top

2024-10-09 16:17:25 +0200simendsjo(~user@79.161.5.185) (Ping timeout: 248 seconds)
2024-10-09 16:16:42 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-10-09 16:07:06 +0200Batzy_(~quassel@user/batzy) (Ping timeout: 246 seconds)
2024-10-09 16:06:55 +0200codaraxis(~codaraxis@user/codaraxis) Codaraxis
2024-10-09 16:04:20 +0200Batzy(~quassel@user/batzy) Batzy
2024-10-09 15:54:20 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2024-10-09 15:49:58 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Excess Flood)
2024-10-09 15:47:43 +0200alexherbo2(~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) (Remote host closed the connection)
2024-10-09 15:46:52 +0200petrichor(~znc-user@user/petrichor) petrichor
2024-10-09 15:46:02 +0200euleritian(~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 +0200petrichor(~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 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2024-10-09 15:44:26 +0200alexherbo2(~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) alexherbo2
2024-10-09 15:43:17 +0200alexherbo2(~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) (Remote host closed the connection)
2024-10-09 15:29:56 +0200identity(~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 +0200alexherbo2(~alexherbo@2a02-8440-330a-55b8-7487-6396-e5cd-7eb2.rev.sfr.net) alexherbo2
2024-10-09 15:17:04 +0200DigitteknohippieDigit
2024-10-09 15:13:13 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-10-09 15:11:17 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds)
2024-10-09 15:07:05 +0200gorignak(~gorignak@user/gorignak) gorignak
2024-10-09 15:06:34 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-10-09 15:04:15 +0200Digit(~user@user/digit) (Ping timeout: 265 seconds)
2024-10-09 15:03:59 +0200Digitteknohippie(~user@user/digit) Digit
2024-10-09 15:03:55 +0200weary-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").