Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 1 / a / Solution

The two constructors encode a natural number by its number of successors. Structural recursion replaces the zero constructor by zero and every successor by one addition:

convert :: Natural -> Integer
convert Zero     = 0
convert (Succ n) = 1 + convert n

Structural induction gives $\boxed{\mathrm{convert}({\mathrm{Succ}}^n\mathrm{Zero})=n}$. The output uses unbounded integers, so there is no machine-word overflow.