[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Stefan,
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!XatwrU-aKYd1XRa3nT193vk7ojHAJl14q2e1KUeemNUZzMN-wZ8bdlsnF09YA9guLUAsf2WsS7PI_7Yw7Jalw0amUAmD1UDAdw$
(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 wouldn't recommend it as a strictly better approach, but it has its
advantages.
I don't know if formalization in a proof-assistant is a part of what
you're doing.
Altenkirch & Kaposi have an Agda formalization where they build quotient
types using postulates & rewrite rules.
Today, to my understanding, it should in principle be possible to
instead do this in agda-cubical, although I don't think anyone has done
it (and it sounds like a very major effort).
FWIW, I have a formalization of multisorted algebraic theories and their
categories of models in agda-cubical (currently using quite some
termination pragmas rather than sized types) at
https://urldefense.com/v3/__https://github.com/anuyts/ctx-alg/__;!!IBzWLUs!XatwrU-aKYd1XRa3nT193vk7ojHAJl14q2e1KUeemNUZzMN-wZ8bdlsnF09YA9guLUAsf2WsS7PI_7Yw7Jalw0amUAmobT5gJw$
Best regards,
Andreas Nuyts
On 21.05.22 03:16, Stefan Monnier wrote:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I often write translations between PTS-style languages where the overall
structure of the translation can be represented by saying that an input
expression `e` is turned into an output `[e]` with a property like
Γ ⊢ e : τ
=>
[Γ] ⊢ [e] : [τ]
Or some variant of it, very much like Boulier et al. did in "The next
700 syntactical models of type theory".
But often my translation function [·] needs a bit more info than that
provided by an expression. E.g. it may need to know the expression's
type or the typing context in which it was found. So what I end up
doing is to define my translation function as taking a typing derivation
as input while still returning a mere expression.
Formally it means the above elegant property becomes:
Γ ⊢ e : τ (which implies that ∃ℓ. Γ ⊢ τ : Typeℓ)
=>
[Γ] ⊢ [Γ ⊢ e : τ] : [Γ ⊢ τ : Typeℓ]
which is much less elegant and less friendly for the reader (I did
something like that for example in "Inductive types deconstructed: the
calculus of united constructions" and this was mentioned as an oddity
by one of the reviewers, for example).
It also makes the presentation more verbose and harder to read, for
which the only way out I have found is to use cringe-worthy abuses of
notation where I might write [e] as a shorthand for [Γ ⊢ e : τ] where
the Γ and τ are presumed "obvious from context".
Has anyone here faced similar issues? What's a better approach?
Stefan
