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.