How to define a function that takes natural numbers of a data type and return their sum?

Question

I am still learning how value constructors work. I read a lot about data types and their value constructors. The problem is that I never saw them in practice. For example

data Nat = Zero | Succ Nat

Now if we want to define a functions that takes two inputs of Nat and returns the product, how would we do that? We have to convert them to Haskell Integrals if we want to use the operator *. And if we want to implement a mult function that takes two Nat's which should multiply them without converting them to Haskel Integrals, how would that look like?

I really don't get data types|value constructors yet. Can anyone illustrate how to correctly use such value constructors from the data Nat example above?

Answer 1

You can implement mult :: Nat -> Nat -> Nat without converting the arguments to Integer first. What is multiplication? It's repeated addition, which you can define recursively:

n * 0 == 0
n * m == n + n * (m - 1)

Recall that m - 1 is the value of the Nat wrapped by Succ; if m == Succ k, then k represents m - 1. With that in mind, you should be able to see how to define mult, assuming you have a definition of add :: Nat -> Nat -> Nat available.

mult :: Nat -> Nat -> Nat
mult n Zero = ...
mult n (Succ m) = ...

add :: Nat -> Nat -> Nat can be defined similarly, using a definition based on repeated incrementing.

-- n + 0 = n
-- n + m = (n + 1) + (m - 1)
def add :: Nat -> Nat -> Nat
add n Zero = ...
add n (Succ m) = ...

Answer 2

You can pattern match on these. For example, we can decrement the number (or return Zero in case it was already Zero) with:

dec :: Nat -> Nat
dec Zero = Zero
dec (Succ n) = n

Here the patterns are thus Zero, which matches the Zero value, and Succ n, which will thus unify n with the value wrapped in the Succ data constructor.

If you want to sum up two Nats, you thus define a function add :: Nat -> Nat -> Nat. You first might want to try all possible cases for the data constructors of the two values, and perhaps later look to improve your code by generalizing the clauses.