Stream: Type theory

Topic: modeling MLTT

Reid Barton (May 14 2020 at 11:46):

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 (May 14 2020 at 11:51):

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 (May 14 2020 at 11:52):

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 (May 14 2020 at 12:02):

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

Reid Barton (May 14 2020 at 12:13):

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

Reid Barton (May 14 2020 at 12:16):

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 (May 14 2020 at 12:18):

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 (May 14 2020 at 12:19):

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 (May 14 2020 at 12:21):

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 (May 14 2020 at 12:43):

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

Reid Barton (May 14 2020 at 12:48):

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 (May 14 2020 at 12:49):

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

Wojciech Nawrocki (May 14 2020 at 12:53):

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 (May 14 2020 at 12:56):

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

Reid Barton (May 14 2020 at 12:56):

But, we can suppose we turn it into data.

Reid Barton (May 14 2020 at 13:14):

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 (May 14 2020 at 13:15):

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 (May 14 2020 at 13:17):

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

Jannis Limperg (May 14 2020 at 13:39):

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 (May 14 2020 at 13:45):

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 (May 14 2020 at 14:25):

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 (May 14 2020 at 14:49):

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.)

Last updated: May 08 2021 at 22:13 UTC