-
Notifications
You must be signed in to change notification settings - Fork 268
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Invisible binders in type declarations #425
Conversation
653cba6
to
b000b59
Compare
Looking good so far! Per #386 (comment) I think you want the scoping and instantiation rules for data families too? |
Does this proposal touch in any way the way implicit pattern matching in type families work? I mean if I pattern match on types with different kinds, GHC implicitly pattern matches on their kinds first which can lead to surprising behavior (partiality when one does not expect it naively). With this proposal, it is possible to bind invisible arguments and explicitly pattern match on them, so would it be possible to disable that implicit pattern match completely and present an error to the user? |
@jvanbruegge The proposal disallows matching on implicit kind parameters on the RHS, so the following will become illegal:
You would need to rewrite it as:
However, if matching happens on the LHS, it is still fair game:
For clarity, we could rewrite it as:
But in this case it is not required. |
Ok, cool. Yeah, I meant the first case |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I like where this is going. Many thanks for writing this up!
type family G x :: forall k. Maybe k | ||
|
||
With ``@``-binders we can do the opposite. We propose that by default, arity | ||
inference would include as few forall-bound variables as possible, to allow |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
More than that, the arity would no longer be strangely influenced by the return kind signature. Instead, you can simply count the binders to the left the ::
(if any).
Sigh: not quite. In
F :: forall k. k -> Type
type family F a
F has arity 2, not 1.
I have added some comments I am happy to see that you have included
but you have zero text motivating, or even specifying, this point. There is plenty to plunder in https://github.com/ghc-proposals/ghc-proposals/blob/wip/spj-instance-scoping/proposals/0000-instance-scoping.rst |
7d0d40e
to
17aaefc
Compare
This is ready for another round of review. |
The title still says “Draft”. Oversight? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm quite happy with this! Thanks.
5. In type synonym declarations, require that every variable mentioned on the | ||
RHS must be bound on the LHS. | ||
|
||
6. In type family and data family instances, require that every variable |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This part is completely separable from the rest of the proposal, I think. Is this stated somewhere?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It’s implied by putting it into a section titled “Secondary Change”.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, but I would expect a "secondary change" to depend on the primary one. This one has no relationship, really, to the rest of the proposal. I'm all for it -- just got surprised at first at seeing a change to instance syntax in a proposal about type syntax.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
True, this proposal bundles a few unrelated changes together.
Secondary Change: Instantiation Rules | ||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | ||
|
||
7. In type family and data family instances, the instantiation is fully |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This, similarly, is completely separable form the rest of the proposal -- even the other point about instances. They are in sympathy with each other (and, indeed, the rest of the proposal), but there is no dependency between the rest of this proposal and these two points about instances. Right?
* Changes (1), (2), and (3) provide the programmer with a more principled way | ||
of brining type variables into scope in certain corner cases. | ||
|
||
* Changes (4), (5), and (6) simplify arity inference and scoping rules, but they are |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(6) does not need a migration strategy, because the fix is backward-compatible.
I'm not very bothered about (4), which is rather exotic.
For (5), I would say to issue a warning for a few releases before pulling the trigger. I don't think that would be hard to implement.
@nomeata I'd like to submit this proposal to the committee. |
@goldfirere In case this slipped your attention, do you plan to make a recommendation? |
@goldfirere Richard, shall we move forward on this one? |
Somehow, this fell off my radar -- apologies. I have recommended acceptance, but with a migration strategy around point (5). |
Vlad, this is pretty impenetrable. Earlier you say "SAKS zipping works over two lists: quantifiers and binders. Let us define it in pseudo-code:". At least give a type signature to this function. But more importantly: so what? Now you have defined zipSAKS. Why have you told me this?
This is a rather negative explanation. Why not say what we do? Something like: The arity of a type-family declaration
is determined solely by the visible arguments
You may want to also point out that there may be invisible inferred kind args. |
I strongly support this proposal, because it lets us say explicitly things that we can only currently say implicitly. It fills out part of the design envelope. Let's do it. |
In sympathy with what I just posted at #442 (comment), I'm fine with the current version of this proposal -- at least until we accept. Perhaps if this is to be long-lasting, it's worth improving the presentation. But, even there, I'm not convinced: the description of this feature belongs in the user manual, not in this repo. And the proposal is burdened with capturing the change from the status quo, which need not appear in the manual. I agree that the current presentation is hard-going, and it has room for various improvements. But I'm equally confident I understand the intent of this proposal and could evaluate whether an implementation meets the specification presented here, and so I don't see the value in the time investment of improving the presentation. To be clear, I would consider a presentation like the one in this proposal below the bar ("unacceptable" sounds very harsh, but is semantically accurate) for the user manual. |
What we explain to our users (in the User’s Guide) does not need to involve But in the “Proposed Change Specification” my goal wasn’t to explain the feature to the end user. Rather, I wanted to specify it in a way that would be precise enough to guide the implementation efforts and to cover all corner cases. Honestly, I have no idea how to do it without introducing the notion of SAKS zipping.
It’s the function that determines which binder corresponds to which quantifier. So if you have
What do |
But that’s simply not the case. Consider:
What arity does it have? Depends on the kind signature:
|
Hmm, yes you are right. It's quite hard to specify arity. And yet we must.
As I say, I'm strongly in favour of accepting this proposal, and that opinion is not conditional on improved presentation. But I know I'm going to be asked to do code review. What often happens is that I'm trying to review code against a specification that is absent or at least hard to understand. I'm trying to avoid that. So I'm reading the proposal thinking "could I implement this?", and writing comments accordingly. I'm perfectly content with a specification presented as a user-manual entry. But (unlike @goldfirere) I would say that a draft user manual entry would be a terrific component of a proposal. It can be written post-acceptance -- I'm not trying to raise the bar for a proposal that might be rejected. My anxiety is that post-acceptance the author breathes a well-deserved sigh of relief, and the improved presentation, the more detailed specification, or the user manual entry, ultimately never gets written. I strongly agree it's much better not presented as a diff against some (also often ill-specified) baseline. |
I would say we should be always able to merge the feature, but it might need a deprecation cycle. For example, simplified subsumption could have gotten a deprecation cycle rather than being cancelled outright as many people probably wished after being unable to upgrade to 9.0. I too need to write a discorse post, but about how the sort of modularity work @hsyl20 and I are into directly relates to our ability to do proper depreciation cycles without drowning in hard-to-test conditional code. |
@goldfirere That’s a fine plan, and thanks for taking the initiative here. |
@goldfirere set a reminder for Mar 24th 2022 |
Hehe Reddit thought it was spam. (What on earth triggered their algorithm?) |
Reddit's zealous spam filter snares me about 10% of the time I post a story. I messaged the mods to request they restore it. |
👋 @goldfirere, review responses . |
All seems in order here. In particular, the community outreach did not produce any red flags. I am (re-)recommending acceptance to the committee. Thanks! |
/remind me to accept this proposal (pending committee agreement) on April 4. |
@goldfirere set a reminder for Apr 4th 2022 |
@goldfirere Note that the reddit post is still marked as |
@JakobBruenker That's true (and I was aware of it). But given the quietness both on Discord and Twitter, I decided not to investigate. If you want to get Reddit unblocked, great! There's no reason that we can't revisit the committee discussion in light of new information from Reddit. But I'm afraid I'm not going to take another crack at Reddit on this front. |
@phadej points out (on Reddit, but the thread is mostly about something else) that this proposal violates the Explicit Variables Proposal, included in #448, because there is no way to bring inferred variables into scope without unification. (Actually, the same is true within #448.) This suggests that this proposal might benefit from the I do not suggest we change this proposal at this point, just that there is an improvement possible in a later proposal. |
👋 @goldfirere, accept this proposal (pending committee agreement) on . |
The proposal has been accepted; the following discussion is mostly of historic interest.
This is my rewrite of #326 + #386.
We propose to allow invisible type variable binders (i.e.
@k
) in type declarations. Here are a few examples:In a class declaration:
In a data type declaration:
In a type family declaration:
We then propose to use these binders to simplify scoping rules and arity inference.
Rendered