# Strict types

Portable & deterministic formalism for algebraic data types

*Strict types* is a formal semantic and notation system for encoding algebraic data types in a portable & deterministic way.

Why do we need another algebraic data types if we have one in Haskell, Idris etc? Well, we need it since existing systems focus on abstract goals and are quite far from the real existing computing platforms. **Strict types**, on the other hand, **apply algebraic data types to the existing computing platforms, networking and programming languages, without sacrificing formal analytical properties**. For instance, in strict types any collection must have a defined bounds for the minimum and maximum number of elements the collection may hold, which becomes a part of a type itself. This allows to precisely predict resource requirements at a compile time and avoid runtime exceptions, as well as apply formal analysis in a platform-specific manner.

Key features of strict types include:

* portability, or platform-independence: it can be used with different computing architectures, instruction set architectures and in networking systems without modification;
* determinism: any two strict encoded data which differ in their byte sequence will represent semantically-distinct information pieces;
* resource limits: any strict-encoded data can be accessed and computed on a limited-resource systems (embedded systems), since none of atomic encoding data pieces can exceed 64kb in size;
* formally verification: with algebraic data types and the strict encoding API it is possible to formally verify that the data serialization and deserialization is performed according to a schema, as well as prove statements about type semantic and memory layout equivalence and convertibility;
* extensibility: strict encoding typing may be extended with new types using provided notation system; this extensions include TLV-like extensions used for agile networking RPC contracts.

Strict types is a functional and close to the bare metal at the same time, which puts it into a segment of serialization languages which was not populated before: 

<figure><img src="/files/q7DNIe6xIlkQ5RDle2CG" alt=""><figcaption><p>Strict encoding on landscape of other languages and encoding notations</p></figcaption></figure>

Strict types were developed by Dr Maxim Orlovsky and is a part of a Swiss non-profit UBIDECO Institute (UBIDECO stands for "Ubiquitous Deterministic Computing"), launched by LNP/BP Standards Association, CypherNet DAO and Pandora Prime Inc at the end of 2022. Its roots go back to 2019 when client-side-validation paradigm was development by LNP/BP Standards Association, targeting distributed computing and originating from Peter Todd ideas about proofmarshal systems. Strict types development was supportedby iFinex Inc (Bitfinex, Tether), Fulgur Ventures, Pandora Prime Inc, DIBA Inc through of LNP/BP Association funding, as well as personal Dr Maxim Orlovsky funds.

Today, strict types are used in such systems as commit-verify cryptographic schemes, client-side-validation (including RGB protocol), distributed computing (including PRiSM computing), network encodings (especially in Internet2-related protocols), [AluVM](https://www.aluvm.org).

This document describes the main design goals behind strict types, its formal semantics and notation syntax, covers the main implementations on different platforms and languages, and targets technical people, engineers and "power users" interested in technology details.


# Data type algebra

## Fundamental types

Fundamental types are types built-in in strict encoding and not derived from any other types. These types include:

1. Unit type `()`
2. Byte type `Byte`
3. Integer numbers (signed `I_`, unsigned `U_` and natural `N_`)
4. Floating-point numbers `F_`
5. UTF-8 character `Utf8`

Byte type is introduced due to the fact that it semantically different from a 8-bit signed or unsigned integer: it does not contain information about sign and may not be representative with an integer at all.

While Unicode character type can be expressed expressed as a composite type, it will be very verbose expression (union with 256 variants), so for the practical purposes (to reduce the complexity of types which use Unicode strings) it was decided to built it in.

Strict encoding has reserved place for 55 more types, which may be introduced in a future to represent more floating-point integer encodings, Unicode variants etc. At the present moment use of that type identifiers would result in encoding/decoding failure.

### Integers

Integer types are named using a single upper case latter specifying set of integers used in type (`U` for unsigned, `I` for signed and `N` for natural non-zero integers) followed by a decimal number of bits in the type encoding (like `U8` or `I1024`).

Strict encoding covers integer types of different size in two ranges:

| Bit size    | Step                     |                    |
| ----------- | ------------------------ | ------------------ |
| 8 to 256    | 8 bits (i.e. 1 byte)     | from U8 up to U256 |
| 272 to 4352 | 128 bits (i.e. 16 bytes) | from U272 to U4352 |

In total, there are 64 different types for unsigned integers, 64 types for signed and 64 types for non-zero integers, giving 194 possible integer types in total. Not all of these types have a representation in all of the supported languages, so below we give a list of integer types which can be represented in Rust:

<table><thead><tr><th width="221">Sten type</th><th width="86">Bytes</th><th width="111">Encoding</th><th>Rust type</th></tr></thead><tbody><tr><td><code>U8</code> / <code>I8</code> / <code>N8</code></td><td>1</td><td>N/A</td><td><code>u8</code> / <code>i8</code> / <code>NonZeroU8</code></td></tr><tr><td><code>U16</code> / <code>I16</code> / <code>N16</code></td><td>2</td><td>LE</td><td><code>u16</code> / <code>i16</code> / <code>NonZeroU16</code></td></tr><tr><td><code>U24</code> / <code>I24</code> / <code>N24</code></td><td>3</td><td>LE</td><td><code>amplify_num::u24</code> / <code>i14</code> / <code>NonZeroU24</code></td></tr><tr><td><code>U32</code> / <code>I32</code> / <code>N32</code></td><td>4</td><td>LE</td><td><code>u32</code> / <code>i32</code> / <code>NonZeroU32</code></td></tr><tr><td><code>U48</code> / <code>I48</code> / <code>N48</code></td><td>6</td><td>LE</td><td><code>amplify_num::u48</code> / <code>i48</code> / <code>NonZeroI48</code></td></tr><tr><td><code>U64</code> / <code>I64</code> / <code>N64</code></td><td>8</td><td>LE</td><td><code>u64</code> / <code>i64</code> / <code>NonZeroU64</code></td></tr><tr><td><code>U128</code> / <code>I128</code> / <code>N128</code></td><td>16</td><td>LE</td><td><code>u128</code> / <code>i128</code> / <code>NonZeroU128</code></td></tr><tr><td><code>U256</code> / <code>I256</code> / <code>N256</code></td><td>32</td><td>LE</td><td><code>amplify_num::u256</code> / <code>i256</code> / <code>NonZero256</code></td></tr><tr><td><code>U512</code> / <code>I512</code> / <code>N512</code></td><td>64</td><td>LE</td><td><code>amplify_num::u512</code> / <code>i512</code> / <code>NonZero512</code></td></tr><tr><td><code>U1024</code> / <code>I1024</code> / <code>N1024</code></td><td>128</td><td>LE</td><td><code>amplify_num::u1024</code> / <code>i1024</code> / <code>NonZero1024</code></td></tr></tbody></table>

### Floating-point numbers

Strict encoding supports the following floating number encodings:

<table><thead><tr><th width="123">Sten type</th><th width="80">Bytes</th><th width="193">Encoding</th><th>Rust type</th></tr></thead><tbody><tr><td><code>R16B</code></td><td>2</td><td>bfloat16</td><td><code>bfloat::bf16</code></td></tr><tr><td><code>R16</code></td><td>2</td><td>IEEE Half</td><td><code>amplify_apfloat::ieee::Half</code></td></tr><tr><td><code>R32</code></td><td>4</td><td>IEEE Single</td><td><code>amplify_apfloat::ieee::Single</code></td></tr><tr><td><code>R64</code></td><td>8</td><td>IEEE Double</td><td><code>amplify_apfloat::ieee::Double</code></td></tr><tr><td><code>R80</code></td><td>10</td><td>IEEE X87 Extended</td><td><code>amplify_apfloat::ieee::X87DoubleExtended</code></td></tr><tr><td><code>R128</code></td><td>16</td><td>IEEE Quad</td><td><code>amplify_apfloat::ieee::Quad</code></td></tr><tr><td><code>R256</code></td><td>32</td><td>IEEE Oct</td><td><code>amplify_apfloat::ieee::Oct</code></td></tr></tbody></table>

Strict encoding has 54 more type identifiers reserved for possible use by future floating-point number encodings (like Tappered float etc); at the present moment use of that type identifiers would result in encoding/decoding failure.

## Type composition

Strict encoding uses generalized algebraic data types (GADT). This means that new types can be composed out of primitive types via following fundamental morphisms:

<table><thead><tr><th>Name</th><th width="214">Syntax form</th><th>Max no of elements / fields / variants</th></tr></thead><tbody><tr><td>Product types (structure, tuple)</td><td><code>• , •</code> <em>or</em> <code>(• , •)</code></td><td>255</td></tr><tr><td>Sum types <br>(union, enum)</td><td><code>• | •</code> <em>or</em> <code>(• | •)</code></td><td>255</td></tr><tr><td>Mapping (function)</td><td><code>• -> •</code> <em>or</em> <br><code>(•) ->^U..D (•)</code></td><td>From <code>U</code> to <code>D</code>, up to 2^64</td></tr><tr><td>Fixed array</td><td><code>[•^N]</code></td><td><code>N</code>, up to 2^16-1</td></tr><tr><td>Dynamic array</td><td><code>[•]</code> <em>or</em> <code>[• ^U..D]</code></td><td>From <code>U</code> to <code>D</code>, up to 2^64</td></tr><tr><td>Dynamic set</td><td><code>{•}</code> <em>or</em> <code>[• ^U..D]</code></td><td>From <code>U</code> to <code>D</code>, up to 2^64</td></tr></tbody></table>

### Enums

Enums are a special case of unit type in which each variant is represented by a `Byte` value.

### Dynamic collections

Fundamental morphisms can be used to build more advanced types, like dynamic maps and dynamic arrays of tuples

<table><thead><tr><th width="222.33333333333331"></th><th width="246">Syntax form</th><th>No of elements</th></tr></thead><tbody><tr><td>Dynamic map</td><td><code>{• -> ^U..D •}</code></td><td>From <code>U</code> to <code>D</code>, up to 2^64</td></tr><tr><td>Dynamic array of tuples</td><td><code>[•, • ^U..D]</code> <em>or</em><br><code>[(•, •) ^U..D]</code></td><td>From <code>U</code> to <code>D</code>, up to 2^64</td></tr></tbody></table>

Construction `^U..D` used in type expression specifying minimum and maximum size of a dynamic collection is called *confinement bounds*. It can be seen as an upper and lower indexes on the possible number of elements, i.e. type definition `[Byte ^ 1..20]` can be read as $$\bigotimes^1\_{20} byte$$ and means product type with dynamic number of fields, from 1 to 20 max, where each field is a byte - or, in more common terms, an byte array of dynamic size which can't have less than one byte - and can't grow larger than 20 bytes.

For simplifying syntax strict encoding provides comprehensions and defaults for specifying the confinement bounds:

<table><thead><tr><th width="195">Comprehension</th><th width="198.33333333333331">Expands to</th><th>Comment</th></tr></thead><tbody><tr><td><code>[•]</code></td><td><code>[• ^ 0..0xFFFF]</code></td><td>Default number of elements in confined collections is from zero to 2^16</td></tr><tr><td><code>[•+]</code>or<br><code>[•^1..]</code></td><td><code>[• ^ 1..0xFFFF]</code></td><td>Collection which must contain at least  one item</td></tr><tr><td><code>[•^U]</code></td><td><code>[• ^ U..0xFFFF]</code></td><td>Collection with minimum of <code>U</code> items</td></tr><tr><td><code>[•^..D]</code></td><td><code>[• ^ 0..D]</code></td><td>Collection having maximum of <code>D</code> items</td></tr></tbody></table>

Please note that type expression of `[•^N..N]`is not allowed, since it means "dynamic" collection with a fixed number of items, which is nonsense, so please use `[•^N]` instead.

### Optionals

A special case of union type of frequent use is an optional monad, which may contain some type or be `None`. In strict encoding there is a special comprehension for writing an optional: `T?`, which is an equivalend ot writing `(()|T)`.

### Types provided by the standard library

Most frequently used types are provided by a strict encoding standard library `StdLib`:

<table><thead><tr><th width="163">Sten type</th><th>Type definition</th><th>Rust type from amplify library</th></tr></thead><tbody><tr><td><code>Bytes</code></td><td><code>[Byte]</code></td><td><code>SmallVec&#x3C;u8></code></td></tr><tr><td><code>Blob</code></td><td><code>[Byte^..0xFFFFFF]</code></td><td><code>MediumVec&#x3C;u8></code></td></tr><tr><td><code>String</code></td><td><code>[Utf8]</code></td><td><code>SmallString</code></td></tr><tr><td><code>Text</code></td><td><code>[Utf8^..0xFFFFFF]</code></td><td><code>MediumString</code></td></tr><tr><td><code>Ascii</code></td><td>type definition too long</td><td><code>AsciiChar</code></td></tr></tbody></table>

<br>


# Type semantics and layout

This chapter introduces and explains three main concepts:

* Type semantics
* Type memory layout
* Type serialization

Each data type in strict types is a **semantic** type, which has some **memory layout**.

Two different types may have the same memory layout - but they are still different types. For instance, both date of month and age of a person can be represented by a single byte in memory - but semantically these are two different types, which instances can't be directly compared or ordered (a person aged 27 is neither can be classified to be "before" or "after" 27 day of any month).

## Type semantics and ids

*Strict types commit to data semantics*, and that commitment represents a **strict type semantic id** (`SemId`). The semantics of a type includes the following information:

1. Memory layout: number of apples on a tree representable as `U16` and in the whole world, representable as `U64` are all different types;
2. Type composition, which includes the information about ordering and naming of all fields or variants of the composed types, is required to distinguish types like `Result<A,B>` from `ControlFlow<A,B>`
3. Type name: two types with the same memory layout and composition still are distinct types. This is required to distinguish a number of apples from a number of oranges: both have the same memory layout and composition, but different semantics.

To achieve this, semantic type id is computed as a SHA2-256 hash of:

1. Type name
2. Names of all fields/variants
3. Semantic identifiers for each of the fields/variants

{% hint style="info" %}
Two strict types are equal only and only if their semantic ids are equal - and otherwise, if two semantic type ids are equal, the corresponding types are equal.
{% endhint %}

This approach allows tracking any breaking changes in types, and formally verifies that new releases of a library do not contain breaking changes in data types, which is important for consensus and networking protocols, data persistence and many other applications.

## Type libraries and type system

Types are structured into type libraries. The type library is a collection of data types, which may depend on other libraries. The library commits to the semantic type ids of its types. Types which use references to types from other libraries commit to both the library id and semantic id of the external types.

Circular dependencies between types from different are not allowed, thus any set of strict types (type library or type system) always represents a DAG.