Type Arithmetics: Computation based on the theory of types
计算与语言
2007-05-23 v1
摘要
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.
引用
@article{arxiv.cs/0104010,
title = {Type Arithmetics: Computation based on the theory of types},
author = {Oleg Kiselyov},
journal= {arXiv preprint arXiv:cs/0104010},
year = {2007}
}
备注
1 HTML page, 1 C++ source code file