Rules

Input/Output

The input and output formats do not have to be the same, but they should be one of these:

• A type constructor of kind * -> * to represent S and a type of kind * to represent Z, e.g. S<S<Z>> to represent 2 in Java or int[][] (int for 0, [] for S).
• A string with a Z at the middle and 0 or more S(s and )s around it, e.g. "S(S(Z))" to represent 2.
• Any other format resembling Peano numbers, where there is a value representing zero at the bottom, and another wrapper that can contain other values.

Rules

S(S(S(Z))) + Z = S(S(S(Z)))                 | 3 + 0 = 3
S(S(Z)) + S(S(S(Z))) = S(S(S(S(S(Z)))))     | 2 + 3 = 5
S(S(S(Z))) - S(S(S(Z))) = Z                 | 3 - 3 = 0
S(S(Z)) * S(S(S(Z))) = S(S(S(S(S(S(Z))))))  | 2 * 3 = 6
S(S(S(S(Z)))) * S(S(Z)) = S(S(Z))           | 4 / 2 = 2
Z / S(S(Z)) = Z                             | 0 / 2 = 0

• Type-Level Programming in Scala (a bunch of articles, including ones about Peano arithmetic) (for Scala)
• Multiplication at compile time (for Scala)
• Peano arithmetic in C++ type system

S(S(S(Z))) + Z = S(S(S(Z)))                 | 3 + 0 = 3
S(S(Z)) + S(S(S(Z))) = S(S(S(S(S(Z)))))     | 2 + 3 = 5
S(S(S(Z))) - S(S(S(Z))) = Z                 | 3 - 3 = 0
S(S(Z)) * S(S(S(Z))) = S(S(S(S(S(S(Z))))))  | 2 * 3 = 6
S(S(S(S(Z)))) / S(S(Z)) = S(S(Z))           | 4 / 2 = 2
Z / S(S(Z)) = Z                             | 0 / 2 = 0

• Type-Level Programming in Scala (a bunch of articles, including ones about Peano arithmetic) (for Scala)
• Multiplication at compile time (for Scala)
• Peano arithmetic in C++ type system (for C++)
• Type arithmetic (for Haskell)

Peano numbers represent nonnegative integers as zero or successors of other Peano numbers. For example, 1 would be represented as Succ Zero and 3 would be Succ Succ Succ Zero.

Peano numbers represent nonnegative integers as zero or successors of other Peano numbers. For example, 1 would be represented as Succ(Zero) and 3 would be Succ(Succ(Succ(Zero))).

Test cases

S is used for successors and Z is used for zero.

S(S(S(Z))) + Z = S(S(S(Z)))                 | 3 + 0 = 3
S(S(Z)) + S(S(S(Z))) = S(S(S(S(S(Z)))))     | 2 + 3 = 5
S(S(S(Z))) - S(S(S(Z))) = Z                 | 3 - 3 = 0
S(S(Z)) * S(S(S(Z))) = S(S(S(S(S(S(Z))))))  | 2 * 3 = 6
S(S(S(S(Z)))) * S(S(Z)) = S(S(Z))           | 4 / 2 = 2
Z / S(S(Z)) = Z                             | 0 / 2 = 0