<p>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.</p>

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

<pre><code>Γ ⊢ e : τ
</code></pre>

<p>and then move this term <code>e</code> to a larger context:</p>

<pre><code>Γ,x₁…xₙ ⊢ e[↑ⁿ] : τ
</code></pre>

<p>where <code>e[↑ⁿ]</code> is the result of <code>n</code> applications of <code>↑</code> to <code>e</code>.  So far so good.</p>

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

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

<p>For example: let's say we have a declaration <code>f : List u → u</code>, and during type inference I want to generalize this to <code>f : ∀t. List t → t</code>, like Twelf does.  The original term <code>List u → u</code> was declared within a context <code>Γ</code> so it looked like <code>Γ ⊢ List u[id] → u[id] : *</code>.  Now this term needs to be moved to the new context <code>Γ,t</code> but if I do it by applying <code>↑</code> I get <code>Γ,t ⊢ List u[↑] → u[↑] : *</code>.  But <code>u[↑]</code> cannot refer to <code>t</code> since <code>t</code> is at debruijn index 0 and the <code>↑</code> substitution adds 1 to the index of any variable reference, so I cannot get from <code>List u[↑] → u[↑]</code> to <code>List t → t</code> by instantiating the metavariable <code>u</code> (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: <code>u</code> exists (is created?) in context <code>Γ</code> and the explicit substitutions are designed to make it possible to use it in different contexts, not to change its own context.</p>

<p>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.</p>

CC BY-SA 4.0
2020-04-09T06:38:01.503Z
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?
Andrej Bauer
CC BY-SA 4.0
2020-04-09T12:59:27.627Z
@AndrejBauer: I added an example which illustrates that the metavars cannot refer to tne new bound variables (directly or not).
Stefan
CC BY-SA 4.0
2020-04-09T15:08:59.207Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-04-09T17:19:21.143Z
My real situation is more complex than my example, of course.
Stefan
CC BY-SA 4.0
2020-04-09T19:34:22.633Z
Ok, but are you trying to abstract meta-variables?
Andrej Bauer
CC BY-SA 4.0
2020-04-09T21:44:27.130Z
Yes, in my example I turn uninstantiated metavariables into arguments, as is done in Hindley-Milner inference.
Stefan
CC BY-SA 4.0
2020-04-11T07:04:03.823Z
We've had a similar situation in Andromeda, but when we abstract meta-variables we get *inference rules* (the meta-variables become premises of a rule). The "type" of a meta-variable is what we call a *boundary* (a judgement with a hole $\Box$), and it's not so clear how you'd abstract over a boundary, say something like $x : A, y : B \vdash \Box : C$ is the type of a meta-variable that may refer to variables $x : A$, $y : A$ and has type $C$ (which depends on $x$ and $y$).
Andrej Bauer
<lambda-calculus><type-inference>
A substitution to add variables in the context
Stefan
# A substitution to add variables in the context

(Asked by: username_0 on 2020-04-08)

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.

**Tags:** lambda-calculus, type-inference

> **Comments:**
> **username_1**: 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?  
> **username_0**: @AndrejBauer: I added an example which illustrates that the metavars cannot refer to tne new bound variables (directly or not).  
> **username_1**: 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.  
> **username_0**: My real situation is more complex than my example, of course.  
> **username_1**: Ok, but are you trying to abstract meta-variables?  
> **username_0**: Yes, in my example I turn uninstantiated metavariables into arguments, as is done in Hindley-Milner inference.  
> **username_1**: We've had a similar situation in Andromeda, but when we abstract meta-variables we get *inference rules* (the meta-variables become premises of a rule). The "type" of a meta-variable is what we call a *boundary* (a judgement with a hole $\Box$), and it's not so clear how you'd abstract over a boundary, say something like $x : A, y : B \vdash \Box : C$ is the type of a meta-variable that may refer to variables $x : A$, $y : A$ and has type $C$ (which depends on $x$ and $y$).  

---

## 0 answers

