[TYPES] Writing syntactic models with "full information"

[Jason Hu]

I don’t know how intrinstically typed formulation can be used to express universes, at least I have not seen one.

With intrinsic formulation, one must index an Exp with a context and a type, but with MLTT-style dependent types, a type is also an Exp, which requires an Exp to be indexed by an Exp.

Is it then possible to tackle it by Tarski-style universes, where types and terms are separated? It sounds to me intrinsic formulation conflicts with Russell-style universes.

In my opinion, I much prefer extrinsic formulation, where we have pre-syntax and typing judgments there to give semantics later. This way avoids many type-level gymnastics that often people do not want to handle.


From: Stefan Monnier<mailto:monnier at iro.umontreal.ca>
Sent: Monday, May 23, 2022 3:51 PM
To: Andreas Nuyts<mailto:andreasnuyts at gmail.com>
Cc: types-list at lists.seas.upenn.edu<mailto:types-list at lists.seas.upenn.edu>
Subject: Re: [TYPES] Writing syntactic models with "full information"

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Andreas Nuyts [2022-05-23 10:44:19] wrote:
> I would suggest the use of intrinsically typed syntax, defined as a quotient
> inductive-inductive type, see
> Altenkirch and Kaposi, Type theory in type theory using quotient inductive
> types
> https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$<https://urldefense.com/v3/__https:/dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$>
> (and further work by either author).
> This way, omitting context and type is not cringe-worthy but formally
> justified in the sense that there is only a single (object-language) context
> and a single (object-language) type in which the (object-language)
> expression e is well-typed (in the metalanguage).

I do tend to presume in my head that my terms are intrinsically typed,
which is why I'm tempted to play fast and loose and abuse notations with
things like [e] meaning [Γ ⊢ e : τ], but at the same time I'm not
completely comfortable relying on such a QIIT representation, because it
doesn't seem sufficiently well established yet.

E.g. I've never seen this used in an article.  Obviously, there has to
be a first for everything, but I'd rather not have to first give a bit of
background on QIIT and show how to define my language using them before
I can move on to the actual presentation of my translation.

Also I often find myself working with languages that offer some form of
impredicativity or some other feature for which I don't have a clear
intuition whether I can assume that it is compatible with QIIT.


        Stefan