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
There is no easy way to give names to existential variables introduced by GADT pattern-matching #7074
Comments
Comment author: @stedolan How about allowing
I interpret the above as introducing new locally abstract types, which are immediately unified with the GADT existentials. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
We should do something about that, eventually. |
Here's a concrete proposal, distilled from the discussion in #5780:
|
Distillation is warmly welcome here, thanks! I don't like 2.a and 2.b, because I find (Should we also allow With this design patterns can introduce local abstract type constructors in addition to term variables. The same restriction for or-patterns must apply that they bind the same variables -- or at least that only the intersection of the two sides stays in the resulting environment. Do we know how to implement this under or-patterns, or is this syntax forbidden under or-patterns for now? With the proposal, I guess we can also write either of the following:
which is cool. (The second one is slightly confusing because it is not checking that the two |
@yallop's 3rd version does indeed make sense. Yet, re-reading the discussion, the solution proposed by @stedolan above, and argued by @lpw25 in #5780, feels more natural. It's just a question putting a correct semantics on it. It seems to me that, if we intend to match the existential type variables through normal unification, these new names should actually represent plain unification variables. function 'a. C ((x : 'a), f) -> ... makes perfect sense (assuming that we accept that |
I would be happy with parts 1 and 2c. The syntax is natural and easy to work out what it means. I have previously argued that 2c shouldn't need full type annotation. However, it is clearly forwards compatible to force full annotation now, and allow less annotation if we work out how to do it well later. |
I would also agree to go for 1 and 2c, which have a nice consensus and do not open further questions (unlike 2a/2b). |
From an outsider's perspective, this does not make perfect sense to me. (Especially with the One of the most common misunderstandings I see in OCaml is in thinking that constraints of the form let id (x : 'a) : 'a = x + 1 module type T = sig type t val print : t -> unit end
let f (module T : T with type t = 'a) (x : 'a) = T.print x My standard response to this is something like: "Type variables like I end up giving this explanation to a lot of students, colleagues, etc. and the new syntax would force me to add "unless the local type is introduced by If we're going to get more ways to introduce local types (which I really appreciate!), I'd much prefer it if they didn't have a leading quote mark. I think this
Footnotes
|
But that was exactly my point: locally abstract types arising from existentials cannot be easily bound other than through some kind of unification process. However, if we use unification variables, we can at least have a way to refer to them (which doesn't imply anything more, i.e. the Of course, I agree with you that using properly introduced type names rather than type variables is more comfortable. Unfortunately it is not always easy to retrofit that on a language based on type inference. I'm still considering how to implement @yallop's suggestion, as it will probably require to do something like for universal type variables (as in polymorphic methods), but using locally abstract types instead... much harder to specify properly. |
Intuitively, one way to relate the notations
From an inference point of view, this interpretation would suggest having those variables be flexible when checking the pattern, and rigid when checking the right-hand-side. This works well when they are used at the position of existential variables, but it behaves weirdly in other situations (if they are unified with non-variables or variables from the context, then only the remaining flexible parts would be rigidified?). |
This was also my analysis. The trouble being that, in normal unification mode, reification does not commute with unification. So that the syntax you suggested would actually be the safest bet. function
| (Int : type a = int . a t) -> ...
| (C : type a b. a * (a -> b list) -> t) (x,f) -> ... I.e. give a complete type, and check that it properly instantiates the constructor. In particular, that all existentials are fresh (and distinct). Actually, this follows @yallop's 2(1) with a more standard syntax (hoping that it doesn't generate conflicts...) |
I don't understand what you mean here, can you elaborate? (In my intuition, but I don't know how local type variables are implemented, we would first type-check the pattern part with just local inference variables, then "ridify them" by turning the locally-bound parts into (rigid) local type variables, and then type-check the body. First we do unification, then rigification, and then more type-checking.) |
Intuitively, another approach would be to create locally abstract types from the start, and then type-check the pattern arguments against an instance of the constructor type where existentials are replaced by fresh unification variables (that can unify with the locally-abstract types). The unification variables could unify "too much", so we then need to check that the resulting inferred type preserved the existential types., I suppose can be done by generalizing it (including the locally-abstract types) and then unifying it with a rigid instance of the constructor type. This reminds me of the discussion in #1132 which contains some of the same ingredients (an inference process that is first flexible, then compared against a rigid version). |
It was a bit fuzzy. The essential problem is that rigid type variables cannot be refined during normal unification, so we need to decide them before using unification. The unify-then-rigidify approach only works if we know exactly the expected type. |
I can see how this is easier for the implementation, but it is also very constraining for the user who has to repeat the whole constructor type each time just for the usability benefits of naming the existential variables. In particular, this is in fact heavier in term of amount of information than the unpleasant trick of re-abstracting over the parameters that contain the existential variables to name them with locally-abstract types. We could provide both forms, but I think that this "fully annotated" form is going to be more rarely used. For functions we have both forms: |
Well, I have a lot to answer.
but I'm not really convinced this feature will be much used anyway. It comes handy, but only In very specific cases. This said, I've battled with menhir to get a valid grammar, and I'm not sure it works yet.
Note that the above annotation is currently illegal, so this may make the new semantics clearer (at least when there are several arguments). |
For me the problem with the fully-annotated form is not so much the length as the loss of locality: if I want to understand the type of
This sounds very brittle and I'm certainly not suggesting we do this. Is my "your second approach" suggestion not viable to avoid it? In the not-fully-annotated case, (after creating the locally abstract types) we would generate fresh inference variables at a level that lets then unify with the internal existentials, and then use pattern checking unification (between the flexible-instantiated constructor type and the user-given pattern with locally-abstract types) to trace which of those inference variables get unified with the locally abstract types. |
I'm not sure what you are suggesting here. If you mean that the matching of the names and existentials can be obtained by unifying an instance of the constructor type with the annotations given by the user, and doing extra checks, this is indeed what I have in mind. |
I haven't followed all of today's discussion, but I was interpreting Jeremy's 2c option to be: | C (type a b) (x : a) (f : a -> b list) -> ... where the type annotations are a required part of the syntax -- it is always an error to omit them. This seems basically equivalent to the above suggestion with an explicit type for the constructor, so I'd be surprised if it were somehow harder to type-check. |
After various attempts, I implemented the following in #9584: | C (type a b) (x, f : a * (a -> b list)) The reason the annotation is on the tuple rather than on individual arguments is that it is simple to enforce it at the parser level. |
#9584 got merged, so I believe this issue can be closed. |
Original bug ID: 7074
Reporter: @garrigue
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2015-12-04T01:38:20Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.3
Target version: later
Category: typing
Has duplicate: #5867
Related to: #5780
Child of: #5998
Monitored by: @gasche @diml "Julien Signoles" @yallop @hcarty @alainfrisch
Bug description
When you do pattern-matching on GADTs, new existential variables may be introduced in the environment, either by refining existing locally abstract types, or because the constructor contains some existential variables. One cannot give them a name: they are incompatible with any existing existential variable, and using a normal type variable name causes a scope extrusion.
One often wants to introduce type annotations just for readability, but in some cases they are even required for typing.
There has been already a lengthy discussion in #5780 on what kind of syntax could be used to do that, but no conclusion yet. Let's move the discussion here.
Steps to reproduce
Additional information
The text was updated successfully, but these errors were encountered: