Skip to content

Instantly share code, notes, and snippets.

@VictorTaelin

VictorTaelin/phoas.md

Last active March 10, 2024 19:28
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save VictorTaelin/eeac9b51b664cec67c2009c9472d4ce5 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save VictorTaelin/eeac9b51b664cec67c2009c9472d4ce5 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. VictorTaelin renamed this gist Oct 20, 2023. 1 changed file with 37 additions and 0 deletions.
    37 changes: 37 additions & 0 deletions phoas.js → phoas.md
    View file
    Original file line number Diff line number Diff line change
    @@ -1,3 +1,8 @@
    ported from https://hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda

    JS

    ```javascript
    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);
    @@ -56,3 +61,35 @@ 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))))
    ```

  2. VictorTaelin created this gist Oct 20, 2023.
    58 changes: 58 additions & 0 deletions phoas.js
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,58 @@
    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));