[TYPES] Writing syntactic models with "full information"

Stefan Monnier monnier at iro.umontreal.ca
Mon May 23 11:39:01 EDT 2022


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$ 
> (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



More information about the Types-list mailing list