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 provide 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.