[TYPES] Writing syntactic models with "full information"

[Paul Blain Levy]

Dear Stefan,

Like you, I write [[ e ]] as an informal shorthand for [[ Gamma |- e:A ]], but this is not really correct.

For example, in simply typed lambda-calculus with zero type and boolean type, we have

[[ x:0 |- true:bool ]] = [[ x:0 |- false:bool ]]

but not

[[ |- true:bool ]] = [[ |- false:bool ]]

Best,
Paul



> On 21 May 2022, at 02:16, 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
>