<p>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:</p>

<pre><code>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 -&gt; expr)
| Abs (tx : expr) (f : var -&gt; 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) -&gt; @expr var1 (* t1 *) -&gt; @expr var1 -&gt; @expr var2 (* t2 *) -&gt; @expr var2 -&gt; Prop :=
| wf_Var {G t1 v1 t2 v2} : List.In (t1, v1, t2, v2) G -&gt; 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
    -&gt; (forall v1 v2,
           wf ((s1, v1, s2, v2) :: G)
              U (d1 v1) U (d2 v2))
    -&gt; 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
    -&gt; (forall v1 v2,
           wf ((s1, v1, s2, v2) :: G)
              (d1 v1) (f1 v1) (d2 v2) (f2 v2))
    -&gt; 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
    -&gt; wf G s1 x1 s2 x2
    -&gt; 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 _ =&gt; d1)) f1 (Pi s2 (fun _ =&gt; d2)) f2
    -&gt; wf G s1 x1 s2 x2
    -&gt; wf G d1 (App f1 x1) d2 (App f2 x2).
</code></pre>

CC BY-SA 4.0
2019-11-27T17:10:44.447Z
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.
Li-yao Xia
CC BY-SA 4.0
2019-11-27T19:39:19.940Z
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...
cody
CC BY-SA 4.0
2019-12-01T17:19:59.100Z
@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?
Joey Eremondi
CC BY-SA 4.0
2019-12-01T22:27:01.883Z
@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.
Jason Gross
CC BY-SA 4.0
2019-12-01T22:27:35.023Z
@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.)
Jason Gross
CC BY-SA 4.0
2019-12-01T22:31:39.363Z
@jmite Telescopes don't make any sense for extrinsic typing.  The well-scopedness is encoded in the fact that we require the bodies of `Pi` and `Abs` to be well-formed in the context `((s1, v1, s2, v2) :: G)` while we require `s1` and `s2` to be well-formed-related in the context `G`.  Hence the type of each variable must mention only variables that come later on in the list.
Jason Gross
CC BY-SA 4.0
2019-12-01T23:48:10.210Z
@JasonGross Right, but we want the G to be well formed, i.e. (x : Nat, y : z) is not a well-formed context. But I guess we just define another relation for this.
Joey Eremondi
CC BY-SA 4.0
2019-12-02T06:05:35.083Z
In that case you probably want to make this inductive mutual with one that says that `G` is a valid telescope, by requiring that each element be well-typed over the rest of the list, and then make this a condition of all the constructors here.  (You probably actually only need it for `wf_U` and `wf_Var`; I think everything else preserves this property on the context.)
Jason Gross
CC BY-SA 4.0
2019-11-26T21:58:03.677Z
2019-12-01T22:32:03.987Z
2019-12-01T22:32:03.987Z
Jason Gross
<p>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: <span class="math-container">$term : (V : Set) \to Set$</span>.</p>

<p><a href="http://adam.chlipala.net/papers/PhoasICFP08/" rel="noreferrer">The original PHOAS paper</a> describes a way to model System F using <em>intrinsic typing</em>: the syntax tree of a term is indexed by its type, so only well typed terms can be constructed.</p>

<p>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 <span class="math-container">$term\ (V : Set) :  term \to Set$</span>.</p>

<p>I'm wondering if there has been any work done on using PHOAS to model <em>extrinsically typed</em> 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 <span class="math-container">$\Gamma \vdash t : T$</span> typing rules.</p>

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

<reference-request><type-theory><lambda-calculus><type-systems><dependent-type>
PHOAS with extrinsic typing?
Joey Eremondi
# PHOAS with extrinsic typing?

(Asked by: username_0 on 2019-11-26)

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](http://adam.chlipala.net/papers/PhoasICFP08/) 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$?

**Tags:** reference-request, type-theory, lambda-calculus, type-systems, dependent-type


---

## 1 answers

### Answer by username_1 on 2019-11-26. Score: 6 | Accepted answer

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).

> **Comments:**
> **username_2**: 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.  
> **username_3**: 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...  
> **username_0**: @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?  
> **username_1**: @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.  
> **username_1**: @username_3 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.)  
> **username_1**: @jmite Telescopes don't make any sense for extrinsic typing.  The well-scopedness is encoded in the fact that we require the bodies of `Pi` and `Abs` to be well-formed in the context `((s1, v1, s2, v2) :: G)` while we require `s1` and `s2` to be well-formed-related in the context `G`.  Hence the type of each variable must mention only variables that come later on in the list.  
> **username_0**: @JasonGross Right, but we want the G to be well formed, i.e. (x : Nat, y : z) is not a well-formed context. But I guess we just define another relation for this.  
> **username_1**: In that case you probably want to make this inductive mutual with one that says that `G` is a valid telescope, by requiring that each element be well-typed over the rest of the list, and then make this a condition of all the constructors here.  (You probably actually only need it for `wf_U` and `wf_Var`; I think everything else preserves this property on the context.)  

---

