8
$\begingroup$

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$?

$\endgroup$
6
$\begingroup$

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).
$\endgroup$
  • 1
    $\begingroup$ Is there an important reason for it being a two-place relation (I suppose that refers to var1,t1/var2,t2)? At a glance it looks like it can be just cut in half, if the point is to demonstrate how to define a well-typedness relation. $\endgroup$ – Li-yao Xia Nov 27 at 17:10
  • 1
    $\begingroup$ As delightful as this answer is, I don't think it would hurt to have a bit of comments peppered in there (sacrilege!), especially since it is implemented in a specific software framework... $\endgroup$ – cody Nov 27 at 19:39
  • $\begingroup$ @JasonGross does it work to just use lists for telescopes? Or is there a way to capture well scopedness using PHOAS? Because later items can refer to the variables of the previous ones? $\endgroup$ – jmite Dec 1 at 17:19
  • 1
    $\begingroup$ @Li-yaoXia It does not have to be a two-place relation per-se, but if you plan to do anything with different variable instantiations, you'll find that a one-place relation is essentially useless. $\endgroup$ – Jason Gross Dec 1 at 22:27
  • $\begingroup$ @cody Indeed, comments would help. I shall aim to add some in the near future. (Others should feel free also to edit my answer with clarifying comments.) $\endgroup$ – Jason Gross Dec 1 at 22:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.