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 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.