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))))