Re: [TYPES] Writing syntactic models with "full information"

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