[TYPES] Writing syntactic models with "full information"

[Jason Hu]

Hi Thorsten,

I value your and your students’ work because I looked into it and learned how things can be done intrinsically. IMO, intrinsic and extrinsic styles are only distinguished by what phase semantics are given in. I don’t think both historically and technically, either style is superior to or more proper than the other. To me, it’s like stepping forward with the left foot or the right foot first. Nevertheless, I do have preference, not to mention I have greatly benefited from the “stone axe” recently.  So there is nothing depressing here, more like a matter of choice and taste.


From: Thorsten Altenkirch<mailto:Thorsten.Altenkirch at nottingham.ac.uk>
Sent: Wednesday, May 25, 2022 5:14 AM
To: Jason Hu<mailto:fdhzs2010 at hotmail.com>; Stefan Monnier<mailto:monnier at iro.umontreal.ca>; 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"



From: Types-list <types-list-bounces at LISTS.SEAS.UPENN.EDU> on behalf of Jason Hu <fdhzs2010 at hotmail.com>
Date: Wednesday, 25 May 2022 at 09:58
To: Stefan Monnier <monnier at iro.umontreal.ca>, Andreas Nuyts <andreasnuyts at gmail.com>
Cc: types-list at lists.seas.upenn.edu <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 ]

I don’t know how intrinstically typed formulation can be used to express universes, at least I have not seen one.
There is no problem and we have done it many times
U : Ty G
El : Tm G U -> Ty G

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.
See our forthcoming TYPES talk (presented by Artem Shinkarov).

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.
You have to perform lots of Gymnastics when you are stuck in the last millennium formulation of Type Theory. The intrinsic syntax of type theory are just the initial categories with families, syntax and semantics fit perfectly.
I have started with the extrinsic formulation of type theory (see my PhD), beta-reduction and single-place substitution. In each instance we learnt how to do things properly: intrinsic, equality, parallel substitution. And then you come and say: “I prefer the stone axe”. It is depressing.
Thorsten



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$><https://urldefense.com/v3/__https:/dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$%3chttps:/urldefense.com/v3/__https:/dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$%3e>
> (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





This message and any attachment are intended solely for the addressee

and may contain confidential information. If you have received this

message in error, please contact the sender and delete the email and

attachment.



Any views or opinions expressed by the author of this email do not

necessarily reflect the views of the University of Nottingham. Email

communications with the University of Nottingham may be monitored

where permitted by law.