Zulip Chat Archive

Stream: Type theory

Topic: modeling MLTT


view this post on Zulip 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 CC whose objects we think of as contexts;
  • we have a presheaf Ty:CopSet\mathsf{Ty} : C^{\mathrm{op}} \to \mathrm{Set} where we think of Ty(Γ)\mathsf{Ty}(\Gamma) as the types in context Γ\Gamma;
  • we have a presheaf Tm:CopSet\mathsf{Tm} : C^{\mathrm{op}} \to \mathrm{Set}, together with a natural transformation p:TmTyp : \mathsf{Tm} \to \mathsf{Ty} where we think of those elements of Tm(Γ)\mathsf{Tm}(\Gamma) which map to a given ATy(Γ)A \in \mathsf{Ty}(\Gamma) as the terms of type AA (in the context Γ\Gamma).

view this post on Zulip Reid Barton (May 14 2020 at 11:51):

Then I want to assign

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 14 2020 at 12:02):

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

view this post on Zulip Reid Barton (May 14 2020 at 12:13):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 14 2020 at 12:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 14 2020 at 12:56):

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

view this post on Zulip Reid Barton (May 14 2020 at 12:56):

But, we can suppose we turn it into data.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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