Logs: freenode/#haskell
| 2021-04-14 09:21:01 | → | Sorna joins (~Sornaensi@077213203030.dynamic.telenor.dk) |
| 2021-04-14 09:22:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-14 09:23:51 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 09:24:04 | × | Sornaensis quits (~Sornaensi@79.142.232.102) (Ping timeout: 252 seconds) |
| 2021-04-14 09:27:01 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 2021-04-14 09:28:53 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-04-14 09:29:57 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 09:30:36 | <gnumonic> | So I'd like to use type level Peano numbers with the singletons library. I don't think that the library itself provides that and I'm pretty sure I shouldn't use typelits, so is there some preferred library that interfaces with singletons? Or does everyone just roll their own and prove axioms of number theory as they need them? :p |
| 2021-04-14 09:32:18 | → | geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) |
| 2021-04-14 09:33:23 | × | zaquest quits (~notzaques@5.128.210.178) (Quit: Leaving) |
| 2021-04-14 09:34:57 | → | zaquest joins (~notzaques@5.128.210.178) |
| 2021-04-14 09:34:58 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-04-14 09:35:27 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 09:37:54 | <__monty__> | That's not an unlikely scenario, given haskell's not really suited to theorem proving anyway. |
| 2021-04-14 09:40:33 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-04-14 09:41:16 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 09:41:23 | <gnumonic> | Bearing in mind that I know nothing about how TypeLits are implemented at all, is there some reason GHC's typechecker can't prove simple facts about typelevel numbers? |
| 2021-04-14 09:41:55 | × | Katarushisu quits (~Katarushi@cpc152083-finc20-2-0-cust170.4-2.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 2021-04-14 09:42:46 | × | BosonCollider quits (~olofs@90-227-86-119-no542.tbcn.telia.com) (Ping timeout: 252 seconds) |
| 2021-04-14 09:42:54 | → | DavidEichmann joins (~david@47.27.93.209.dyn.plus.net) |
| 2021-04-14 09:43:31 | <__monty__> | No, it's just not a popular pursuit. |
| 2021-04-14 09:43:34 | <__monty__> | @where hasochism |
| 2021-04-14 09:43:35 | <lambdabot> | I know nothing about hasochism. |
| 2021-04-14 09:43:41 | × | LKoen quits (~LKoen@65.250.88.92.rev.sfr.net) (Remote host closed the connection) |
| 2021-04-14 09:43:43 | × | shutdown_-h_now quits (~arjan@2001:1c06:2d0b:2312:d1b3:8e6:fe83:6a87) (Ping timeout: 260 seconds) |
| 2021-04-14 09:43:47 | × | seanparsons quits (~sean@cpc145088-gill21-2-0-cust281.20-1.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2021-04-14 09:43:57 | <DigitalKiwi> | dibblego gave me some peano exercises maybe he has an idea |
| 2021-04-14 09:43:58 | × | Foritus quits (~buggery@cpc91316-watf11-2-0-cust68.15-2.cable.virginm.net) (Ping timeout: 240 seconds) |
| 2021-04-14 09:44:00 | <kuribas> | I don't get why people think haskell is about proving business logic in types. |
| 2021-04-14 09:44:18 | × | Tesseraction quits (~Tesseract@unaffiliated/tesseraction) (Ping timeout: 240 seconds) |
| 2021-04-14 09:44:27 | <__monty__> | This paper shows what's possible and how inconvenient it is compared to a language with support for such things, https://dl.acm.org/doi/abs/10.1145/2578854.2503786 |
| 2021-04-14 09:44:58 | <kuribas> | I see haskell more like, it's a language with nice abstractions, and a type system that is expressive enough to express and guard those abstractions. |
| 2021-04-14 09:45:13 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2021-04-14 09:45:28 | <__monty__> | kuribas: You're extrapolating. gnumonic is probably just interested in this. No harm checking it out. |
| 2021-04-14 09:46:08 | <__monty__> | gnumonic: Codewares.io has a couple fun type-level hackery challenges. |
| 2021-04-14 09:46:13 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-04-14 09:46:27 | <kuribas> | __monty__: I am not saying you shouldn't have fun with it. |
| 2021-04-14 09:46:32 | × | nut quits (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 2021-04-14 09:46:52 | → | Katarushisu joins (~Katarushi@cpc152083-finc20-2-0-cust170.4-2.cable.virginm.net) |
| 2021-04-14 09:46:58 | <gnumonic> | monty: mkay I'll check it out, thank you. And yeah I'm just sort of experimenting with what I can do at the type level. |
| 2021-04-14 09:47:21 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 09:48:03 | → | Foritus joins (~buggery@cpc91316-watf11-2-0-cust68.15-2.cable.virginm.net) |
| 2021-04-14 09:48:23 | <kuribas> | __monty__: I am just saying you probably make your life harder if you go that route. |
| 2021-04-14 09:48:24 | <DigitalKiwi> | kuribas: the real mad lads are the people that write their business logic in hedgehog |
| 2021-04-14 09:48:52 | <__monty__> | DigitalKiwi: Surely you mean describe their business logic to hedgehog and have it infer the implementation? : ) |
| 2021-04-14 09:49:13 | <DigitalKiwi> | https://clrnd.com.ar/posts/2017-04-21-the-water-jug-problem-in-hedgehog.html idk :D |
| 2021-04-14 09:49:15 | → | seanparsons joins (~sean@cpc145088-gill21-2-0-cust281.20-1.cable.virginm.net) |
| 2021-04-14 09:49:34 | → | Tesseraction joins (~Tesseract@unaffiliated/tesseraction) |
| 2021-04-14 09:51:58 | → | shutdown_-h_now joins (~arjan@2001:1c06:2d0b:2312:d1b3:8e6:fe83:6a87) |
| 2021-04-14 09:52:09 | <kuribas> | I've been wondering if there is a way to create tests for edge cases... |
| 2021-04-14 09:52:28 | <kuribas> | Like, you have some code, and you generate tests which will exercise all code paths. |
| 2021-04-14 09:52:38 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-14 09:53:00 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 09:53:23 | <__monty__> | I think maybe there's some FSM test machinery that does so? |
| 2021-04-14 09:54:05 | <__monty__> | The general problem sounds very Halting-y to me. |
| 2021-04-14 09:54:54 | <kuribas> | I had a bug in our compression algorithm which happened only in few cases. |
| 2021-04-14 09:55:05 | <kuribas> | Luckily we did a large scale test first. |
| 2021-04-14 09:55:08 | <DigitalKiwi> | smolcheck |
| 2021-04-14 09:55:43 | → | rdivyanshu joins (uid322626@gateway/web/irccloud.com/x-andoqpzjmzizoeoe) |
| 2021-04-14 09:55:47 | <kuribas> | https://github.com/burmanm/compression-int/issues/6 |
| 2021-04-14 09:55:48 | <DigitalKiwi> | kuribas: "large scale test" == "pushed to prod" ? |
| 2021-04-14 09:56:00 | <kuribas> | DigitalKiwi: before pushing to prod even! |
| 2021-04-14 09:56:03 | <maralorn> | kuribas: There is a difference between "proving your business logic" and using typelevel nats for good code. I e.g. am doing a lot of stuff mit matrices and tracking on the typelevel that their dimensions match seems not crazy to me at all. |
| 2021-04-14 09:56:16 | <DigitalKiwi> | kuribas: congrats you're a 10x dev |
| 2021-04-14 09:56:27 | <maralorn> | Although the constraints "(KnownNat n, KnownNat k, KnownNat (n * k), (n * k) ~ (k * n)) =>" are certainly not satisfying. |
| 2021-04-14 09:56:45 | <kuribas> | DigitalKiwi: not sure, it took us months testing and integrating the compression. |
| 2021-04-14 09:57:43 | <DigitalKiwi> | well if had gone to prod it would have likely become a feature |
| 2021-04-14 09:57:47 | <kuribas> | maralorn: my take is, avoid complicated types if you can, otherwise just use them :-) |
| 2021-04-14 09:58:08 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-14 09:58:10 | → | BosonCollider joins (~olofs@90-227-86-119-no542.tbcn.telia.com) |
| 2021-04-14 09:58:27 | <DigitalKiwi> | as in, it'd never get fixed, all future code would be aware of it, and require its existence |
| 2021-04-14 09:58:50 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 09:59:38 | <DigitalKiwi> | ...or not aware of it and be extra perplexing when it doesn't work :D |
| 2021-04-14 10:00:25 | <kuribas> | Or customers suddenly not making their quotas because of the change to compression... |
| 2021-04-14 10:01:22 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2021-04-14 10:04:00 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-14 10:04:40 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 10:05:12 | × | ubert quits (~Thunderbi@77.119.128.21.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
| 2021-04-14 10:07:13 | × | dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 240 seconds) |
| 2021-04-14 10:07:55 | → | idhugo__ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-04-14 10:09:50 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 2021-04-14 10:10:12 | × | idhugo_ quits (~idhugo@87-49-44-84-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 2021-04-14 10:10:18 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-04-14 10:10:32 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 10:10:44 | → | heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-04-14 10:15:12 | × | heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2021-04-14 10:15:46 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-14 10:16:04 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 10:18:14 | → | LKoen joins (~LKoen@65.250.88.92.rev.sfr.net) |
| 2021-04-14 10:21:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 2021-04-14 10:21:43 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 10:23:53 | × | geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 2021-04-14 10:27:19 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-14 10:27:34 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 10:28:26 | × | LKoen quits (~LKoen@65.250.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 2021-04-14 10:30:40 | × | fiedlr quits (~fiedlr@83.148.33.254) (Remote host closed the connection) |
| 2021-04-14 10:31:28 | → | proteusguy joins (~proteusgu@cm-58-10-209-239.revip7.asianet.co.th) |
| 2021-04-14 10:32:07 | × | __minoru__shirae quits (~shiraeesh@46.34.206.215) (Ping timeout: 265 seconds) |
| 2021-04-14 10:32:32 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-04-14 10:33:26 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
All times are in UTC.