# 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 a 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)
}
}
```