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?

Improve this question
$\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
    Mar 3 at 20:34

0

Reset to default

Your Answer

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