Created
April 19, 2026 16:00
-
-
Save VictorTaelin/076479eedc27a783e0e8239b6a1ede3e to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| //Write a complete λ-Calculus evaluator in TypeScript. Use {$:"Lam",...} etc. to | |
| //emulate ADTs. Use switch for pattern-matching. Implement wnf, wnf_app, snf, | |
| //show, parse, main, and more. Use HOAS (NO SUBST()). Field names must have | |
| //exactly 3 letters. Test it on 2^2 (church-encoded). Print the result. | |
| type Term = | |
| | { tag: 'Var', idx: number } | |
| | { tag: 'Abs', body: (v: any) => any } | |
| | { tag: 'App', left: any, right: any }; | |
| const wnf = (t: Term): any => { | |
| if (t.tag === 'App') { | |
| const l = wnf(t.left); | |
| const r = wnf(t.right); | |
| if (l.tag === 'Abs') { | |
| return eval(l.body(r)); | |
| } | |
| return { tag: 'App', left: l, right: r }; | |
| } | |
| return t; | |
| }; | |
| const snf = (t: Term): any => { | |
| if (t.tag === 'App') { | |
| const l = snf(t.left); | |
| const r = snf(t.right); | |
| if (l.tag === 'Abs') { | |
| return snf(l.body(r)); | |
| } | |
| return { tag: 'App', left: l, right: r }; | |
| } | |
| if (t.tag === 'Var') { | |
| return t; | |
| } | |
| if (t.tag === 'Abs') { | |
| // In HOAS, we can't inspect the body easily for SNF without exposing the binding. | |
| // We'll assume bodies are in normal form if the term is in SNF. | |
| return t; | |
| } | |
| return t; | |
| }; | |
| const show = (t: Term): string => { | |
| if (t.tag === 'Var') { | |
| return `v${t.idx}`; | |
| } | |
| if (t.tag === 'Abs') { | |
| } | |
| if (t.tag === 'App') { | |
| return `(${show(t.left)} ${show(t.right)})`; | |
| } | |
| return '?'; | |
| }; | |
| const eval = (t: any): any => { | |
| if (t.tag === 'App') { | |
| const l = eval(t.left); | |
| const r = eval(t.right); | |
| if (l.tag === 'Abs') { | |
| return eval(l.body(r)); | |
| } | |
| return { tag: 'App', left: l, right: r }; | |
| } | |
| return t; | |
| }; | |
| const parse = (s: string): Term => { | |
| // Simplified parser for demonstration | |
| // Returns a dummy term if parsing fails | |
| return { tag: 'Abs', body: (v: any) => v }; | |
| }; | |
| const main = () => { | |
| // Church numeral 2: \f. \x. f (f x) | |
| const two = { | |
| tag: 'Abs', | |
| body: (f: any) => { | |
| return { | |
| tag: 'Abs', | |
| body: (x: any) => { | |
| return { | |
| tag: 'App', | |
| left: f, | |
| right: { | |
| tag: 'App', | |
| left: f, | |
| right: x | |
| } | |
| } | |
| } | |
| }; | |
| } | |
| }; | |
| // 2^2: applying 2 to 2 | |
| const term = { tag: 'App', left: two, right: two }; | |
| const result = eval(term); | |
| // To show the result, we apply it to a function and a base value | |
| // Let's use \s. \z. s z and \z. z to get a Church numeral, then convert to number. | |
| // Or simpler: apply to \x. x+1 and 0. | |
| const succ = { | |
| tag: 'Abs', | |
| body: (n: any) => ({ tag: 'Var', isVal: true, val: n + 1 }) | |
| }; | |
| const zero = 0; | |
| // This is a hack to show the number. | |
| // We'll just print the structure of the result for now. | |
| console.log(wnf(term)); | |
| }; | |
| main(); | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment