# Data type¶

The protocol standardises basic types and general algebraic data types. All messages sent and received within and between nodes and all parts of state must have an associated data type. Data types used by the protocol itself are fixed a priori (by this specification). Implementation languges will typically represent these types as native types in their typesystem, such that the implementation language can provide typechecking. Data types used by applications are chosen by application authors, serialised, and passed around at runtime in order to handle data appropriately.

## Types¶

### Basic types¶

A *basic type* is defined as either:

- a finite set type, of order \(n\)
- a natural number type (arbitrary-size)
- a function type from one data type to another data type

```
type BasicType :=
| FinSetT Nat
| NatT
| FunctionT DataType DataType
```

Note

This set of basic types is minimal, designed only to distinguish between fixed-size values, variable-size values, and functions. Other semantic information (e.g. whether a finite set value is intended to represent a ring or a finite field) will be tracked at a separate layer.

### Data types¶

A *data type* is defined as either:

- a basic type
- a product of other data types
- a coproduct of other data types

Note

Here `[]`

is used as shorthand notation for an ordered list of at least one element.

Note

Here `[]`

is used as shorthand notation for an ordered list of at least one element.

```
type DataType :=
| BasicT BasicType
| ProductT [DataType]
| CoproductT [DataType]
```

## Values¶

### Basic values¶

A *basic value* is defined as either:

- a natural number value \(n\)
- a function value (represented with a particular virtual machine, identified by a natural number)

```
type BasicValue :=
| NatV Nat
| FunctionV Nat Bytestring
```

### Data values¶

A *data value* is defined as either:

- a basic value
- a tuple of other data values (inhabitant of a product type)
- a option with an index and a data value (inhabitant of a coproduct type)

```
type DataValue :=
| BasicV BasicValue
| TupleV [DataValue]
| OptionV Nat DataValue
```

## Typechecking¶

The typechecking relation

```
typecheck : DataValue -> DataType -> Boolean
```

can be implemented in the obvious manner. Typechecking functions would require typechecking support from particular virtual machines, which isnâ€™t covered for now, but could be added in the future in a straightforward way.