[TYPES] Writing syntactic models with "full information"

[Craig McLaughlin]

Hi Stefan,

I see quite a number of logical relations-based models define functions 
of the form [| Γ ⊢ e : τ |] which then use the context and type of e as 
needed. Such a function could be seen to be defined on well-typed and 
well-scoped expressions[1] where (the usually implicit) Γ and τ are made 
explicit. Of course, if you are dealing with extrinsic (as opposed to 
intrinsic above) syntax this viewpoint may be of little help.

[1] - Allais et al. “A Type and Scope Safe Universe of Syntaxes with 
Binding, Their Semantics and Proofs” 9, no. 4 (n.d.): 30.

On 21/5/22 11: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
>