The Coq mailing list

[Joey Eremondi <joey.eremondi AT gmail.com>]

Disclaimer: x-posted at https://cstheory.stackexchange.com/questions/45924/phoas-with-extrinsic-typing

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) -> 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  ->  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 |- 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  ->  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 `?

Thanks!