1
$\begingroup$

I'm doing type-inference in a dependently typed language, using (as is commonly done) a λ-calculus with explicit substitutions like that of Abadi (with a representation based on debruijn indices) in order to handle the issues of scoping when performing (higher-order) unification.

The "shift" operation of those explicit substitutions (denoted ) allows one to move a term to a larger context (i.e. applying weakening). I.e. we can start from

Γ ⊢ e : τ

and then move this term e to a larger context:

Γ,x₁…xₙ ⊢ e[↑ⁿ] : τ

where e[↑ⁿ] is the result of n applications of to e. So far so good.

This also works with metavariables: if a metavariable u appears within e (where it should appear as u[σ] where σ is a "pending" substitution that should be applied to u when it gets instantiated), then in e[↑ⁿ] u will get a new explicit substitution which is a combination of σ and ↑ⁿ to make sure that after instantiating u the result is properly adjusted for the context Γ,x₁…xₙ.

Now here's my problem: The metavariables in e[↑ⁿ] will never be able to refer to any of the x₁…xₙ variables. In general, this is indeed desirable and necessary. But in my case I know that all my metavariables's original context is Γ or some extension thereof, and I'd like to compute something like e[↑ⁿ] but where the metavariables are modified such that they can refer to the new x₁…xₙ variables.

For example: let's say we have a declaration f : List u → u, and during type inference I want to generalize this to f : ∀t. List t → t, like Twelf does. The original term List u → u was declared within a context Γ so it looked like Γ ⊢ List u[id] → u[id] : *. Now this term needs to be moved to the new context Γ,t but if I do it by applying I get Γ,t ⊢ List u[↑] → u[↑] : *. But u[↑] cannot refer to t since t is at debruijn index 0 and the substitution adds 1 to the index of any variable reference, so I cannot get from List u[↑] → u[↑] to List t → t by instantiating the metavariable u (currently, I do it by manually traversing the term instead of reusing the existing metavariable instantiation infrastructure: it works but it's unsatisfactory). Note that this is no accident: u exists (is created?) in context Γ and the explicit substitutions are designed to make it possible to use it in different contexts, not to change its own context.

My question is if it rings a bell and someone has seen a similar problem somewhere, which might help me better understand the underlying problem and maybe find a different approach.

$\endgroup$
  • $\begingroup$ I think it would help if you gave an example where what you are doing makes sense and seems potentially useful. Your metavariables will be able to refer to the new bound variables indirectly via the substitition $\sigma$, won't they? $\endgroup$ – Andrej Bauer Apr 9 at 6:38
  • $\begingroup$ @AndrejBauer: I added an example which illustrates that the metavars cannot refer to tne new bound variables (directly or not). $\endgroup$ – Stefan Apr 9 at 12:59
  • $\begingroup$ The original sin here is to use a meta-variable u in the first place. As far as I am concerned, you shouldn't be using meta-variables for anything that is going to be abstracted. Write down the inference rule for $\forall$-introduction, what does it look like? It should be, more or less, that from $\Gamma, X : * \vdash A : * $ we may conclude $\Gamma \vdash (\forall X . A) : *$. The $X$ here is a object-level type-variable, not a meta-variable. $\endgroup$ – Andrej Bauer Apr 9 at 15:08
  • $\begingroup$ My real situation is more complex than my example, of course. $\endgroup$ – Stefan Apr 9 at 17:19
  • $\begingroup$ Ok, but are you trying to abstract meta-variables? $\endgroup$ – Andrej Bauer Apr 9 at 19:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.