Typing of substitution in a bidirectional type system

Question

In most typed lambda calculi, we have the following lemma:

• If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[t_1/x]$

However, I'm wondering how we'd phrase such a lemma in a bidirectional typing system, with synthesis $\Rightarrow$ and checking $\Leftarrow$ judgements.

The main problem is that substitution does not preserve synthesis. For example, in most systems, $\Gamma \vdash x \Rightarrow T$ if $x : T \in \Gamma$, but $[(\lambda y \ldotp t)/x]x$ won't synthesize any type if there are only checking rules for $\lambda$.

Potential solutions I can think of:

1. Restrict to substituting with synthesizing expressions. This seems like it would give us the induction hypothesis we need (since, in most systems, all synthesizing expressions also check), but is very restrictive.

2. Only show that substitution preserves checking. This is a weaker result, and I'm unsure of whether it gives us a strong enough inductive hypothesis, since it would be difficult to rebuild typing derivations with synthesis judgements in the premises.

This seems like a pretty basic metatheoretic property, so I'm sure I'm not the first one to have encountered this. Does anyone have a reference to a bidirectional system that cleanly solves these issues? Is there an obvious solution I am missing?

Answer 1

The key observation is that whether the substitution theorem holds, depends on the definition of substitution.

For the usual definition of substitution of terms for variables, the substitution theorem is only true for substituting synthesizing terms for variables.

Indeed, if you introduce separate grammatical classes for synthesizing and checking terms, then using the usual substitution operation to replace a variable with a checking term will leave you with an ungrammatical expression. So this suggests that the usual substitution operation is the wrong definition.

However, this leaves you with the option of defining a different substitution operation. The keyword to search for is "hereditary substitution". It's based on two key observations:

1. If you replace a variable with an introduction form at an elimination site (eg, replace the $f$ in $f\;x$ with a lambda) then you can just do the reduction as part of the substitution.

2. Next, you can turn synthesizing terms into checking terms by $\eta$-expanding them. That is, if $f$ is a variable of type $X \to Y$, you can turn it into the introduction form $\lambda x:X.\;f\,x$.

One paper you might want to look at in addition to the ones that gallais pointed you at is my paper with Nick Benton, A Semantic Model of Graphical User Interfaces, which defines and proves the correctness of hereditary substitution for a mixed linear/intuitionistic calculus (in section 5).

Answer 2

One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't fit. It is not that restrictive in the sense that usually a checkable term together with a type annotation gives you an inferrable term. This embedding is typically called cut because well... this is what it is. This restriction is described (and deployed) in I Got Plenty o’ Nuttin’.

Alternatively (which is also mentioned in IGPoN) you can define hereditary substitution (a formalised account for STLC) whereby if you are about to form a redex because of the checkable you just plugged in, you fire it. And again. And again. And again. Until your substitution is not creating any new redexes.