type of pair term

Stream: maths

[Leonard Wiechmann]

hey all, this is not lean related, so i thought the maths channel would be appropriate:
i'm implementing type theory (inspired by http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/).
i had a little problem when determining the type of a (dependent) pair term. the code was (roughly):

    Pair (terms) => {
        let (a, b) = terms.as_ref();
        let     ta = infer_term(ctx, a);
        let mut tb = infer_term(ctx, b);
        shift(&mut tb, 1, 0); // delta, cut_off
        Sigma(Box::new((ta, tb)))
    }

basically: infer the types of the sub-terms and construct a sigma type by shifting the second type (to account for the scope introduced by a sigma type).
the problem was: obviously, the sigma type could never refer to its fst value. i'm using syntactic equality of reduced terms as definitional equality. to check types i use definitional equality (and u1 <= u2 for sorts).
so if the type of snd depends on the value passed into fst, that information gets lost.
i have solved the problem by substituting the value a (shifted by one) in tb (after shifting) with Var(0).
and now for why i'm posting this:
i'm not too comfortable with the solution.
first of all, sub-tree matching is pretty expensive, compared to the other operations in the type checker.
secondly, i have not seen this "trick" anywhere else. the links to the code in the article are dead, but this seems to be the code from around that time: https://github.com/Andromedans/andromeda/blob/d7ec08f94331e1254dc4430607e7ea95b16a7f6f/typing.ml they also shift the type of snd, but there is no substitution.
the typing rule in mltt80 is: (a: A) (b: B(a)) |- (a, b): (\Sigma x: A)B(x). i interpret the presence of x as the same kind of information loss that i've experienced before my change.
in conclusion: my "trick" seems fishy to me. maybe someone knows how this problem (determining the (dependent) type of a pair) is usually handled in type checking kernels.

edit: here is an example that failed to type check (due to mismatched de bruijn indices in the type of the pair (a, b) - argument to g at the end - specifically, b's type was referring to the parameter a, not the first value of the pair -- this is the lean equivalent)

def f := λ (T: Type 0) (f: T → Type 0) (g: Π (x : (Σ a : T, f a)), f x.1) (a: T) (b: f a), g ⟨a, b⟩

[Chris B]

I'm sure someone else can give you a better survey of general solutions, but Lean uses locally nameless, which I think would solve this by replacing occurrences of a in b with Local(ta, unique) instead of Var(0), and then the result would be Sigma (x : ta), tb.abstract(locals).

[Leonard Wiechmann]

Thanks @Chris B ! So this does appear to be a "real" problem that needs to be addressed in a type checker. I was mostly worried that I did something wrong, elsewhere in my code (which could of course still be the case :P).
For now, I'm fine with my tree substitution thing. But if anyone else has something interesting about this topic, I'd of course still be interested!