Understanding Recursive Algebraic Types in Functional Programming

Question

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

Translate Succ with 1 +. Every natural number is 1 + (1 + ( ... (1 + 0) ... )) for a suitable number of operations. — Daniel Fischer
– Daniel Fischer, Commented Mar 31, 2012 at 13:21

ehird · Accepted Answer · 2012-03-31 13:34:26Z

13

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.

edited Mar 31, 2012 at 13:34

answered Mar 31, 2012 at 13:21

ehird

40.9k3 gold badges185 silver badges184 bronze badges

Sign up to request clarification or add additional context in comments.

3 Comments

user1058210 Over a year ago

Thanks for such a clear answer ehird! So is the Succ constructor an inbuilt function representing n+1? I was confused because I thought it was just declaring another possible value in the normal fashion. If we have a number n, why do we want to represent the value n+1 i.e. the next value in the natural number sequence? Aren't we just concerned with how we can express the value n? Thanks for the pattern matching bit at the end - it was very useful!

ehird Over a year ago

No, it's not built-in; you could rename it to Fnarf and it'd be exactly the same. The idea is that we define this type, and assign each value of it a meaning as a natural number: we represent the data with the type. Succ n represents n + 1 because n already has to be represented by another Nat. If you have Zero (0), and you want 1, you have to use Succ Zero, to represent 0 + 1 = 1. If you have Succ Zero (1), and you want 2, you have to use Succ (Succ Zero), to represent 1 + 1 = 2... and so on.

sepp2k Over a year ago

@user1058210 No, Succ is not built-in. It's just the name you gave to the constructor. You need a way to get from n to n+1, so you can represent any number. If the definition was just data Nat = Zero, you could only represent zero. Of course you could extend that to more numbers like data Nat = Zero | One | Two, but that approach only gives you a finite number of numbers. Using Succ you can just apply Succ to Zero n times to represent the number n.

Collectives™ on Stack Overflow

Understanding Recursive Algebraic Types in Functional Programming

1 Answer 1

3 Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

3 Comments

Your Answer

Sign up or log in

Post as a guest

Related