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))))
From https://stackoverflow.com/questions/77332495/is-it-possible-using-phoas-to-evaluate-a-term-to-normal-form-and-then-stringi
A better version on HVM is:
{-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} import Data.Char data Term v t where Lam :: (v a -> Term v b) -> Term v (a -> b) App :: Term v (a -> b) -> Term v a -> Term v b Var :: v t -> Term v t data Exp t = Exp (forall v. Term v t) data FreeTerm v a = Pure (v a) | Free (Term (FreeTerm v) a) norm :: Term (FreeTerm v) a -> Term (FreeTerm v) a norm (Lam bod) = Lam (\v -> norm (bod v)) norm (App fun arg) = case norm fun of Lam f_bod -> f_bod (Free arg) fun2 -> App fun2 (norm arg) norm (Var (Pure x)) = Var (Pure x) norm (Var (Free x)) = norm x eval :: Exp a -> Exp a eval (Exp x) = Exp (cut (norm x)) cut :: Term (FreeTerm v) a -> Term v a cut (Lam bod) = Lam (\x -> cut (bod (Pure x))) cut (App fun arg) = App (cut fun) (cut arg) cut (Var (Pure x)) = Var x cut (Var (Free x)) = cut x data Name a = Name Int showTermGo :: Int -> Term Name t -> String showTermGo d (Lam a) = "@x" ++ show d ++ " " ++ showTermGo (d+1) (a (Name d)) showTermGo d (App f x) = "(" ++ showTermGo d f ++ " " ++ showTermGo d x ++ ")" showTermGo _ (Var (Name i)) = "x" ++ show i showTerm :: Exp t -> String showTerm (Exp e) = showTermGo 0 e main :: IO () main = do let c2 = (Lam (\f -> (Lam (\x -> (App (Var f) (App (Var f) (Var x))))))) let xp = (App c2 c2) putStrLn $ "term: " ++ showTerm (Exp xp) putStrLn $ "norm: " ++ showTerm (eval (Exp xp))Translated to HVM, we have: