modeling MLTT

Stream: Type theory

[Reid Barton]

Mario Carneiro said:

Here's a sketch: [...]

Great. Now suppose I want to interpret this syntax into the following kind of setup (the natural models of https://arxiv.org/abs/1406.3219v4):

• we have a category $C$ whose objects we think of as contexts;
• we have a presheaf $\mathsf{Ty} : C^{\mathrm{op}} \to \mathrm{Set}$ where we think of $\mathsf{Ty}(\Gamma)$ as the types in context $\Gamma$;
• we have a presheaf $\mathsf{Tm} : C^{\mathrm{op}} \to \mathrm{Set}$, together with a natural transformation $p : \mathsf{Tm} \to \mathsf{Ty}$ where we think of those elements of $\mathsf{Tm}(\Gamma)$ which map to a given $A \in \mathsf{Ty}(\Gamma)$ as the terms of type $A$ (in the context $\Gamma$).

[Reid Barton]

Then I want to assign

• to every "well-formed" Γ : list exp an object $\Gamma$ of $C$,
• to every pair Γ : list exp and A : exp that is well-formed/well-typed, a section $A \in \mathsf{Ty}(\Gamma)$,
• to every suitable Γ A e a suitable section in $\mathsf{Tm}(\Gamma)$.

[Reid Barton]

What's not yet obvious to me is whether I can do it by induction on Γ A e rather than on the derivations.

[Reid Barton]

(Obviously $\mathsf{Ty}$ and $\mathsf{Tm}$ are equipped with some extra structure which tells me how to interpret type formers)

[Reid Barton]

Maybe I really can define it by induction on exp! That would be nice.

[Reid Barton]

Normally there are things called a reversion or reversal lemmas or something that let you recover the types of pieces of an expression from the type of the entire expression, right? And somewhere you must have to take into the account that definitionally equal types can be interchanged.

[Reid Barton]

Like one example must be that if var n has type A in context Γ then list.nth Γ n has to be some A' for A and A' defeq but not necessarily equal.

[Reid Barton]

Might it make sense to consider well-formed-ness and defeq-ness together as a partial equivalence relation? Type theory people seem to like those...

[Reid Barton]

I'm not sure how to reconstruct the type of the function f in app f x though. Seems like you lost the information of the entire dependent type that is its output.

[Reid Barton]

Actually you would need to recover type information for both f and x.

[Reid Barton]

In https://github.com/guillaumebrunerie/initiality/blob/reflection/typetheory.agda the expressions are decorated with a lot more typing information. Seems like either you have to do this, or prove that you can reconstruct all the type information--I guess this is like translating the language you sketched into a language with the extra type info.

[Reid Barton]

Or maybe you could just use choice to pick a derivation witnessing well-typedness, but that sounds awkward later.

[Wojciech Nawrocki]

The way this kind of thing usually seems to be done is by induction on typing derivations (pf i guess?) precisely because from those you can mostly recover the types of subexpressions. The defeq (conversion) rule is an exception but one can then inspect its premise.

[Reid Barton]

In that case, though, it's awkward for pf to be a Prop.

[Reid Barton]

But, we can suppose we turn it into data.

[Reid Barton]

I'm also not sure whether I expect two different derivations of the same judgment to lead to equal translations into the model, or whether it necessarily matters.

[Wojciech Nawrocki]

Although the Agda project does seem to do define the interpretation just from the very-explicit syntax, e.g. for app. I'm guessing you only need the typing derivations to prove the "totality" (completeness?) of this interpretation.

[Reid Barton]

Yes, with the typing information in the syntax I think I can see how to do it

[Jannis Limperg]

Guillaume's approach uses a neat trick: all the assume statements in the partial interpretation collect preconditions which are needed to construct the model object. The output of [[ t ]] is then effectively a function from 'all preconditions needed for the interpretation to make sense' to a model object. I guess he then later proves that wellfoundedness of t implies that these preconditions are indeed satisfied. This should be equivalent to defining the interpretation over well-foundedness derivations in the first place, only with a better separation of concerns.

My hunch is that it won't be an issue to have the well-foundedness predicate in Prop, since you should only be using it to kill impossible cases and to build Props in the model. However, I'm not sure about this. If you can keep it in Prop, that's great because otherwise you'll indeed probably have to prove that different derivations are interpreted into the same object (or that well-foundedness is an hProp, but even then you only get a propositional equality rather than a definitional one).

[Reid Barton]

Hmm, I am a bit worried that in order to define the interpretation of app f x, one might need to conjure up not only a proof of a condition (some Prop), but actually the entire types of f and x (some data). But maybe that's actually not needed.

[Reid Barton]

Based on the way these natural models work, if I know the interpretation of f and x, I know the interpretations of their types. But the interpretations of A and Pi A B might not determine that of B, and I think that would prevent me from constructing the interpretation of f x.

[Reid Barton]

Anyways, I think I'm okay with assuming that we start from syntax that contains typing annotations (particularly as the Agda initiality project also does this), especially if it would be possible to tack on a preprocessor that reconstructs these annotations from a proof of type-correctness. (Isn't this basically what the Lean kernel has to do in order to type check an expression? expr doesn't contain these typing annotations.)