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) = ...