PHOAS with extrinsic typing?

Question

Parameterized Higher Order Abstract Syntax (PHOAS) is a representation of syntax trees that allows the host language's binding to be used to represent binding in the language being modelled, while fulfilling the strict positivity requirements that most dependently typed languages impose . This is done by modelling the type of variables as a type parameter: $term : (V : Set) \to Set$.

The original PHOAS paper describes a way to model System F using intrinsic typing: the syntax tree of a term is indexed by its type, so only well typed terms can be constructed.

The problem I have is that, I would like to use PHOAS to model a dependently typed calculus. Having terms and types be in the same syntactic category means that (as far as I can see) the extrinsic approach is not feasible: we can't have $term\ (V : Set) : term \to Set$.

I'm wondering if there has been any work done on using PHOAS to model extrinsically typed languages: that is, where our syntax allows ill-typed terms to be formed, and we have a separately defined relation between telescopes, terms and types, i.e. traditional $\Gamma \vdash t : T$ typing rules.

In particular, I'm unsure how to model a term whose free variables all come from the given telescope. PHOAS uses $Term_0 = \forall V . term\ V$ to model closed terms, and $Term_1 = \forall V . (V \to term\ V)$ to model terms with one open variable. How can I generalize this to arbitrary telescopes? Should my typing rules refer to $term$s or $Terms$?

Answer 1

The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS. The main subtlety is how to handle reduction at the type level. Here's a start of a two-place relation for well-typed in Coq:

Require Import Coq.Lists.List.
Reserved Infix "@" (left associativity, at level 11).
Local Open Scope list_scope.

Inductive expr {var : Set} : Set :=
| Var (v : var)
| U : expr
| Pi (s : expr) (d : var -> expr)
| Abs (tx : expr) (f : var -> expr)
| App (f x : expr).
Declare Scope expr_scope.
Delimit Scope expr_scope with expr.
Infix "@" := App : expr_scope.

Inductive wf {var1 var2} : list ((@expr var1 (* t1 *)) * var1 * (@expr var2) (* t2 *) * var2) -> @expr var1 (* t1 *) -> @expr var1 -> @expr var2 (* t2 *) -> @expr var2 -> Prop :=
| wf_Var {G t1 v1 t2 v2} : List.In (t1, v1, t2, v2) G -> wf G t1 (Var v1) t2 (Var v2)
| wf_U {G} : wf G U U U U
| wf_Pi {G s1 s2 d1 d2}
  : wf G U s1 U s2
    -> (forall v1 v2,
           wf ((s1, v1, s2, v2) :: G)
              U (d1 v1) U (d2 v2))
    -> wf G U (Pi s1 d1) U (Pi s2 d2)
| wf_Abs {G s1 s2 d1 d2 f1 f2}
  : wf G U s1 U s2
    -> (forall v1 v2,
           wf ((s1, v1, s2, v2) :: G)
              (d1 v1) (f1 v1) (d2 v2) (f2 v2))
    -> wf G (Pi s1 d1) (Abs s1 f1) (Pi s2 d2) (Abs s2 f2)
| wf_App {G s1 d1 s2 d2 f1 x1 f2 x2}
  : wf G (Pi s1 d1) f1 (Pi s2 d2) f2
    -> wf G s1 x1 s2 x2
    -> wf G (App (Abs s1 d1) x1) (App f1 x1) (App (Abs s2 d2) x2) (App f2 x2)
| wf_App_nd {G s1 d1 s2 d2 f1 x1 f2 x2}
  : wf G (Pi s1 (fun _ => d1)) f1 (Pi s2 (fun _ => d2)) f2
    -> wf G s1 x1 s2 x2
    -> wf G d1 (App f1 x1) d2 (App f2 x2).