Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

["'Thorsten Altenkirch' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.com>]

[-- Attachment #1: Type: text/plain, Size: 10539 bytes --]

Hi Mike,

Certainly I would never claim that anybody’s work is meaningless, but I think that understanding and presentation can often by improved by using an appropriate level of abstraction. Often the obvious and naïve choice isn’t the best option. I experience this a lot with students who often use strings to represent syntactic objects like expressions. One of my mantras is “use trees not strings” – I even made a youtube video<https://youtu.be/7tCNu4CnjVc> about it.

Now most people accept that we should use trees to represent syntax but many still believe that typing should be extrinsic: ie we first define untyped syntax (using trees) and then a typing relation. In my view they make a similar mistake as my students using strings but on a different level. When I think about type theory I only want to talk about typed objects. Properties like subject reduction, admissibility of substitution etc are just noise caused by using an inappropriate level of abstraction. The essence of what we want to say becomes clear once we overcome these misleading traditions. This becomes even more essential once we deal with dependent types where the overhead often becomes unbearable.

Now people we say that we do need to implement and verify programs like type checkers. That is true and it is similar to the need for parsers to translate from strings to trees. My understanding of a parser is that it is the partial inverse of the printing function which translates trees into strings. Similarly a type checker is the partial inverse of a function from intrinsically typed terms to untyped terms. Hence yes we do need to implement the whole toolchain of parsers, typecheckers and when we implement a type system but its specification should happen on the top.

I haven’t worked on modal type theories but I suspect that they can and should be presented intrinsically. I refer to Jon’s comments on this topic.

Cheers,
Thorsten

From: Michael Shulman <shulman@sandiego.edu>
Date: Friday, 18 November 2022 at 02:36
To: Jon Sterling <jon@jonmsterling.com>
Cc: Thorsten Altenkirch (staff) <psztxa@exmail.nottingham.ac.uk>, andrej.bauer <andrej.bauer@andrej.com>, Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory
As far as the mathematical study of type theories and their models goes, that may be true.  But I believe that when talking about the way type theories are used in practice, either on paper or in a proof assistant, there is still a difference.

Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I want to evaluate f(3).  I don't write

f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.

Instead, I jump right to f(3) = 3^2+1, because substitution is an operation that happens immediately in my head, not a computational step analogous to 3^2 = 9.  Similarly, the user of a proof assistant never types or sees substitution as part of the syntax; it is an operation *on* syntax that happens behind the scenes.

Yes, this is a property of a particular *presentation* of a free structure rather than a property of the structure itself, but that doesn't intrinsically make it unimportant.  Groups and group presentations are both important.  Maybe you want to say that "a type theory" refers to the free structure rather than its presentation, but choosing to use words in that way doesn't by itself make "presentations of type theories" (or whatever you call them) less important.  Maybe you want to define an "admissible rule" to be a property that holds in the syntax but fails in some actual models; but that doesn't make "rules that hold in all models and can be made to hold in a particular presentation of the free model without being given explicitly as generating operations/equalities" (or whatever you call them) less important.

I do agree that Andrej's formulation sounds backwards.  In practice (in my experience) one doesn't write the rules down first and then try to figure out what kind of substitution is admissible.  Instead one decides what the substitution rule should be, and *then* (hopefully) works out a way of presenting the syntax to make that substitution rule admissible.  This is particularly tricky for modal type theories, where the categorically "obvious" rules do not admit substitution, and leads to the introduction of split contexts as used in the BFP paper.  I have trouble imagining how I could have written that paper if I had been forced to write explicit substitutions everywhere.  Thorsten and Jon, do you maintain that all the work that's gone into figuring out ways to present modal type theories with "admissible substitution" is meaningless?

On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling <jon@jonmsterling.com<mailto:jon@jonmsterling.com>> wrote:

Indeed, I echo Thorsten's comment — to put it another way, even being able to tell whether these rules are derivable or only admissible is like knowing what an angel's favorite TV show is (in other words, a form of knowledge that cannot be applied toward anything by human beings). At least for structural type theory, there is nothing worth saying that cannot be phrased in a way that does not depend on whether structural rules are admissible or derivable. It may be that admissiblity of structural rules starts to play a role in substructural type theory, however, but this is not my area of expertise.

It is revealing that nobody has proposed a notion of **model** of type theory in which the admissible structural rules do not hold; this would be the necessary form taken by any evidence for the thesis that it is important for structural rules to not be derivable. Absent such a notion of model and evidence that it is at all compelling/useful, we would have to conclude that worrying about admissibility vs. derivability of structural rules in the official presentation of type theory is fundementally misguided.


On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory wrote:
That depends on what presentation of Type Theory you are using. Your remarks apply to the extrinsic approach from the last millennium. More recent presentation of Type Theory built in substitution and weakening and use an intrinsic approach which avoids talking about preterms you don’t really care about.

https://dl.acm.org/doi/10.1145/2837614.2837638

Cheers,
Thorsten

From: homotopytypetheory@googlegroups.com<mailto:homotopytypetheory@googlegroups.com> <homotopytypetheory@googlegroups.com<mailto:homotopytypetheory@googlegroups.com>> on behalf of andrej.bauer@andrej.com<mailto:andrej.bauer@andrej.com> <andrej.bauer@andrej.com<mailto:andrej.bauer@andrej.com>>
Date: Tuesday, 15 November 2022 at 22:39
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com<mailto:homotopytypetheory@googlegroups.com>>
Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory
>  Does this also include the structural rules of type theory such as the substitution and weakening rules?

I would just like to point out that substutition and weakening typically are not part of the rules. They are shown to be admissible. In this spirit, the question should have been: what is the precise version of substitution and weakening (which is a special case of substitution) that is admissible in cohesive type theory?

With kind regards,

Andrej

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.

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.






--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com?utm_medium=email&utm_source=footer>.



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.




-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB7869899326D6A5C41CC20CB9CD099%40PAXPR06MB7869.eurprd06.prod.outlook.com.

[-- Attachment #2: Type: text/html, Size: 19143 bytes --]