PHOAS in JS / HVM

phoas.md

ported from https://hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda

JS

const Lam = bod => lam => app => vah => lam(bod);
const App = fun => arg => lam => app => vah => app(fun)(arg);
const Var = exp => lam => app => vah => vah(exp);

const nz = v => nz => ns => nz(v);
const ns = t => nz => ns => ns(t);

const norm = expr => {
  let if_lam = bod => Lam(v => norm(bod(v)));
  let if_app = fun => arg => normapp(norm(fun))(arg);
  let if_var = exp => normvar(exp);
  return expr(if_lam)(if_app)(if_var); };

const normapp = fun => arg => {
  let if_lam = f_bod => norm(f_bod(ns(arg)));
  let if_app = f_fun => f_arg => App(fun)(norm(arg));
  let if_var = f_exp => {
    let if_nz = f_f => App(fun)(norm(arg));
    let if_ns = f_f => norm(App(f_f)(arg))
    return f_exp(if_nz)(if_ns); };
  return fun(if_lam)(if_app)(if_var); };

const normvar = exp => {
  let if_nz = f => Var(exp);
  let if_ns = f => norm(f);
  return exp(if_nz)(if_ns); };

const cut = expr => {
  let if_lam = bod => Lam(v => cut(bod(nz(v))));
  let if_app = fun => arg => App(cut(fun))(cut(arg));
  let if_var = exp => {
    let if_nz = f => Var(f);
    let if_ns = f => cut(f);
    return exp(if_nz)(if_ns); };
  return expr(if_lam)(if_app)(if_var); };

const show = (term, depth = 0) => {
  let if_lam = bod => {
    const body = show(bod(depth), depth + 1);
    return `λv${depth}. ${body}`;
  };
  let if_app = fun => arg => {
    const f = show(fun, depth);
    const x = show(arg, depth);
    return `(${f} ${x})`;
  };
  let if_var = exp => `v${exp}`;
  return term(if_lam)(if_app)(if_var);
};

var id = Lam(x => Var(x));
var c2 = Lam(f => Lam(x => App(Var(f))(App(Var(f))(Var(x)))));
var k2 = Lam(f => Lam(x => App(Var(f))(App(Var(f))(Var(x)))));

var term = App(c2)(c2);
var term = cut(norm(term));

console.log(show(term));

HVM

Lam = λnam λbod λlam λapp λvar (lam nam bod)
App = λfun λarg λlam λapp λvar (app fun arg)
Var = λnam      λlam λapp λvar (var nam)

View = λterm
  let clam = λnam λbod ((Lam) nam λx ((View) (bod ((Var) nam))))
  let capp = λfun λarg ((App) ((View) fun) ((View) arg))
  let cvar = λnam ((Var) nam)
  (term clam capp cvar)
  
Eval = λterm
  let clam = λnam λbod ((Lam) nam λx ((Eval) (bod x)))
  let capp = λfun λarg ((DoApp) ((Eval) fun) ((Eval) arg))
  let cvar = λnam ((Var) nam)
  (term clam capp cvar)

DoApp = λfun λarg
  let clam = λfnam λfbod λarg (fbod arg)
  let capp = λffun λfarg λarg ((App) ((App) ffun farg) arg)
  let cvar = λfnam       λarg ((App) ((Var) fnam) arg)
  (fun clam capp cvar arg)

Main = ((View) ((Eval) ((App)
  ((Lam) 0 λf ((Lam) 1 λx ((App) f ((App) f x))))
  ((Lam) 0 λx x))))

So after thinking about what makes PHOAS work I realized we can just do this:

Lam =      λbod λlam λapp λvar (lam bod)
App = λarg λfun λlam λapp λvar (app arg fun)
Var = λexp      λlam λapp λvar (var exp)

View = λd λterm
  let clam = λbod      λd (Lam (View (+ 1 d) (bod (Var d))))
  let capp = λarg λfun λd (App (View d arg) (View d fun))
  let cvar = λexp      λd (Var exp)
  (term clam capp cvar d)
  
Eval = λterm
  let clam = λbod (Lam λx (Eval (bod (Var x))))
  let capp = λarg λfun (DoApp (Eval arg) (Eval fun))
  let cvar = λexp exp
  (term clam capp cvar)

DoApp = λfun λarg
  let clam = λfbod       λarg (fbod arg)
  let capp = λfarg λffun λarg (App (App farg ffun) arg)
  let cvar = λfexp       λarg (App (Var fexp) arg)
  (fun clam capp cvar arg)

ID    = (Lam λx x)
C0    = (Lam λf (Lam λx x))
C1    = (Lam λf (Lam λx (App f x)))
C2    = (Lam λf (Lam λx (App f (App f x))))
C3    = (Lam λf (Lam λx (App f (App f (App f x)))))
C4    = (Lam λf (Lam λx (App f (App f (App f (App f x))))))
False = (Lam λt (Lam λf f))
True  = (Lam λt (Lam λf t))
Not   = (Lam λb (App (App b False) True))

Main = (Eval (App (App C3 Not) True))

the only difference is that we add a Var constructor on the lam case of Eval, and remove that Var on the var case. I believe the issue was that Eval was reaching variables somehow caused disconnected graphs. for example, Eval (Lam (λx x)) would result in Lam (λx (Eval x)) - notice the Eval call stuck there. I believe that, since x was not substituted, and since Eval is recursive, it would expand infinitely. when we used View, this would be "fixed" because View substitutes x, but only for variables that are part of the normal form of the original program. so, if the input term itself had parts that got disconnected, then View would never be able to substitue some x's, causing Eval's somewhere to unroll infinitely. now, by using the Var constructor as a "guard" inside Eval itself, we will have that Eval (Lam (λx x)) will result in (Lam (λx (Eval (Var x))) , which returns (Lam (λx x)), i.e., Eval always disappears before having the change of expanding infinitely, and it doesn't need another function (like View) to "fix" it