[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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, monn...@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 >