# Examples

Here we’ll take a look at some of the common examples of programs to give you a better feel of how the Plutus language works. We’ll implement Peano numerals, cons lists, and binary trees, as well as some common functions relating them.

To start with, let’s define Peano numerals:

```
data Nat = { Zero | Suc Nat }
```

The naturals support a variety of functions, of course, such as addition, multiplication, factorial, and Fibonacci, which are typical examples of programs.

```
add : Nat -> Nat -> Nat {
add Zero n = n ;
add (Suc m) n = Suc (add m n)
}
mul : Nat -> Nat -> Nat {
mul Zero _ = Zero ;
mul (Suc m) n = add (mul m n) n
}
fac : Nat -> Nat {
fac Zero = Suc Zero ;
fac (Suc n) = mul (Suc n) (fac n)
}
fib : Nat -> Nat {
fib Zero = Suc Zero ;
fib (Suc Zero) = Suc Zero ;
fib (Suc (Suc n)) = add (fib n) (fib (Suc n))
}
```

Cons lists are also a familiar type:

```
data List a = { Nil | Cons a (List a) }
```

This demonstrates the use of parametric types, where `List a`

has a type
parameter `a`

for the type of elements. So, for example, `List Nat`

is the type
of lists of Peano numerals.

Lists support a variety of functions, such as `length`

, `append`

, and `map`

:

```
length : forall a. List a -> Nat {
length Nil = Zero ;
length (Cons _ xs) = Suc (length xs)
}
append : forall a. List a -> List a -> List a {
append Nil ys = ys ;
append (Cons x xs) ys = Cons x (append xs ys)
}
map : forall a b. (a -> b) -> List a -> List b {
map _ Nil = Nil ;
map f (Cons x xs) = Cons (f x) (map f xs)
}
```

Here we can see the use of polymorphism principle in Plutus. These functions work for any list, regardless of the element type, so we can abstract over the element type by using `forall`

. For instance, the type of `length`

says that for any choice of `a`

, we have a function of type `List a -> Nat`

.

It’s important to note that in Plutus, this polymorphism exists only for the
declaration of values. Any time you use a polymorphically declared value, the
choice of the type variable must be fixed at the use site. You can’t treat these
declarations as giving polymorphic values in general, as in System-F. Rather,
a polymorphic type in a declaration is an abbreviation for an infinite family of
identical definitions that differ only in the choice of that type variable. For
example, we could define multiple `length`

functions like so:

```
lengthNat : List Nat -> Nat {
lengthNat Nil = Zero ;
lengthNat (Cons _ xs) = Suc (lengthNat xs)
}
lengthBool : List Bool -> Nat {
lengtBool Nil = Zero ;
lengthBool (Cons _ xs) = Suc (lengthBool xs)
}
lengthListNat : List (List Nat) -> Nat {
lengthListNat Nil = Zero ;
lengthListNat (Cons _ xs) = Suc (lengthListNat xs)
}
```

And they’re all identical except the name and the choice for `a`

. This is of
course redundant, so we can use the polymorphic declaration given above. But
this declaration does not give us a value `length`

with the type
`forall a. List a -> Nat`

. Instead, it gives us that entire infinite family of
declarations, but with a convenient abbreviation syntax. This is why the use of
such polymorphic declarations requires the choice of the type variables to be
fixed at the use site.

Another common type is the type of binary trees with data in the branches:

```
data Tree a = { Leaf | Branch a (Tree a) (Tree a) }
```

Such trees support functions such as `count`

, `traversal`

, and `reverse`

:

```
count : forall a. Tree a -> Nat {
count Leaf = Zero ;
count (Branch _ l r) = Suc (add (count l) (count r))
}
traversal : forall a. Tree a -> List a {
traversal Leaf = Nil ;
traversal (Branch x l r) = Cons x (append (traversal l) (traversal r))
}
reverse : forall a. Tree a -> Tree a {
reverse Leaf = Leaf ;
reverse (Branch x l r) = Branch x (reverse r) (reverse l)
}
```