1
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Apoorv
    Commented Mar 3, 2023 at 20:34

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.