# Is it possible to define beta reduction for PHOAS?

I'm using Parametric Higher-Order Abstract Syntax (PHOAS) as a representation for untyped lambda calculus in OCaml:

type 'x term_def =
| Lam of ('x -> 'x term_def)
| Appl of 'x term_def * 'x term_def
| Var of 'x

type term = { t : 'x. 'x term_def }


My incentive is to rule out exotic terms that pattern-match on a bound variable. I don't particularly care about strong normalization since my goal is to only implement untyped lambda calculus.

Defining print is pretty straightforward:

let print lvl =
let rec go lvl = function
| Lam f -> "(λ" ^ go (lvl + 1) (f lvl) ^ ")"
| Appl (m, n) -> "(" ^ go lvl m ^ " " ^ go lvl n ^ ")"
| Var x -> string_of_int x
in
fun { t } -> (go lvl) t


However, I'm a bit stuck with implementing beta reduction. With vanilla HOAS, I could do something like this:

type term =
| Lam of (term -> term)
| Appl of term * term
| FreeVar of int

let rec eval = function
| Lam f -> Lam (fun n -> eval (f n))
| Appl (m, n) -> (
match (eval m, eval n) with Lam f, n -> eval (f n) | m, n -> Appl (m, n))
| FreeVar x -> FreeVar x


But when I tried to do that in terms of PHOAS, I couldn't make type checking pass. Is it possible to implement beta reduction for PHOAS (in a Turing-complete language such as OCaml) without first converting PHOAS to some other representation? Maybe I'm missing something?

• maybe you want is something like: Appl : ('x -> 'y) term * 'x term -> 'y term? Basically encode it as a GADT for type inference to be happy. Commented Mar 3, 2023 at 20:34