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