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