To be honest, I sometime need in Coq to explicitly write all the variables to make sure the type checker and I understand each other ;-) ... and sometimes I want it to be implicit. So I don't think there is a perfect solution to this problem except to provide both solutions in a clear and standard way.
Coq gives the user the ability to change how the system handles implicit variables (Implicit Arguments On/Off). But it is done at the file level. Your syntax solution "`something else` for those variables that are meant to be implicit arguments?" could be triggered by a lexically scoped macro. So anyone using (with-something-else-syntax ...... ) will have use for example ??a for implicit variables and someone using (with-implicit-on-syntax .....) would revert to the default.
That would show off the power of Typer's macros .... although I guess it would have to be a built-in macro since it's tied to the elaborator.
Vincent
On Tue, Jun 9, 2020 at 1:44 PM Archambault-Bouffard Vincent < vincent.archambault-bouffard@umontreal.ca> wrote:
From: TyperOn Behalf OfStefan Monnier Sent: June 9, 2020 1:43:52 PM (UTC-05:00) Eastern Time (US & Canada) To: typer@IRO.UMontreal.CA Subject: [Typer] Variables in type annotations
OK people, I have a language-design question for you. Any ideas/comments/suggestions welcome. Here's the problem:
Let's say we want to define a proof that:
myproof : IsReverse ?a ?b -> IsReverse ?b ?c -> Eq ?a ?c; myproof P1 P2 = ...;If `IsReverse` is defined on plain lists, the real type would likely look like:
myproof : (ℓ : TypeLevel) ≡> (α : Type ℓ) ≡> (a : List α) ≡> (b : List α) ≡> (c : List α) ≡> IsReverse a b -> IsReverse b c -> Eq a c;But of course, if `IsReverse` is only defined on lists of integers, then the real type would likely look like:
myproof : (a : List Int) ≡> (b : List Int) ≡> (c : List Int) ≡> IsReverse a b -> IsReverse b c -> Eq a c;and there can be many other variants if `IsReverse` is instead defined on length-indexed lists or on lists that live in a specific universe, ...
The point is that we want a form of *generalization* (like Hindley-Milner's let-polymorphism) where we add implicit parameters.
Now there are 2 different implicit parameters above: those that appear explicitly in the source (i.e. `a`, `b`, and `c`) and those that are introduced indirectly (`ℓ` and `α`).
Currently in Typer I treat those two kinds of implicit parameters identically: they're just metavariables and they get generalized if they haven't been instantiated.
But there's a question of what I consider before generalizing: A) What I do currently is to just elaborate
IsReverse ?a ?b -> IsReverse ?b ?c -> Eq ?a ?cto make sure it's a valid type, and then generalize whichever part has not been instantiated during this elaboration.
B) Another option is to elaborate the complete definition of `myproof` and generalize the type it returns.
If I do (B) then it might be the case that during elaboration of `myproof` one of the variables like `a` ends up instantiated (because I wrote a proof which only proves it for the case where `a` is the empty list, for example), so I might end up with
myproof: IsReverse nil nil -> IsReverse nil nil -> Eq nil nil;which is correct if the `?a`, `?b`, `?c` are taken to mean "let elaboration figure out what should come here", but is probably not what the coder intended above.
With option (A) this can still happen, but is much less likely, which is why it's the option I've taken so far. But really, I'm starting to feel like Typer should distinguish those 2 sets of implicit parameters: the ones that appear explicitly in the code should never be instantiated.
Some languages use a convention that any variable that doesn't yet exist in the context is assumed to be one of those "implicit arguments" like `a`, `b`, and `c`, so we could write:
myproof : IsReverse a b -> IsReverse b c -> Eq a c; myproof P1 P2 = ...;without the question marks, and that would distinguish the two sets of implicit parameters.
But this has the disadvantage that the user has to be careful to use names that aren't already present in the context.
So, should we have 3 different ways to write a variable?
- `a` for normal vars found in the context
- `?a` for metavariables than can be instantiated (i.e. to mean "fill this for me")
- `somethingelse` for those variables that are meant to be implicit arguments? I guess 'a could be a "natural" choice here for people used to the SML/OCaml syntax.
I'd be really happy if I could avoid that complexity.
Stefan
Typer mailing list Typer@iro.umontreal.ca https://mailman.iro.umontreal.ca/cgi-bin/mailman/listinfo/typer