[TYPES] Writing syntactic models with "full information"

[Stefan Monnier]

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