Logs: liberachat/#haskell
| 2026-01-03 17:32:40 | <monochrom> | I work backwards. If the impossible happens, do I have a plan B for the program to continue working (is it even required?), or should it just crash and I just fix the bug and move on? |
| 2026-01-03 17:33:45 | <EvanR> | Milan_Vanca, true, it is pointless to use a Maybe, pattern match and then throw an error. Unless you want to change the error message in case the impossible happens. The failure case is impossible right? |
| 2026-01-03 17:34:10 | <Milan_Vanca> | monochrom: This is great idea! I should ask this question more often when programming. |
| 2026-01-03 17:34:39 | <EvanR> | sometimes Nothing would be impossible |
| 2026-01-03 17:34:59 | <EvanR> | but it's important to not delude yourself... which is why you need proof |
| 2026-01-03 17:35:05 | <EvanR> | not a runtime test |
| 2026-01-03 17:35:07 | <Milan_Vanca> | EvanR: Yeah it should be, I try to implement MD5 which pads messages to modulo 512. Then computes whole blocks. So it should not error as it would imply I padded wrong. |
| 2026-01-03 17:35:17 | <monochrom> | But in your example, I don't even have that dichotomy. Instead of pre-padding then expect well-padded, just go ahead consume the chunk and pad the last chunk when found. |
| 2026-01-03 17:36:00 | <EvanR> | sometimes the algorithm can be made more efficient at the expense of requiring a meticulous proof that some situations can't happen, not covered by the type system |
| 2026-01-03 17:36:02 | <Milan_Vanca> | monochrom: Yeah agree this is nice solution, but MD5 says there must be padding. As operation is not defined on blocks of different length that 512 |
| 2026-01-03 17:36:08 | <monochrom> | s/consume the chunk/consume the chunks/ |
| 2026-01-03 17:36:51 | <EvanR> | it sounds scary until you realize every line of dynamically typed code is using this mentality |
| 2026-01-03 17:37:02 | <EvanR> | and somehow runs the world |
| 2026-01-03 17:37:25 | <Leary> | The problem with "this case is impossible anyway" is that you can be wrong, or code elsewhere can change that breaks it. When that happens, you will really want to see a runtime error that points precisely to the code that threw it, not a "*** Exception: Maybe.fromJust: Nothing" which could have come from anywhere. |
| 2026-01-03 17:37:28 | <Milan_Vanca> | EvanR: This idea of proofing is interesting, but I am not proficient at math and cannot even imagine how could I proof that something will or won't happen. However I have a strong gut feeling :D |
| 2026-01-03 17:38:22 | <EvanR> | since you're dealing with a very specific algorithm, it is possible and somebody has probably done it 1000 times |
| 2026-01-03 17:38:31 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2026-01-03 17:38:36 | <Milan_Vanca> | EvanR: :( So true... My day to day job is with these dynamic languages. |
| 2026-01-03 17:38:41 | <EvanR> | just trace backwards where this nothing might have come from and see that it is ... nowhere |
| 2026-01-03 17:39:35 | <EvanR> | also Leary is also right |
| 2026-01-03 17:39:51 | <Milan_Vanca> | Leary: Oookey I can see that.. I will try to document "imposible" cases |
| 2026-01-03 17:40:08 | <EvanR> | GHC has crashed on my with "the impossible happened" xD |
| 2026-01-03 17:40:15 | <Leary> | Milan_Vanca: I would not pad the list, but parse fixed-size chunks from the list into a (dense) bespoke type with your invariant. That type would then have fast, safe operations written in terms of unsafe or partial functions. |
| 2026-01-03 17:40:16 | <EvanR> | very sad |
| 2026-01-03 17:40:40 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 2026-01-03 17:41:55 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 17:42:03 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2026-01-03 17:42:03 | ljdarj1 | is now known as ljdarj |
| 2026-01-03 17:42:08 | <Milan_Vanca> | EvanR: Was the error *** Exception: Prelude.head: empty list ?? :D Just kidding :D |
| 2026-01-03 17:42:27 | <Milan_Vanca> | EvanR: SO internal GHC error? |
| 2026-01-03 17:42:28 | <EvanR> | ... no |
| 2026-01-03 17:42:45 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 17:43:09 | <EvanR> | this was very rare which is good |
| 2026-01-03 17:43:27 | → | merijn joins (~merijn@62.45.136.136) |
| 2026-01-03 17:43:32 | <EvanR> | but shows how hard it can be to verify code even when the language forces you to think about the cases |
| 2026-01-03 17:44:46 | <Milan_Vanca> | Leary: Hmm not sure if I want to rewrite my algo now.. But I might try it later when I am bored. So basically you would "pad" only when last block is not 512 and in moment you parse it to some datatype? |
| 2026-01-03 17:46:38 | <Leary> | Yes, something like `newtype Chunk512 = UnsafeMkChunk512 Text; parseChunk512 :: [Char] -> Maybe (Chunk512, [Char])`. |
| 2026-01-03 17:47:55 | × | merijn quits (~merijn@62.45.136.136) (Ping timeout: 240 seconds) |
| 2026-01-03 17:48:39 | <EvanR> | then internal code only uses UnsafeMkChunk512 when it is definitely the case that the chunk has that length. Parsers bear a lot of burden |
| 2026-01-03 17:49:22 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 17:49:35 | <EvanR> | for extra paranoia don't export UnsafeMkChunk512 at least in a public API |
| 2026-01-03 17:50:16 | <Leary> | That's not extra paranoia, that's the basic level. |
| 2026-01-03 17:52:16 | <EvanR> | who would use UnsafeMkChunk512 irresponsibly when it says Unsafe all over it?? xD |
| 2026-01-03 17:54:08 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-03 17:56:21 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 17:57:00 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 17:57:15 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 2026-01-03 18:00:56 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 18:01:50 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 18:05:17 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 18:05:41 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-01-03 18:08:03 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2026-01-03 18:09:40 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-03 18:12:52 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 18:17:43 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-03 18:18:38 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 18:20:16 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 18:28:36 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 18:29:57 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-01-03 18:32:14 | → | Inline joins (~User@cgn-195-14-221-74.nc.de) |
| 2026-01-03 18:33:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2026-01-03 18:36:58 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 18:37:55 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 18:38:17 | × | Digit quits (~user@user/digit) (Remote host closed the connection) |
| 2026-01-03 18:43:51 | → | Digit joins (~user@user/digit) |
| 2026-01-03 18:44:23 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 18:46:43 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 18:47:54 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 18:49:23 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-03 18:51:42 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 18:52:59 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 19:00:10 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 19:03:08 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 19:03:56 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 19:04:58 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-03 19:06:23 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2026-01-03 19:09:08 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 19:09:51 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 19:12:46 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 19:13:48 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 19:13:58 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 19:18:40 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-03 19:23:11 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 19:23:50 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 19:28:13 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 19:28:15 | × | aman quits (~aman@user/aman) (Ping timeout: 240 seconds) |
| 2026-01-03 19:28:55 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 19:29:36 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-03 19:35:19 | × | Inline quits (~User@cgn-195-14-221-74.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/) |
| 2026-01-03 19:35:21 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 19:35:25 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 264 seconds) |
| 2026-01-03 19:35:45 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2026-01-03 19:35:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-03 19:36:35 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
| 2026-01-03 19:37:02 | × | wennefer0 quits (~wennefer0@user/wennefer0) (Client Quit) |
| 2026-01-03 19:37:04 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2026-01-03 19:39:34 | → | wennefer0 joins (~wennefer0@user/wennefer0) |
| 2026-01-03 19:40:42 | → | pebble joins (~pebble@212.104.118.193) |
| 2026-01-03 19:40:46 | → | Inline joins (~User@cgn-195-14-221-74.nc.de) |
| 2026-01-03 19:43:40 | × | mangoiv quits (~mangoiv@user/mangoiv) (Quit: The Lounge - https://thelounge.chat) |
All times are in UTC.