Actually, I think I disagree on a deeper level: To say that a model (in the sense of algebraic theories) respects the equational theory of a language, does not *only* mean that the evaluation of syntactic programs in that model respects equality. It also means that the evaluation of programs containing subterms that are actually quoted elements from the model, respects equality. (Algebraically speaking, the model should be an Eilenberg-Moore-algebra for the quotiented version of the term monad.) But since *admissible* substitution is undefined for such quoted elements, this cannot be stated (the term monad cannot be quotiented satisfactorily). So while it's true that "you can still check in the admissible-subst scenario whether the interpretation function respects the beta law on all terms", this is a much weaker property than respecting the equational theory of the language. But I agree that my statement "Prettyprinting indeed disrespects βη-equality." made it sound as evidence of something, whereas I was merely arguing that it's a drawback that you cannot reasonably complain about if you were looking for a model without substitution in the first place. On 01.12.22 16:57, Andreas Nuyts wrote: > Right, but when looking for a model that misses a substitution > operation and is not contrived, you're not going to find it among the > models that try to respect equality, because that isn't even statable > in the model. When you drop both the requirement of supporting > substitution, and of respecting equality, then your search space has > grown enough that prettyprinters can be found in it. > > On 01.12.22 16:54, Jon Sterling wrote: >> The issue regarding the beta law is kind of spurious: one of course >> states the beta law using the ADMISSIBLE substitution action. The >> problem with pretty printing is that it is indeed not satisfying the >> beta law but this has absolutely nothing to do with substitution — >> you can still check in the admissible-subst scenario whether the >> interpretation function respects the beta law on all terms, and in >> this case it just happens that it doesn’t. >> >>> On Dec 1, 2022, at 3:40 PM, Andreas Nuyts >>> wrote: >>> >>>  Hi everyone, >>> >>> I finally found time to read up on this lengthy conversation. >>> >>> Jon wrote: >>> >>> 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. >>> >>> >>> I think, on the contrary, that such models are not acknowledged as >>> being models, because the language without substitution is in >>> general not really the language of interest. An example of a model >>> disrespecting substitution is the prettyprinter by Allais, Atkey, >>> Chapman, McBride & McKinna (2021): >>> https://doi.org/10.1017/S0956796820000076 >>> Indeed, substitution is no longer possible after prettyprinting, but >>> all other language constructs are supported. Note that if a >>> substitution operation is unavailable in a model, then the β-rule >>> for functions cannot even be stated in that model, let alone asked >>> to hold. So a model that fails to have a substitution operation >>> necessarily also disrespects the equational theory of a language >>> with such a β-rule. Prettyprinting indeed disrespects βη-equality. >>> >>> Mike wrote: >>> >>> MTT is also not equivalent to split-context theories, and IMHO >>> is less pleasant to work with in practice. >>> >>> >>> I'm reluctant to postulate here that any split-context theory is >>> equivalent to some instance of MTT, but I would be quite surprised >>> if you ever face any practical problems when abandoning a >>> split-context system in favour of MTT. If you're thinking in >>> particular about a system with crisp and non-crisp variables: such a >>> system is implemented by Andrea in agda-flat. At the last Agda >>> meeting, we have been investigating how mature the current modality >>> system in Agda is and how feasible it is to support full MTT. One >>> thing we observed is that - of all the parallel modality systems >>> implemented in Agda - the cohesive one (of which only the flat and >>> non-flat modalities are exposed to the user) is actually the one >>> that adheres to the discipline of MTT (by having a third "squash" >>> modality that effectively removes variables from the context). >>> Both regarding usability and equivalence, do not be misled by the >>> invasive-looking locks. These locks have two confluent histories: >>> - there is a history of fitch-style logics, >>> - there is a history of modal logics with left-division. When >>> implementing Menkar, which was intended as a proof assistant for >>> general multimode systems with left division, I observed at some >>> point that the left division of all modalities in the context >>> actually never needs to be computed and can thus be regarded as a >>> context /constructor/, rather than as an operation (i.e. >>> admissibility of left division was not required, in none of the >>> senses of the word mentioned so far). Modal Agda does use an eagerly >>> computed left division. These systems with left division are very >>> closely related to dual context systems. >>> >>> I think usability is hard to judge because there isn't yet good tool >>> support to experiment with. But I believe that it can grow on the >>> user. A lock simply means "we've moved into a modal subterm". The >>> position of the lock in the context is important in order to keep >>> track of which variables were introduced before/after moving into >>> that modal subterm. When using a variable, you just need to make >>> sure that the variable's modal annotation is ≤ the composition of >>> the locks, i.e. the modality of the position where we currently are >>> and where we want to use the variable. >>> >>> I am happy to discuss this matter further if you have any questions >>> or doubts. >>> >>> Best regards, >>> Andreas Nuyts >>> >>> On 18.11.22 18:14, Michael Shulman wrote: >>>> That's an interesting question.  I was thinking of operations and >>>> equalities, and annotations are neither of those, but I can see >>>> that they're somewhat similar in spirit.  But I find it even more >>>> difficult to imagine how to define this phenomenon precisely in a >>>> way that would include them... >>>> >>>> On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling >>>> wrote: >>>> >>>> On 18 Nov 2022, at 11:56, Michael Shulman wrote: >>>> >>>> > Thanks.  It does sound like we mostly agree.  I would >>>> probably argue that >>>> > even for type theories in development, where we don't yet >>>> know that full >>>> > definitional equality is decidable -- or intrinsically >>>> ill-behaved type >>>> > theories like Lean, or Agda with non-confluent rewrite rules, >>>> where >>>> > definitional equality *isn't* decidable -- there is still >>>> value in being >>>> > able to reduce just substitutions.  But I think that's a >>>> relatively minor >>>> > point. >>>> > >>>> > Maybe we can work out some way to use words so that this >>>> underlying >>>> > agreement is evident.  For instance, can we find a third word >>>> to use >>>> > alongside "admissible" and "derivable" to refer to >>>> operations/equalities >>>> > like substitution and its theory, which hold in all >>>> reasonable models, and >>>> > can be made admissible in some presentations, but more >>>> importantly can be >>>> > eliminated in an equality-checking algorithm? >>>> > >>>> >>>> Cool, it's a relief to start getting this cleared up! I really >>>> agree with you that there is a need for terminology to describe >>>> the situation you mention, and maybe even more, there is a need >>>> to define this phenomenon... >>>> >>>> I wonder if we can think of more concrete examples of this. For >>>> instance, in many versions of syntax (like bidirectional ones) >>>> we can choose to drop certain annotations because they will be >>>> available as part of the flow of information in the elaboration >>>> algorithm. Would these be an example of the phenomenon you are >>>> describing, or is it something different? >>>> >>>> Best, >>>> Jon >>>> >>>> -- >>>> 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/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com >>>> . >>> > -- 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/74bff49b-91b0-8b55-5cb1-10ce815ce470%40gmail.com.