Parametric Higher-order Abstract Syntax and Normalization by Evaluation

Using Coq
1

Recently, I was reading about Parametric Higher-order Abstract Syntax (PHOAS) and found that its a neat way of representing binders for, say, simply-typed lambda calculus. Using such a representation, I decided to start working on a simple interpreter using the Normalization by Evaluation (NBE) technique. Interestingly enough, I found it to be a really challenging exercise.

I was able to implement the reify and reflect functions, however I got stuck around the implementation of a suitable method which would allow me to map lambda terms into their semantic denotations, elegantly forcing the simultaneous evaluation of beta redexes. The problem seems to centered around the PHOAS abstractions – had I used, say, de Bruijn indices, I could create an explicit free variable context and pass it down the recursion, eventually matching variables with their binders (much like described in Adam Chlipala’s Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant). Afterwards, a reification of the semantic denotation would give me back the desired beta normal form (perhaps even in a dedicated datatype). In the PHOAS representation, however, I seem to be missing how I could achieve this goal.

Is there a clever way of using both PHOAS and NBE in order to create an interpreter for the simply-typed lambda calculus? Is there a “best practice” around the two?

1 Like
2

You probably need to use a well chosen instance of the parameter for your PHOAS syntax (the type family of variables) so that you actually carry the semantic context. Without a more concrete presentation of your problem, it’s difficult to say more.

In my experience, the point where you get stuck is when trying to prove the parametricity of your syntax PHOAS (unless you assume it as an axiom).

3

I represent simple types the usual way (here with a single ground type #o):

Inductive type : Set :=
  | Ground : type
  | Arrow  : type -> type -> type.

With this definition, terms are represented as follows:

Variable var : type → Set.

Inductive term : type → Set :=
| Var : forall α, var α → term α
| App : forall α β, term (α → β) → term α → term β
| Abs : forall α β, (var α → term β) → term (α → β).

The semantical denotation of terms is represented using a recursive fixpoint definition.

Fixpoint sem (σ : type) : Set :=
match σ with
| α → β => sem α → sem β
| #o => term var #o
end.

Now, with such definitions, I have reify and reflect functions (written in the usual manner), which allow me to map terms of type σ into sem σ (and vice versa). The question is, how to map term σ into sem σ while also evaluating the term in the target language, instead of using object level substitutions?

4

You can write the following function sem_term

Section sem.
  Variable var : type -> Set.

  Fixpoint sem (σ : type) : Set :=
  match σ with
  | α --> β => sem α -> sem β
  | #o => term var #o
  end.

  Fixpoint sem_term {α} (t:term sem α)  {struct t} : sem α :=
    match t with
    | Var _ α x => x
    | App _ α β t1 t2 => sem_term t1 (sem_term t2)
    | Abs _ α β t1 => fun x => sem_term (t1 x)
    end.
End sem.

Now if you have a parametric element of term, that is t : forall var : type -> Set, term var a you can just take fun var => sem_term var (t (sem var)).

1 Like
5

@kyod Thank you - it’s a really marvelous solution!

I guess that I was missing the bigger point that the parametric variable function can be used to ‘tag’
variables with arbitrary types in Set, in particular sem σ. Consequently, I can carry the semantic context
for ‘free’, choosing a suitable instantiation for the parametric type – a truly elegant idea!