[TYPES] Writing syntactic models with "full information"

[Jonathan Chan]

In Compiling with Dependent Types
<https://urldefense.com/v3/__https://repository.library.northeastern.edu/files/neu:m044c025b/fulltext.pdf__;!!IBzWLUs!Qla5r5grH46LjmcHFZP8Maq1vuoJYgPdDZRX-3mVZiFwz-g45gSiUNp6NvkJriifrKMjK_PyhdqbE5rvXEYojKOxjZv_mWUgZVpf$ >
the translations that depend on the typing derivation (looking at 6.5 or
5.3 for instance) are defined as judgements, e.g.

Γ ⊢ A : κ' ⇝ *A*    Γ, x: A ⊢ κ : U ⇝ *κ*
----------------------------------
Γ ⊢ Πx: A. κ : U ⇝ Π*x*: *A*. *κ*

(using colour and styling to distinguish source/target, not entirely shown
here) but abbreviations are still given for the translations with Γ and U
being implicit, so it doesn't look like there's a way around verbosity vs.
abuse of notation here.
In the end, the theorem is still stated as Γ ⊢ e : τ ⇒ Γ* ⊢ e* : τ*, where
e* ≝ *e* s.t. Γ ⊢ e : τ ⇝ *e* and Γ* ≝ *Γ* s.t. ⊢ Γ ⇝ *Γ*, or using the ⟦·⟧
notation.

On Sun, 22 May 2022 at 06:29, Stefan Monnier <monnier at iro.umontreal.ca>
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
>
>