Nat and Int in raku

type-theory.raku

module Typ {
  our class Int {...}
  our class Nat {
    has Nat $.pred;
    method succ { (state %){self.WHICH} //= self.new: pred => self } 
  }
  multi sub infix:<==>(Nat $a, Nat $b) is export { $a === $b }
  constant zero  is export = Nat.new;
  constant one   is export = zero.succ;
  constant two   is export = one.succ;
  constant three is export = two.succ;

  class Int {
    has Nat ($.left, $.right);
    multi method new(Nat $n) { self.bless: left => $n, right => zero }
  }

  multi sub infix:<+>(Nat $a, zero --> Nat) is export { $a }
  multi sub infix:<+>(zero, Nat $a --> Nat) is export { $a }
  multi sub infix:<+>(Nat $a, Nat $b --> Nat) is export { samewith $a.pred, $b.succ }
  multi sub infix:<*>(Nat $ , zero --> Nat) is export { zero }
  multi sub infix:<*>(Nat $a, one  --> Nat) is export { $a }
  multi sub infix:<*>(Nat $a, Nat $b --> Nat) is export {
    $a + samewith $a, $b.pred
  }

  multi sub infix:<->(Int $a, Int $b) is export {
    Int.new: left => $a.left + $b.right, right => $a.right + $b.left;
  }

  multi sub infix:<==>(Int $a, Int $b) is export { 
    $a.left + $b.right == $a.right + $b.left
  }

}

import Typ;

say one.succ + zero == two;
say Typ::Int.new: one;

say (one ... three).map({"."}).join;