idris-lang
The Unique Hole
The Unique Hole
- [X] I have read CONTRIBUTING.md.
- [X] I have checked that there is no existing PR/issue about my proposal.
Summary
Define "unique holes", with the syntax ?_.
Make every occurrence of ?_ distinct, including from other instances of ?_, and allow it to be used in multiple different scopes in the same namespace.
Motivation
Idris' hole system is incredibly powerful. However, usage of it can often be tedious due to the constant need for the programmer to generate fresh holes names.
The proposal
Allow for "unique holes", with the syntax ?_.
Unique holes behave exactly like other named holes, except for the fact that every usage of them represents a different hole.
Unique holes should always be replaceable by named hole that occurs nowhere else in the program. These would be solely a convenience, albeit a useful one.
Note that unique holes are less powerful than named holes.
This is because, even when fully qualified, a unique hole may not name a single hole, as in, for instance, f : ?_ -> ?_.
While this does prevent querying of unique holes at the REPL, this should not be a problem.
This is because unique holes should not and indeed can not replace named holes for every single use. Unique holes serve the use of quickly sketching a project, leaving the implementations of functions to be left "for later".
Named holes, on the other hand, would serve the purpose of inspecting needed subexpressions as a tool for constructing them at the time. Named holes, as of current, are used for both of these. However, in the first case, the one that unique holes are designed for, it is not always important to be able to query information (from the REPL) about the hole. In the case that information on a hole is needed, it should always be (or should always be changed to) an appropriate named hole.
Examples
Consider the list of days of the week:
data Weekday = Monad | Tuesday | Wednesday | Thursday | Friday
Together with some functions, showDay, dayToTag, and nextDay:
showDay : Weekday -> String
showDay day = case day of
Monday => "monday"
Tuesday => "tuesday"
Wednesday => "wednesday"
Thursday => "thursday"
Friday => "friday"
dayToTag : Weekday -> Int
dayToTag day = case day of
Monday => 0
Tuesday => 1
Wednesday => 2
Thursday => 3
Friday => 4
nextDay : Weekday -> Weekday
nextDay day = case day of
Monday => Tuesday
Tuesday => Wensday
Wednesday => Thursday
Thursday => Friday
Friday => ?dayAfterFriday
After getting this far, you might think it would be nice for the nextDay function to be complete, so decide to add Saturday and Sunday.
With unique holes, the exact same code can be used for all 3 functions (without name conflicts):
data Weekday = Monad | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday
showDay : Weekday -> String
showDay day = case day of
Monday => "monday"
Tuesday => "tuesday"
Wednesday => "wednesday"
Thursday => "thursday"
Friday => "friday"
_ => ?_
dayToTag : Weekday -> Int
dayToTag day = case day of
Monday => 0
Tuesday => 1
Wednesday => 2
Thursday => 3
Friday => 4
_ => ?_
nextDay : Weekday -> Weekday
nextDay day = case day of
Monday => Tuesday
Tuesday => Wednesday
Wednesday => Thursday
Thursday => Friday
Friday => ?dayAfterFriday
_ => ?_
As opposed to without them:
data Weekday = Monad | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday
showDay : Weekday -> String
showDay day = case day of
Monday => "monday"
Tuesday => "tuesday"
Wednesday => "wednesday"
Thursday => "thursday"
Friday => "friday"
_ => ?h0
dayToTag : Weekday -> Int
dayToTag day = case day of
Monday => 0
Tuesday => 1
Wednesday => 2
Thursday => 3
Friday => 4
_ => ?h1
nextDay : Weekday -> Weekday
nextDay day = case day of
Monday => Tuesday
Tuesday => Wednesday
Wednesday => Thursday
Thursday => Friday
Friday => ?dayAfterFriday
_ => ?h2
The difference is, admittedly, quite small. However, in a file with the number of "todo-like" holes
Technical implementation
Unique holes, as previously mentioned, are not (in the internal language) different from named holes. Rather, at some point in compilation, each named hole is replaced internally with a hole with a generated, unique identifier for that given hole.
As mentioned above, named holes cannot and should not be queryable by REPL commands, as this is beyond the intended scope. The generated names need not be given to the user.
Finally, although a little beyond the scope of this proposal itself, a command such as :holes might be created that shows every hole in a program in its context, including unique ones.
However, this is beyond this proposal's scope.
Alternatives considered
Named Holes
The major alternative is of course named holes. As already mentioned, named holes are wonderful at many things. They are queryable, integrated into the core language, and ultimately a very good system for what they are designed for.
However, unique holes were created not to replace named holes, but merely to create a system to slightly improve a specific use of named holes. Unique holes serve the single purpose of acting as a "zero effort" version of named holes, without the need to make each hole have a different name.
It should again be emphasized that unique holes are both eventually translated into the same core construct as named holes and are also less powerful than their named counterparts. Unique holes serve the sole purpose of a quick "todo" style hole that one doesn't want to keep track of.
Conclusion
Idris is perhaps one of the few languages that fully realizes the potential of complex, type-safe software. It can often be useful, when writing software, to consider the interface of a software before considering its exact implementation. Because of this, a utility to quickly note that a value should be constructed at some future point of time would serve a large practical purpose, even if it has no actual expressive power.
Personally, I just keymash random hole names, like ?sdnfjhke. These are almost always unique, and because they are actually named, I can copy and paste them into the REPL for querying. So I don't really see the need for this.
There is no need for this, only a desire for it. However, at least personally, this feels far more elegant. In addition, the holes above, in the case that you want to inspect them can just be replaced with a named hole, with no possibility of failure (assuming that the named holes does not overlap any other name)
I'm glad I'm not the only one mashing my keyboard.
My strategy for a while was to loop through multiple translation of the words "what" and "how". (un)fortunately this never actually made me learn new languages.
Anonymous holes are probably still a good idea, but I'm amused that the first comment is literally "have you tried facerolling on your keyboard?". It's also probably not too hard to implement, so I'm curious to see what other people think, especially the ones who commented on the first issue
Another keymasher here 👋
I do think elseLuna raise a good point: how would unique holes interact with the REPL? Part of the strength of holes (imo) is to be able to query them at the REPL, having multiple buffers/terminals/screens open at the same time, with the hole information in at least one of those. So unique holes which I could reference, that would be awesome. Unless that turns out to be a pain to implement, in which case the answer might be "if you want unique holes, that's fine, but like machine names, these are u̷n̷s̴p̶e̷a̶k̶a̸b̶l̵e̷ by mere mortals and you'll need to name things yourself"
No I discussed this in detail with @andrevidela previously. Ultimately, the conclusion reached was the fundamentally the purpose of "unique holes" is that of a hole that is to be done later but not inspected now. Then, when the time comes to implement it, and it turns out to be a complex task, then you switch to named holes.
So yeah, it is a little bit of an annoyance, but I think for the purpose of all our keyboards something that would be better to live with then our the keyboard rights activists showing up at our doors.
(The reason they'd be a pain to implement (or even design a system for) is that unique holes, are, well, unique. Currently, named holes have distinct names up to their namespace. However, unique holes are not just not unique up to the namespace, there's also no guarantee they're unique beyond that (ie, f : ?_ -> ?_ has two holes, which can't be distinguished by name).
I think its important that unique holes have a very limited scope, the aforementioned "keymash now, implement later" point. They are not intended to be inspected, and merely serve as a placeholder. But again, a unique hole can always be replaced by a named hole that is unique, so, for instance, if we wanted to start constructing the type of f, we might change f : ?_ -> ?_ to f : ?h0 -> ?h1 to allow for easier inspection.
I hope this answers the question, I realize this response is a little rambling in nature 😅
If such a hole is a “todo” then I’d think at the very least being able to enumerate and jump to it would be useful. What use is a TODO if it’s hard for me to locate because I am just visually scanning the file? Current named holes show up in the list of “metas” and the LSP can jump between them. I don’t recall off hand who does the heavy lifting there (compiler or LSP) but my point is that these new holes would hopefully at least make that kind of thing a possibility.
On the point about them not being inspectable, I assume they also cannot be used by other code actions like “fill.” This is actually pretty limiting I think as my use-case for keyboard smashing a hole into existing often does end up eventually in me performing some code action on that hole.
I’m not sure I see the example about completing functions in the description as very motivating. Adding a catchall clause and putting a hole on the RHS (whether it’s a named hole or not) doesn’t complete a function, it just moves the gap around. Leaving function clauses off makes a function explicitly partial, adding clauses with holes makes them implicitly partial until the hole is filled. Furthermore, the compiler will generate missing cases for you and give the resulting holes names so the use case is specifically for non-interactive editing.