Newest at the top
| 2025-12-11 17:08:36 +0100 | <kuribas> | Due to bottom. |
| 2025-12-11 17:08:30 +0100 | <kuribas> | haskell doesn't really have "proofs". |
| 2025-12-11 17:07:39 +0100 | <haskellbridge> | <matti palli> and it’s simultaneously the dictionary which contains the code, afaiu |
| 2025-12-11 17:06:46 +0100 | <haskellbridge> | <matti palli> yeah, and the right instance is the proof |
| 2025-12-11 17:06:05 +0100 | <kuribas> | You don't emit a "proof", the type inference does a proof search to find the right instance. |
| 2025-12-11 17:05:30 +0100 | <haskellbridge> | <matti palli> that’s how the typechecker works, you solve constraint by emitting a “proof” that the constraint holds, and that contains the dictionary which contains the code |
| 2025-12-11 17:05:30 +0100 | yin | (~zero@user/zero) zero |
| 2025-12-11 17:05:26 +0100 | <kuribas> | And the point is that the hole is not just "an error", but allows you to fill in the rest of the program, while leave out details. |
| 2025-12-11 17:05:15 +0100 | yin | (~zero@user/zero) (Remote host closed the connection) |
| 2025-12-11 17:04:40 +0100 | <kuribas> | constraints are just implicits. |
| 2025-12-11 17:04:17 +0100 | <kuribas> | How are constraints "generating code"? |
| 2025-12-11 17:03:47 +0100 | Axman6 | (~Axman6@user/axman6) (Remote host closed the connection) |
| 2025-12-11 17:03:37 +0100 | <haskellbridge> | <matti palli> Allowing missing constraints is a bit problematic, since constraints is how we generate code. Indeed, holes are just an “undefined variable” error with a fancy message |
| 2025-12-11 17:02:49 +0100 | <merijn> | kuribas: You could try and fix it. I hacked that flag together when I barely knew haskell :p |
| 2025-12-11 17:00:24 +0100 | deptype | (~deptype@2406:b400:3a:9d2f:fd44:bbca:9ef1:b046) (Read error: Connection reset by peer) |
| 2025-12-11 17:00:01 +0100 | deptype_ | (~deptype@2406:b400:3a:9d2f:fd44:bbca:9ef1:b046) (Quit: Leaving) |
| 2025-12-11 16:53:08 +0100 | <kuribas> | And if you allow holes, why not allow missing constraints on those holes? |
| 2025-12-11 16:52:35 +0100 | <kuribas> | indeed! |
| 2025-12-11 16:52:10 +0100 | <merijn> | I saw -fdefer-type-errprs and I was like "man, that's useless. But also, it would be nice if I could run my code while it still had holes" |
| 2025-12-11 16:52:10 +0100 | <kuribas> | "Typed holes are a powerful feature in GHC inspired by Agda. But what are typed holes, and how do they help us write code? " |
| 2025-12-11 16:51:46 +0100 | <kuribas> | Well, the hole thingy came from proof assistants, no? |
| 2025-12-11 16:51:37 +0100 | <kuribas> | ah right :) |
| 2025-12-11 16:51:23 +0100 | <merijn> | It was I, Dio! |
| 2025-12-11 16:51:19 +0100 | <merijn> | kuribas: It didn't come from proof assistants |
| 2025-12-11 16:50:59 +0100 | <kuribas> | I don't have an easy example right now. |
| 2025-12-11 16:50:43 +0100 | <merijn> | Can you pastebin an example? |
| 2025-12-11 16:50:22 +0100 | <kuribas> | If a0 is the type of a hole, I don't want an error. |
| 2025-12-11 16:49:32 +0100 | <merijn> | holes don't help you there |
| 2025-12-11 16:49:26 +0100 | <merijn> | kuribas: The ambiguous variable *is* an error and it cannot be solved |
| 2025-12-11 16:49:02 +0100 | <kuribas> | proof |
| 2025-12-11 16:49:00 +0100 | <kuribas> | merijn: it came from profo assistants, no? |
| 2025-12-11 16:47:39 +0100 | tromp | (~textual@2001:1c00:3487:1b00:dd4:56d:fd02:60e2) |
| 2025-12-11 16:47:32 +0100 | <kuribas> | tomsmeding: A feature request I have been missing for 10 years or so :) |
| 2025-12-11 16:46:55 +0100 | <merijn> | (I missed the context, btw) |
| 2025-12-11 16:46:39 +0100 | <tomsmeding> | which is a completely different thing, namely a feature request instead of a bug report |
| 2025-12-11 16:46:29 +0100 | <tomsmeding> | well that turns this from "GHC's diagnostics are bad" into "-fdefer-typed-holes is not strong enough" |
| 2025-12-11 16:46:17 +0100 | <merijn> | -fdefer-typed-holes is the greatest flag ever and whoever implemented it was a visionary genius |
| 2025-12-11 16:46:02 +0100 | <merijn> | Of course you do |
| 2025-12-11 16:43:12 +0100 | <kuribas> | right :) |
| 2025-12-11 16:42:54 +0100 | <tomsmeding> | kuribas: the context "I want to work with -fdefer-typed-holes" is very important there :p |
| 2025-12-11 16:42:12 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-12-11 16:26:04 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) (Ping timeout: 246 seconds) |
| 2025-12-11 16:24:54 +0100 | Enrico63 | (~Enrico63@host-212-171-79-170.retail.telecomitalia.it) (Quit: Client closed) |
| 2025-12-11 16:24:28 +0100 | Square | (~Square4@user/square) Square |
| 2025-12-11 16:23:42 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-12-11 16:21:00 +0100 | deptype_ | (~deptype@2406:b400:3a:9d2f:fd44:bbca:9ef1:b046) |
| 2025-12-11 16:19:36 +0100 | fp | (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 252 seconds) |
| 2025-12-11 16:17:13 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds) |
| 2025-12-11 16:17:01 +0100 | tromp | (~textual@2001:1c00:3487:1b00:dd4:56d:fd02:60e2) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-12-11 16:16:31 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 240 seconds) |