add_example.hvm

// Scott Bins
(O x) = λo λi λe (o x) // bit 0
(I x) = λo λi λe (i x) // bit 1
E     = λo λi λe e // bitstring end

// Repeated application of a function and its inverse.
// Rep : Bin -> (f: a -> a) -> a -> a
(Rep a f x) = (a
  λa_pred λf λx (Rep a_pred λx(f (f x)) x)
  λa_pred λf λx (Rep a_pred λx(f (f x)) (f x))
  λf λx x
  f x)

// Increments a Bin.
// Inc : Bin -> Bin
(Inc x) = λo λi λe
  let case_o = i 
  let case_i = λx (o (Inc x))
  let case_e = e
  (x case_o case_i case_e)

// Addition
(Add a b) = (Rep a λx(Inc x) b)

// Better visualization
(Show x) = (x
  λp (List.cons 0 (Show p))
  λp (List.cons 1 (Show p))
  List.nil)

Main = 
  let a = (I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I E))))))))))))))))))))))))))))))))
  let b = (O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O E))))))))))))))))))))))))))))))))
  (Show (Add a b))

Example that does NOT fuse:

// Scott Bins
(O x) = λo λi λe (o x) // bit 0
(I x) = λo λi λe (i x) // bit 1
E     = λo λi λe e // bitstring end

// Repeated application of a function and its inverse.
// Rep : Bin -> (f: a -> a) -> a -> a
(Rep a f x) = (a
  λa_pred λf λx (Rep a_pred λx(f (f x)) x)
  λa_pred λf λx (Rep a_pred λx(f (f x)) (f x))
  λf λx x
  f x)

// Increments a Bin.
// Inc : Bin -> Bin
(Inc x) = λo λi λe
  let case_o = i
  let case_i = λx (o (Inc x))
  let case_e = (i e)
  (x case_o case_i case_e)

// Addition
(Add a b) = (Rep a λx(Inc x) b)

// Better visualization
(Show x) = (x
  λp (List.cons 0 (Show p))
  λp (List.cons 1 (Show p))
  List.nil)

Main = 
  let a = (I(I(I(I(I(I(I(I(I(I(I(I(I(I(I(I E))))))))))))))))
  let b = (O(O(O(O(O(O(O(O(O(O(O(O(O(O(O(O E))))))))))))))))
  (Show (Add a b))