Hey I'm having some trouble understanding how Recursive Algebraic Types work and how to use them exactly. For example, take the below RAT definition for the natural numbers:
data Nat = Zero | Succ Nat
We're using a RAT here because the set of values needs to be infinite and I know the principle is to express each new value in terms of a previous one, but I don't understand how this forms the natural numbers. Would someone mind clearing this up? Thanks
This states that:
Nat
is a type.
Zero
has type Nat
. This represents the natural number 0.
If n
has type Nat
, then Succ n
has type Nat
. This represents the natural number n+1.
So, for example, Succ (Succ Zero)
represents 2, Succ (Succ (Succ Zero))
represents 3, Succ (Succ (Succ (Succ Zero)))
represents 4, and so on. (This system of defining the natural numbers from 0 and successors is called the Peano axioms.)
In fact, Zero
and Succ
are just special kinds of functions (constructors) that are declared to create Nat
values:
Zero :: Nat
Succ :: Nat -> Nat
The difference from regular functions is that you can take them apart with pattern-matching:
predecessor :: Nat -> Nat
predecessor Zero = Zero
predecessor (Succ n) = n
Nothing about this is special to recursive algebraic data types, of course, just algebraic data types; but the simple fact that an algebraic data type can have a value of the same type as one of its fields is what creates the recursion here.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With