[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.altenki...@nottingham.ac.uk> Sent: Wednesday, May 25, 2022 5:14 AM To: Jason Hu<mailto:fdhzs2...@hotmail.com>; Stefan Monnier<mailto:monn...@iro.umontreal.ca>; Andreas Nuyts<mailto:andreasnu...@gmail.com> Cc: types-list@lists.seas.upenn.edu<mailto:types-list@lists.seas.upenn.edu> Subject: Re: [TYPES] Writing syntactic models with "full information" From: Types-list <types-list-boun...@lists.seas.upenn.edu> on behalf of Jason Hu <fdhzs2...@hotmail.com> Date: Wednesday, 25 May 2022 at 09:58 To: Stefan Monnier <monn...@iro.umontreal.ca>, Andreas Nuyts <andreasnu...@gmail.com> Cc: types-list@lists.seas.upenn.edu <types-list@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:monn...@iro.umontreal.ca> Sent: Monday, May 23, 2022 3:51 PM To: Andreas Nuyts<mailto:andreasnu...@gmail.com> Cc: types-list@lists.seas.upenn.edu<mailto:types-list@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.
