# 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? Commented Jan 28, 2021 at 6:08
• @Kaddath That depends entirely on the language. Commented Jan 28, 2021 at 8:54
• Also, what determines whether the numbers are represented in Peano arithmetic? I flagged the question as "needs more clarity". Commented Jan 28, 2021 at 9:11
• @xigoi You can convert to numbers and do arithmetic and convert back to Peano, as long as it happens at compile time. Nothing wrong with that.
– user
Commented Jan 28, 2021 at 12:36
• @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
Commented Jan 28, 2021 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
Commented Jan 28, 2021 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
Commented Jan 28, 2021 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
Commented Jan 29, 2021 at 18:07
• 320 bytes Commented Feb 1, 2021 at 9:32
• The last one also works in Objective-C. Commented Aug 28, 2021 at 15:39

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


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


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

impl<B> Add<B>for Z{type R=B;}

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.