# Introduction

Plutus is a strictly typed pure functional programming language used for defining smart contracts in Cardano. The syntax is fairly Haskell-like, but unlike Haskell, the language is eagerly evaluated.

## Declaring Data Types

In Plutus, to define a data type, we give the name of the type, then any type parameters, together with a list of constructor alternatives — like in Haskell. Each constructor alternative has the types of its arguments.

So, for instance, the type of Peano numerals would be defined as

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

whereas binary trees would be defined as

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

The type constructor `Tree`

takes one parameter, `a`

. It’s inhabited by values
constructed by two constructors, `Leaf`

, which has no arguments, and `Branch`

,
which has three arguments, a left subtree of type `Tree a`

, a value of type
`a`

, and a right subtree of type `Tree a`

.

We can inspect data using the `case`

construct, like so:

```
case t of {
Leaf -> ... ;
Branch l x r -> ...
}
```

## Declaring Values

To declare a new value (whether it’s a function or not), we give its type, and
then specify its value. For instance, to define addition for natural numbers,
we can give a recursive definition using `case`

:

```
add : Nat -> Nat -> Nat {
add = \m n ->
case m of {
Zero -> n ;
Suc m' -> Suc (add m' n)
}
}
```

We can also use pattern matching equations in the same way as in Haskell, which makes the definition of functions like this much more elegant:

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

## Smart Contract Computations

Plutus has one important type built into the language specific for smart
contract computations: the type constructor `Comp`

, which takes one type
parameter. The simplest way to make values is with the two computation
constructors `success`

, which takes a value `M`

with type `A`

(for any choice
of `A`

) and produces a computation of type `Comp A`

which represents a
successful smart contract computation that returns `M`

. You can also build a
value of type `Comp A`

with just `failure`

, which represents a failed
computation.

It’s also possible to chain smart contract computations together using `do`

notation. Given a term `M`

of the type `Comp A`

, and a term `N`

of type
`Comp B`

with a free variable `x`

of type `A`

, we can form `do { x <- M ; N }`

which runs the computation `M`

, binds its returned value to `x`

, then runs the
computation `N`

. If the term `M`

computes to `failure`

, then the failure is
propagated by the `do`

construct and the whole thing computes to `failure`

.

This is most useful for building validator scripts for smart contracts. The
standard way of doing this is by asking for a redeemer program of type `Comp A`

and a validator program of type `A -> Comp B`

, which then are composed to form
`do { x <- redeemer ; validator x }`

. The `redeemer`

program is run, returning
whatever data `validator`

needs, and then that data is given to `redeemer`

that is run.

## More Detailed Overview

The other files in this directory provide a more detailed overview of the grammar, types, and programs of Plutus, including the built-in types and functionality, and should be read before diving into writing programs. There’s also a demo file, showing the implementation of a number of common functions, to give a good sense of the use of the language.