Type Arithmetics: Computation based on the theory of types

TL;DR

This paper introduces a type system capable of expressing arbitrary arithmetic computations, including negative numbers, with arithmetic operations implemented as type reduction rules, enabling compile-time computation and error detection.

Contribution

It presents a novel type system that encodes Peano arithmetic with negative numbers, allowing arithmetic operations to be performed at compile time through type reduction.

Findings

Arithmetic operations are expressed as type reduction rules.

Division by zero is detected as a compile-time type error.

The system supports negative numbers in arithmetic computations.

Abstract

The present paper shows meta-programming turn programming, which is rich enough to express arbitrary arithmetic computations. We demonstrate a type system that implements Peano arithmetics, slightly generalized to negative numbers. Certain types in this system denote numerals. Arithmetic operations on such types-numerals - addition, subtraction, and even division - are expressed as type reduction rules executed by a compiler. A remarkable trait is that division by zero becomes a type error - and reported as such by a compiler.