Peano arithmetic at compile time

Question

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))).

Task

Implement the following operations on Peano numbers, at compile time:

• Addition
• Subtraction - You will never be required to subtract a greater number from a smaller one.
• Multiplication
• Division - You will never be required to divide two numbers if the result will not be an integer.

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

• You may use type members, implicits, type constructors, whatever you want, as long as a result can be obtained at compile time.
• For the purposes of this challenge, any execution phase before runtime counts as compile time.
• Since answers must work at compile-time, answers must be in compiled languages. This includes languages like Python, provided you can show that the bytecode contains the result of your computation before you even run the code.
• This is code-golf, so shortest code in bytes wins!

Example for just addition in Scala

sealed trait Num {
  //This is like having a method `abstract Num plus(Num n);`
  type Plus[N <: Num] <: Num
}
object Zero extends Num {
  //When we add any n to zero, it's just that n again
  type Plus[N <: Num] = N
}
final class Succ[N <: Num](n: N) extends Num {
  //In Java: `Num plus(Num x) { return new Succ(n.plus(x)) }
  type Plus[X <: Num] = Succ[N#Plus[X]]
}

Usage (Scastie):

//This is just for sugar
type +[A <: Num, B <: Num] = A#Plus[B]

type Zero = Zero.type
type Two = Succ[Succ[Zero]]
type Three = Succ[Two]
type Five = Succ[Succ[Three]]
val five: Five = null
val threePlusTwo: Three + Two = five
val notFivePlusTwo: Five + Two = five //should fail
val zeroPlusFive: Zero + Five = five

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

Some links to help you get started

• 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)

Answer 1

CP-1610 assembly, 37 bytes

This is simply using macro expansion.

Z EQU 0
MACRO S(n)
(%n%+1)
ENDM
 DCW [expression]

Example

With the expression S(S(Z)) * S(S(S(Z))), this gets compiled as:

00000000 Z                          
0x0                             Z EQU 0
                                MACRO S(n)
                                (%n%+1)
                                ENDM
                                ;DCW S(S(Z)) * S(S(S(Z)))
                                ;DCW (S(Z)+1) * S(S(S(Z)))
                                ;DCW ((Z+1)+1) * S(S(S(Z)))
                                ;DCW ((Z+1)+1) * (S(S(Z))+1)
                                ;DCW ((Z+1)+1) * ((S(Z)+1)+1)
0000   0006                      DCW ((Z+1)+1) * (((Z+1)+1)+1)
 ERROR SUMMARY - ERRORS DETECTED 0
               -  WARNINGS       0

(compiled with as1600 from the SDK included with jzIntv)

Answer 2

C++, 328 bytes

#define T template<class
#define O T N>struct
#define W T A,class B>struct
#define U using t=
U int;O S;W a;W a<S<A>,B>:a<A,S<B>>{};O a<t,N>{U N;};W s{U A;};W s<S<A>,S<B>>:s<A,B>{};W m{U int;};O m<N,S<t>>{U N;};W m<A,S<B>>:a<typename m<A,B>::t,A>{};T A,class B,class V=t>struct d:d<typename s<A,B>::t,B,S<V>>{};W d<t,A,B>{U B;};

Try it online!

0 (Z) is represented by the type int. Succ(N) is represented by the type S<N>.

A+B is a<A, B>::t, A-B is s<A, B>::t, A*B is m<A, B>::t and A/B is d<A, B>::t.

---

C++, 285 bytes

#define U template<
#define Q U class N>struct
#define X(n,o)U class A,class B>struct n:T<i<A>::v o i<B>::v>{};
Q S;Q i{static const int v=0;};Q i<S<N>>{static const int v=1+i<N>::v;};U int i>struct T{using t=S<typename T<i-1>::t>;};U>struct T<0>{using t=int;};X(a,+)X(s,-)X(m,*)X(d,/)

This "cheatier" version (if this is allowed) is shorter. It simply converts type to int -> do operation -> convert back to type.

Try it online!

---

C++ or C, 29 bytes

#define Z 0
#define S(N)(N+1)

Try it online!

This is even more cheaty, and relies on C having integer constant expressions and C++ having constant evaluation that can be run at compile time

Answer 3

TypeScript, 618 585 bytes

type R<T,U,V>=T extends U?V:T
type I<T>=R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<T,20,21>,19,20>,18,19>,17,18>,16,17>,15,16>,14,15>,13,14>,12,13>,11,12>,10,11>,9,10>,8,9>,7,8>,6,7>,5,6>,4,5>,3,4>,2,3>,1,2>,0,1>
type D<T>=R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<R<T,0,[]>,1,0>,2,1>,3,2>,4,3>,5,4>,6,5>,7,6>,8,7>,9,8>,10,9>,11,10>,12,11>,13,12>,14,13>,15,14>,16,15>,17,16>,18,17>,19,18>,20,19>,21,20>
type A<T,U>=T extends 0?U:A<D<T>,I<U>>
type S<T,U>=U extends 0?T:S<D<T>,D<U>>
type F<T,U,V=0>=S<T,U>extends[]?V:F<S<T,U>,U,I<V>>
type B<T,U>=U extends 0?0:U extends 1?T:A<B<T,D<U>>,T>

Playground link

Key

Value	Syntax
Zero	0
Successor of n	I<n>
n + m	A<n, m>
n - m	S<n, m>
n * m	B<n, m>
floor(n / m)	F<n, m>

Test Cases

type Zero = 0
type Two = I<I<Zero>>
type Three = I<Two>
type Four = I<Three>
type Five = I<Four>
declare const zero: Zero;
declare const two: Two;
declare const three: Three;
declare const five: Five;
declare const six: I<Five>;

let threePlusTwo: A<Three, Two> = five;
let fivePlusTwo: A<Five, Two> = five; // error: '5' is not '7'
let zeroPlusFive: A<Zero, Five> = five;

let threePlusZero: A<Zero, Three> = three;
let twoPlusThree: A<Two, Three> = five;
let threeMinusThree: S<Three, Three> = zero;
let twoTimesThree: B<Two, Three> = six;
let fourOverTwo: F<Four, Two> = two;
let zeroOverTwo: F<Zero, Two> = zero;

Explanation

• R<T, U, V> is a replacement function: It takes T as its main input and replaces U with V.
• I<T> and D<T> are used to change numbers by 1. I know that I hardcoded it to stop at 21, but unfortunately I can't go further due to TypeScript's recursion limit. I originally tried a different method that was easier to understand and to extend, but it hit the recursion limit even faster. Underflow is represented with [] (empty tuple).
• A<T, U> returns U when T = 0, and A<T - 1, U + 1> otherwise.
• S<T, U> returns T when U = 0, and S<T - 1, U - 1> otherwise.
• F<T, U, V> technically returns floor(T / U) + V, but V defaults to 0. It uses V to keep track of the answer.
• B<T, U> returns immediately when U is 0 or 1, and otherwise returns B<T, U - 1> + T.

TL;DR: A lot of recursion.

Dividing by zero gives an error (TS2589), which I think is the correct behavior.

Bonus

Modulo and primality test:

type M<T,U>=S<T,U>extends[]?T:M<S<T,U>,U>
type H<T,U>=U extends 1?1:M<T,U>extends 0?0:H<T,D<U>>
type P<T>=T extends 1?0:H<T,D<T>>

M<T, U> returns T mod U. P<T> returns 1 when T is prime and 0 otherwise.
Like with division, these both give an error when attempting to use 0 where it doesn't make sense.

---

Original

The original answer was very similar, but with a small difference in how F was defined:

type G<T,U>=S<U,T>extends []?1:0
type F<T,U,V=0>=G<U,T>extends 1?V:F<S<T,U>,U,I<V>>

Answer 4

Rust, 547 bytes

struct Z;struct S<Z>(Vec<Z>);trait A<B>{type R;}impl<B>A<B>for Z{type R=B;}impl<B,N:A<B>>A<B>for S<N>{type R=S<<N as A<B>>::R>;}trait M<B>{type R;}impl<N>M<N>for Z{type R=Z;}impl<N>M<Z>for S<N>{type R=S<N>;}impl<P,N:M<P>>M<S<P>>for S<N>{type R=<N as M<P>>::R;}trait T<B>{type R;}impl<B>T<B>for Z{type R=Z;}impl<B,N:T<B>>T<B>for S<N>where<N as T<B>>::R:A<B>{type R=<<N as T<B>>::R as A<B>>::R;}trait D<B>{type R;}impl<P>D<S<P>>for Z{type R=Z;}impl<P,N:M<P>>D<S<P>>for S<N>where<N as M<P>>::R:D<S<P>>{type R=S<<<S<N> as M<S<P>>>::R as D<S<P>>>::R>;}

Try it online

This is basically equivalent to the Scala version. It defines two structs, Z and S<Z>, and four traits that implement the operations (called A, M, T and D in the golfed code).

Readable version:

struct Z;
struct S<Z>(Vec<Z>);

trait Add<B>{type R;}
impl<B> Add<B>for Z{type R=B;}
impl<B,N: Add<B>> Add<B>for S<N>{type R=S<<N as Add<B>>::R>;}

trait Sub<B>{type R;}
impl<N>Sub<N>for Z{type R=Z;}
impl<N> Sub<Z>for S<N>{type R=S<N>;}
impl<P,N: Sub<P>> Sub<S<P>>for S<N>{type R=<N as Sub<P>>::R;}

trait Times<B>{type R;}
impl<B> Times<B>for Z{type R=Z;}
impl<B,N: Times<B>> Times<B>for S<N> where <N as Times<B>>::R: Add<B>{type R=<<N as Times<B>>::R as Add<B>>::R;}

trait Divide<B>{type R;}
impl<P>Divide<S<P>>for Z{type R=Z;}
impl<P,N:Sub<P>>Divide<S<P>>for S<N>where<N as Sub<P>>::R:Divide<S<P>>{type R=S<<<S<N> as Sub<S<P>>>::R as Divide<S<P>>>::R>;}

Answer 5

C++ (gcc), 307 bytes

#define _ struct
#define n typename
#define t template<n T
#define U{using X
_ Z;
t>_ S U=T;};

t,n B>_ s U=S<n s<n T::X,B>::X>;};
t>_ s<Z,T>U=T;};

t,n B>_ b U=n b<n T::X,n B::X>::X;};
t>_ b<T,Z>U=T;};

t,n B>_ m U=n s<T,n m<T,n B::X>::X>::X;};
t>_ m<T,Z>U=Z;};

t,n B>_ d U=S<n d<n b<T,B>::X,B>::X>;};
t>_ d<Z,T>U=Z;};

Try it online!

• There's already a good C++ answer but I was missing template meta programming.

• Left newlines on the code for some "readability" , already subtracted 14 bytes.

• Basically S (succ) stores it's template type which is then recursively inspected inside the various operations (s=sum,b=subtract,m=multiply,d=division) to dig the Peano structure.