# Peano arithmetic at compile time

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

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

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


• This seems like a kind of non-observable requirement. What prevents us from converting the numbers to a regular representation, doing the arithmetic and converting back? – xigoi Jan 28 at 6:08
• @xigoi I feel there is some validity in your comment, but wouldn't converting to regular numbers and doing the arithmetic happen in run time instead of compile time? – Kaddath Jan 28 at 8:32
• @Kaddath That depends entirely on the language. – xigoi Jan 28 at 8:54
• Also, what determines whether the numbers are represented in Peano arithmetic? I flagged the question as "needs more clarity". – xigoi Jan 28 at 9:11
• @user202729 It isn't, but as xigoi pointed out, the question was unclear the way it was, so I had to edit it. I'm not sure what you mean about the C++ one, though. Do you that it could be interpreted as a Peano number somehow? – user Jan 28 at 17:24

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

• I've restricted the output to look like a Peano number now, but this answer is good since it was posted before I edited the question. – user Jan 28 at 13:41

# 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

• I've restricted the output to look like a Peano number now, but this answer is good since it was posted before I edited the question. – user Jan 28 at 13:41
• I don't know how your second version works exactly, but it should be fine as long as input and output look like Peano numbers and aren't normal ints. Although if you make that your main answer, please don't delete the first one, it's interesting. – user Jan 29 at 18:07
• 320 bytes – ceilingcat Feb 1 at 9:32

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

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

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>;}


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