Logs: liberachat/#haskell
| 2025-12-11 15:51:19 | <merijn> | kuribas: It didn't come from proof assistants |
| 2025-12-11 15:51:23 | <merijn> | It was I, Dio! |
| 2025-12-11 15:51:37 | <kuribas> | ah right :) |
| 2025-12-11 15:51:46 | <kuribas> | Well, the hole thingy came from proof assistants, no? |
| 2025-12-11 15:52:10 | <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 15:52:10 | <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 15:52:35 | <kuribas> | indeed! |
| 2025-12-11 15:53:08 | <kuribas> | And if you allow holes, why not allow missing constraints on those holes? |
| 2025-12-11 16:00:01 | × | deptype_ quits (~deptype@2406:b400:3a:9d2f:fd44:bbca:9ef1:b046) (Quit: Leaving) |
| 2025-12-11 16:00:24 | × | deptype quits (~deptype@2406:b400:3a:9d2f:fd44:bbca:9ef1:b046) (Read error: Connection reset by peer) |
| 2025-12-11 16:02:49 | <merijn> | kuribas: You could try and fix it. I hacked that flag together when I barely knew haskell :p |
| 2025-12-11 16:03:37 | <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 16:03:47 | × | Axman6 quits (~Axman6@user/axman6) (Remote host closed the connection) |
| 2025-12-11 16:04:17 | <kuribas> | How are constraints "generating code"? |
| 2025-12-11 16:04:40 | <kuribas> | constraints are just implicits. |
| 2025-12-11 16:05:15 | × | yin quits (~zero@user/zero) (Remote host closed the connection) |
| 2025-12-11 16:05:26 | <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 16:05:30 | → | yin joins (~zero@user/zero) |
| 2025-12-11 16:05:30 | <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 16:06:05 | <kuribas> | You don't emit a "proof", the type inference does a proof search to find the right instance. |
| 2025-12-11 16:06:46 | <haskellbridge> | <matti palli> yeah, and the right instance is the proof |
| 2025-12-11 16:07:39 | <haskellbridge> | <matti palli> and it’s simultaneously the dictionary which contains the code, afaiu |
| 2025-12-11 16:08:30 | <kuribas> | haskell doesn't really have "proofs". |
| 2025-12-11 16:08:36 | <kuribas> | Due to bottom. |
| 2025-12-11 16:09:33 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 2025-12-11 16:10:09 | <kuribas> | Even so, proof assistants like agda and idris allow you to have holes as proofs. |
| 2025-12-11 16:10:15 | <kuribas> | Then they are just "assumptions". |
| 2025-12-11 16:10:15 | <lucabtz> | i remember a video of tsoding on youtube referring to implementing instances like the functor instance as "proving" something is a functor |
| 2025-12-11 16:10:15 | <haskellbridge> | <matti palli> yeah sure, you can emit a “proof” that just contains error |
| 2025-12-11 16:10:58 | <haskellbridge> | <matti palli> what I mean is that you solve the constraint and emit a witness that is the dictionary |
| 2025-12-11 16:11:17 | <kuribas> | That's how large proofs are done, you treat some parts as "assumptions", and proof them later. Or they turn out to be false, and you have to abort the whole proof (or find another proof). |
| 2025-12-11 16:12:12 | <haskellbridge> | <matti palli> sure, you can do that with undefined or error as well. but then you have the issue of ambiguous type variables, as you’ve encountered |
| 2025-12-11 16:12:31 | <tomsmeding> | is the problem here that you want to be sure that the unsolvable constraint is _purely_ due to a typed hole? |
| 2025-12-11 16:12:43 | <kuribas> | yeah |
| 2025-12-11 16:12:56 | <tomsmeding> | because instantiating a typeclass dictionary argument with an error term is very much expressible in Core, at least |
| 2025-12-11 16:13:22 | <tomsmeding> | it's just hard to draw the line between an arbitrary unsolved constraint and one that is "intuitively" part of the hole |
| 2025-12-11 16:13:43 | <tomsmeding> | and replacing arbitrary unsolved constraints with errors (and thus not stopping compilation for them) is rather against the idea of -fdefer-typed-holes |
| 2025-12-11 16:13:54 | <kuribas> | tomsmeding: isn't that use a graph on the typeclass dependencies? |
| 2025-12-11 16:14:16 | <tomsmeding> | perhaps, but I expect you're going to have a lot of spurious dependencies |
| 2025-12-11 16:14:23 | <tomsmeding> | also, the graph needs to include type variables |
| 2025-12-11 16:16:03 | <tomsmeding> | one thing that's probably implementable (I say without having ever looked at the GHC typechecker) is instantiating any ambiguous unification variable with a special type such that unsolved constraints that mention that special type get magically solved with an error |
| 2025-12-11 16:16:13 | <tomsmeding> | but that would be -fdefer-type-errors behaviour, not -fdefer-typed-holes |
| 2025-12-11 16:16:59 | <kuribas> | tomsmeding: the hole gives rise to a type variable, which can be either unified with something, or remains "ambiguous". In the latter case you can trace which type classes depend on the ambiguous variable, no? |
| 2025-12-11 16:17:07 | <haskellbridge> | <matti palli> You could get there by just giving a more specific type to the hole "_ :: blah", resolving the ambiguity |
| 2025-12-11 16:17:12 | <tomsmeding> | "the hole gives rise to a type variable" is not a thing |
| 2025-12-11 16:17:30 | <tomsmeding> | every term gives rise to potentially multiple unification variables, and a lot of those are equal |
| 2025-12-11 16:17:44 | <tomsmeding> | you can track dependencies of everything, but that likely slows down type checking significantly |
| 2025-12-11 16:18:31 | <tomsmeding> | if the type of the hole itself is the ambiguous type variable, then sure, it clearly "gives rise" to it (though even then, there's not at all necessarily a causal relationship!) |
| 2025-12-11 16:19:04 | <tomsmeding> | what if you have `read undefined + _`; that has an ambiguous type, but is that type "given rise to" by the hole? |
| 2025-12-11 16:19:08 | <tomsmeding> | how would GHC decide? |
| 2025-12-11 16:19:10 | <haskellbridge> | <matti palli> tomsmeding: technically the type of the hole starts of as a type variable, but is then quickly unified with variables that exist in scope. |
| 2025-12-11 16:19:16 | <tomsmeding> | right |
| 2025-12-11 16:19:29 | <haskellbridge> | <matti palli> it never comes up with a completely new variable |
| 2025-12-11 16:20:01 | <tomsmeding> | well, if the type of the hole starts off as a type variable, that variable was completely new, wasn't it? ;) |
| 2025-12-11 16:20:34 | <haskellbridge> | <matti palli> well yes but it shouldn’t escape the scope (you’d get the skolem has escaped warning haha) |
| 2025-12-11 16:20:47 | <tomsmeding> | but kuribas what do you think about my little example? |
| 2025-12-11 16:21:30 | <haskellbridge> | <matti palli> but yeah you are completely right, the ambiguity isn’t introduced by the hole, it’s just that the hole isn’t resolving any ambiguity (nor should it!) |
| 2025-12-11 16:21:59 | <tomsmeding> | you can try to deduce that fixing the type of the whole would resolve the ambiguity, perhaps |
| 2025-12-11 16:22:16 | <tomsmeding> | but I'm not sure that characterises precisely what kuribas intends |
| 2025-12-11 16:22:28 | <tomsmeding> | and also that feels like fragile code, especially in GHC where you have zonking |
| 2025-12-11 16:22:37 | <kuribas> | tomsmeding: (read undefined :: Read a => a), after + it becomes (Read a, Num a), and (_ :: ?hole1), so after unifying with the hole, you have (Read ?hole, Num ?hole) => ?hole |
| 2025-12-11 16:22:57 | <tomsmeding> | kuribas: or you have (Read a, Num a) => a, with the hole also of type a |
| 2025-12-11 16:23:17 | <haskellbridge> | <matti palli> the type of the home becomes a, not the other way around |
| 2025-12-11 16:23:21 | <tomsmeding> | GHC makes some arbitrary rewriting choice when handling the equality `a ~ ?hole` introduced by the + |
| 2025-12-11 16:23:49 | <tomsmeding> | (it's not random, of course, but if it's the one I can probably flip it around by swapping the arguments to +) |
| 2025-12-11 16:24:14 | <tomsmeding> | the point is, GHC's behaviour ought not to depend on which choice is made here |
| 2025-12-11 16:24:28 | <kuribas> | tomsmeding: like you said, "read undefined" gives rise to a unification variable. |
| 2025-12-11 16:24:54 | <tomsmeding> | because if it does depend on internal typechecker choices like these, then behaviour in practice will be highly unpredictable, which GHC in general considers worse than just not supporting the thing at all |
| 2025-12-11 16:25:19 | <tomsmeding> | kuribas: if I write simply `read undefined` in a program without a hole, and I set -fdefer-typed-holes, should that result in an error? |
| 2025-12-11 16:25:32 | <tomsmeding> | if so, my `read undefined + _` makes it ambiguous whether it should throw an error or not |
| 2025-12-11 16:25:35 | <kuribas> | tomsmeding: in idris it doesn't :) |
| 2025-12-11 16:25:44 | <tomsmeding> | then it's -fdefer-type-errors, not -fdefer-typed-holes |
| 2025-12-11 16:25:49 | <kuribas> | tomsmeding: It'll happily generate an empty list of undefined type. |
| 2025-12-11 16:25:57 | <tomsmeding> | `read undefined` has no holes in haskell |
| 2025-12-11 16:26:26 | <kuribas> | tomsmeding: why should it? |
| 2025-12-11 16:26:50 | <tomsmeding> | because if it doesn't, then -fdefer-typed-HOLES should not have an impact on GHC's behaviour when compiling `read undefined` |
| 2025-12-11 16:27:21 | <tomsmeding> | (I guess the 'undefined' is a red herring in all of this, `read ""` works just as well) |
| 2025-12-11 16:27:22 | <kuribas> | tomsmeding: well it doesn't? |
| 2025-12-11 16:27:28 | → | sindu joins (~sindu@2.148.32.207.tmi.telenormobil.no) |
| 2025-12-11 16:27:38 | <tomsmeding> | right |
| 2025-12-11 16:27:49 | <kuribas> | tomsmeding: I tag ?hole as a unification variable belonging to a hole, and any constraints on it are deferred as well. |
| 2025-12-11 16:28:01 | <tomsmeding> | and should `read "" + _` and `_ + read ""` have the same behaviour under -fdefer-typed-holes? |
| 2025-12-11 16:28:29 | <kuribas> | yes |
| 2025-12-11 16:28:43 | <tomsmeding> | but the unification variable resulting from `read ""` and the one resulting from `_` are the same to GHC |
| 2025-12-11 16:28:54 | <tomsmeding> | so they're rewritten in some direction, and one of the two disappears |
| 2025-12-11 16:29:18 | <kuribas> | tomsmeding: they are now, but like I said, I would tag it as belonging to a hole. |
| 2025-12-11 16:29:30 | <tomsmeding> | what about `show (fromJust _)`? |
| 2025-12-11 16:29:45 | <tomsmeding> | does the `a` in the `Maybe a` that is the type of `_`, arise from the hole? |
| 2025-12-11 16:29:49 | <haskellbridge> | <matti palli> kuribas: but it doesn’t, it belongs to the undefined or the read |
| 2025-12-11 16:30:19 | <tomsmeding> | matti: kuribas is arguing that a type variable "arising from" a hole originally should have a little tag saying so, and when unifying two type variables, you take the union of the tags |
| 2025-12-11 16:30:21 | <tomsmeding> | I think |
| 2025-12-11 16:30:28 | <tomsmeding> | ok I have to go, sorry |
| 2025-12-11 16:30:29 | <kuribas> | tomsmeding: right |
| 2025-12-11 16:30:36 | <tomsmeding> | good luck :p |
| 2025-12-11 16:30:58 | × | lucabtz quits (~lucabtz@user/lucabtz) (Remote host closed the connection) |
| 2025-12-11 16:31:46 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2025-12-11 16:32:06 | <haskellbridge> | <matti palli> tomsmeding: hmm yes interesting |
| 2025-12-11 16:32:06 | <haskellbridge> | SPJ bugged me about this, saying we should add provenance to type variables for improved errors. If you had that you could improve holes as well |
| 2025-12-11 16:32:30 | → | spew joins (~spew@user/spew) |
| 2025-12-11 16:32:47 | <kuribas> | Yes "fromJust :: Maybe a -> a", then "?hole ~ Maybe ?sub_hole", and "Show ?sub_hole" is deferred. |
All times are in UTC.