Types

This document contains a reference for the types in the Plutus language. It uses some informal type theory, which hopefully is understandable to everyone reading this document.

Plutus comes with a handful of built-in types (ints, floats, bytestrings), and a single built-in type operator (functions). Other types are defined by the authors of programs. We’ll discuss each of these in turn.

Ints, Floats, and Byte Strings

Int, Float, and ByteString are primitive types, with constructor forms given by various constants specified by the following grammar.

<int> ::= "-"? <digit>+
<float> ::= "-"? <digit>+ <fractExponent>
<digit> = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
<fractExponent> ::= <fraction> <exponent>? | <exponent>
<fraction> ::= "." <digit>+
<exponent> ::= ("e" | "E") ("-" | "+") <digit>+

<bytestring> ::= "#" <byte>*
<byte> ::= <nybble> <nybble>
<nybble> ::= <digit>
           | "a" | "b" | "c" | "d" | "e" | "f"
           | "A" | "B" | "C" | "D" | "E" | "F"

There are no true eliminator forms for these types, but there are a number of built-in operations which can be applied to these types. We write the signatures of built-ins as follows: f : (A,B) ⇀ C indicates that built-in name f can be applied to an A and a B to produce a C. The built-ins for these primitive types are as follows, with implementations in terms of Haskell functions:

addInt : (Int,Int) ⇀ Int
  implemented as `(+) :: Int -> Int -> Int`

subtractInt : (Int,Int) ⇀ Int
  implemented as `(-) :: Int -> Int -> Int`

multiplyInt : (Int,Int) ⇀ Int
  implemented as `(*) :: Int -> Int -> Int`

divideInt : (Int,Int) ⇀ Int
  implemented as `div :: Int -> Int -> Int`

remainderInt : (Int,Int) ⇀ Int
  implemented as `(%) :: Int -> Int -> Int`

lessThanInt : (Int,Int) ⇀ Bool
  implemented as `(<) :: Int -> Int -> Bool`

equalsInt : (Int,Int) ⇀ Bool
  implemented as `(==) :: Int -> Int -> Bool`

intToFloat : (Int) ⇀ Float
  implemented as `fromInteger . toInteger :: Int -> Float`

intToByteString : (Int) ⇀ ByteString
  implemented as `encode :: Int -> ByteString`

addFloat : (Float,Float) ⇀ Float
  implemented as `(+) :: Float -> Float -> Float`

subtractFloat : (Float,Float) ⇀ Float
  implemented as `(-) :: Float -> Float -> Float`

multiplyFloat : (Float,Float) ⇀ Float
  implemented as `(*) :: Float -> Float -> Float`

divideFloat : (Float,Float) ⇀ Float
  implemented as `(/) :: Float -> Float -> Float`

lessThanFloat : (Float,Float) ⇀ Bool
  implemented as `(<) :: Float -> Float -> Bool`

equalsFloat : (Float,Float) ⇀ Bool
  implemented as `(==) :: Float -> Float -> Bool`

ceiling : (Float) ⇀ Float
  implemented as `ceiling:: Float -> Float`

floor : (Float) ⇀ Float
  implemented as `floor :: Float -> Float`

round : (Float) ⇀ Float
  implemented as `round :: Float -> Float`

concatenate : (ByteString,ByteString) ⇀ ByteString
  implemented via `concat :: [ByteString] -> ByteString`

drop : (Int,ByteString) ⇀ ByteString
  implemented via `drop :: Integer -> ByteString -> ByteString`

take : (Int,ByteString) ⇀ ByteString
  implemented via `take :: Integer -> ByteString -> ByteString`

sha2_256 : (ByteString) ⇀ ByteString
  implemented via `hash : [Char8] -> Digest SHA256`

sha3_256 : (ByteString) ⇀ ByteString
  implemented via `hash : [Char8] -> Digest SHA3_256`

equalsByteString : (ByteString,ByteString) ⇀ Bool
  implemented as `(==) :: ByteString -> ByteString -> Bool`

The use of these built-in functions is by prefixing the name with ! and fully applying them to arguments. E.g., adding 2 and 3 would be !addInt 2 3.

Function Types

Given any A and B types, there is a function type A -> B. To get a term of this type, we can use the lambda introduction form as follows: if M has type B and has a free variable x that has type A, then \x -> M has type A -> B. We can use a term with a function type as follows: if M has type A -> B and N has type A, then M N has type B. The computation for functions is standard beta reduction: (\x -> M) N reduces to [N/x]M, i.e. to M with N substituted for x. Computation in Plutus is performed eagerly, so N is evaluated before substitution is performed.

User Declared Types

When a user declares a new data type, for example

data Foo a = { Bar | Baz a }

this defines a new type constructor, in this case Foo, which has the following inference rule associated with it: given any type A, Foo A is also a type.

It also comes with inference rules for the constructors, as follows: Bar has type Foo A, for any choice of A; and if M has type A, then Baz M has type Foo A.

The eliminator form for user declared types is the case construct, which is used for all such types. Case analysis is the same as in Haskell, for example, we could write

case foo of { Bar -> 0 | Baz x -> x }

to analyze an element of type Foo Int, computing an Int. There is a minor difference from Haskell, however: we can analyze multiple terms at the same time, by separating them (and their corresponding patterns) with |:

case foo0 | foo1 of { Bar | Bar -> 0 ; Baz x | Baz y -> !addInt x y }

Case analysis is not required to be total, that is to say, there may be missing patterns. Any failed match causes the entire program to fail to run, and will cause a transaction to be considered invalid.

Int, Float, and ByteString literals can be patterns as well; for example, we can define the factorial function using case in this way:

facInt : Int -> Int {
  facInt n = case n of {
    0 -> 1 ;
    _ -> !multiplyInt n (!subtractInt n 1)
  }
}