NLinker

Church numbers with TypeScript

Oct 24th, 2018
190
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. interface Nat {
  2.     name: 'zero' | 'succ';
  3.     pred: Nat;
  4. }
  5.  
  6. class Zero implements Nat {
  7.     name: 'zero';
  8.     pred: Zero;
  9.     constructor() { this.pred = this; }
  10. }
  11.  
  12. class Succ<T extends Nat> implements Nat {
  13.     name: 'succ';
  14.     pred: T;
  15.     constructor(pred: T) { this.pred = pred; }
  16. }
  17.  
  18. class Plus<A extends Nat, B extends Nat> {
  19.     zero: {
  20.         zero: B;
  21.         succ: B;
  22.     };
  23.     succ: {
  24.         zero: A;
  25.         succ: Succ<Plus<A['pred'], B>[A['pred']['name']][B['name']]>;
  26.     };
  27. }
  28.  
  29. type One = Succ<Zero>;
  30. type Two = Succ<One>;
  31.  
  32. type Sum = Plus<One, Two>[One['name']][Two['name']];
Add Comment
Please, Sign In to add comment