Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Datatypes

SAIL provides algebraic data types (ADTs) for defining structured values. An ADT declares a named type together with one or more constructors. Each constructor describes one way to build a value of that type and may carry zero or more fields of arbitrary types.

enum Option<A> {
    None,
    Some(A)
}

Data types may be defined at the top level of a source file or inside a contract body.

Enumeration Types

The simplest kind of algebraic data type has only nullary constructors with no fields. Such a type acts as a finite enumeration.

enum TokenStatus {
    Active,
    Paused,
    Deprecated
}

Each constructor is a distinct value of the type. Enumerations are commonly used wherever Solidity uses enum.

contract Registry {
    enum TokenStatus {
        Active,
        Paused,
        Deprecated
    }

    function statusCode(s: TokenStatus) returns (word) {
        match (s) {
            case TokenStatus.Active {
                return 1;
            }
            case TokenStatus.Paused {
                return 2;
            }
            case TokenStatus.Deprecated {
                return 0;
            }
        }
    }

    function main() returns (word) {
        return statusCode(TokenStatus.Active);
    }
}

Constructors with Fields

A constructor can carry one or more fields. The field types are listed in parentheses, separated by commas.

enum TxStatus {
    Pending,
    Settled,
    Failed
}

enum TxOutcome {
    Success(TxStatus),
    Revert(TxStatus),
    Unknown
}

A constructor with fields is applied like a function: TxOutcome.Success(TxStatus.Settled) produces a value of type TxOutcome wrapping a value of type TxStatus.

Enum-constructor payloads are extracted by pattern matching; unlike named struct fields, positional payloads have no record-style field access. The pattern mirrors the constructor application:

function outcomeCode(x: TxOutcome) returns (word) {
    match (x) {
        case TxOutcome.Success(TxStatus.Settled) {
            return 1;
        }
        case TxOutcome.Revert(TxStatus.Failed) {
            return 2;
        }
        default {
            return 0;
        }
    }
}

Parametric Data Types

A data type can be parameterized by one or more type variables, making it a generic or parametric type. The type variables are listed in angle brackets after the type name.

enum Option<A> {
    None,
    Some(A)
}

Here A is a type variable. Option<word> is the type of optional words, Option<bool> is the type of optional booleans, and so on. The type variable A may appear in the field types of any constructor.

contract Option {
    enum Option<A> {
        None,
        Some(A)
    }

    function just<A>(x: A) returns (Option<A>) {
        return Option.Some(x);
    }

    function maybe(defaultValue: word, opt: Option<word>) returns (word) {
        match (opt) {
            case Option.None {
                return defaultValue;
            }
            case Option.Some(x) {
                return x;
            }
        }
    }

    function main() returns (word) {
        return maybe(0, Option.Some(42));
    }
}

The type checker verifies that every use of a parametric type supplies the correct number of type arguments. Applying Option to two arguments, for instance, is a type error.

Nested Pattern Matching

Patterns may be nested to arbitrary depth to match inside multiple layers of constructors in a single arm.

enum Option<A> {
    None,
    Some(A)
}

// Unwrap an approval amount nested in two Option layers.
function resolveApproval(outer: Option<Option<word>>) returns (Option<word>) {
    match (outer) {
        case Option.Some(Option.Some(x)) {
            return Option.Some(x);
        }
        default {
            return Option.None;
        }
    }
}

The wildcard _ matches any value without binding it. It can appear at any depth in a pattern.

Opaque Wrappers

A single-constructor, single-field type is the standard idiom for introducing a distinct type that is represented by an existing type at runtime. This is similar to Haskell's newtype or Solidity's user-defined value types.

enum uint256 {
    uint256(word)
}

uint256 is a type distinct from word even though it carries exactly one word field. The type checker treats them as incompatible, preventing accidental mixing. The wrapper is removed during compilation: uint256 values occupy exactly one EVM word, just like word.

Wrapping and unwrapping are done explicitly with the constructor and a pattern:

function wrap(x: word) returns (uint256) {
    return uint256(x);
}

function unwrap(x: uint256) returns (word) {
    match (x) {
        case uint256(w) {
            return w;
        }
    }
}

The standard library defines uint256, bytes4, bytes32, and address this way, each wrapping word.

Phantom Type Parameters

A type parameter that does not appear in any constructor field is called a phantom type parameter. It carries no runtime information but allows the type system to distinguish values that would otherwise be identical.

// A is phantom: the constructor Proxy carries no field of type A.
enum Proxy<A> {
    Proxy
}

Proxy<word> and Proxy<bool> are distinct types at compile time but produce the same runtime value. Phantom types are useful for passing type information to functions without allocating extra memory.

trait MemoryType<A> {
    function size(prx: Proxy<A>) returns (word);
}

impl MemoryType<word> {
    function size(prx: Proxy<word>) returns (word) {
        return 32;
    }
}

The Proxy<A> argument lets the caller select which MemoryType implementation to use without passing an actual value of type A.

Note Because phantom type parameters leave the constructor's result type partially undetermined, the type checker requires an explicit type annotation whenever a Proxy value is constructed in a context where the type cannot be inferred from surrounding expressions. Use an explicit conversion, Proxy as Proxy<word>, to resolve the ambiguity.

Tuples

SAIL has built-in support for product types (tuples). A tuple type is written as a parenthesised, comma-separated list of component types. Tuple values are written the same way.

function swap(p: (word, bool)) returns ((bool, word)) {
    match (p) {
        case (x, b) {
            return (b, x);
        }
    }
}

Tuples of more than two elements are right-nested pairs internally. The type (word, bool, word) is represented as pair<word, pair<bool, word>>.

The unit type () is the zero-element tuple. It carries no information and is used as the return type of functions that exist only for their side effects.

function storeBalance(account: word, amount: word) {
    assembly { sstore(account, amount) }
}

Note Tuple patterns may appear anywhere a pattern is expected, including inside constructor patterns:

impl<A, B> Nth<Zero, (A, B), A> {
    function nth(idx: Proxy<Zero>, tup: (A, B)) returns (A) {
        match (tup) {
            case (x, _) {
                return x;
            }
        }
    }
}

Contextual Constructor Syntax

In a context where the expected type is known, the module qualifier can be omitted from a constructor name by prefixing it with .. The compiler resolves the constructor to the appropriate type automatically.

enum Option<A> {
    None,
    Some(A)
}

function just(x: word) returns (Option<word>) {
    return .Some(x);   // equivalent to Option.Some(x)
}

function nothing() returns (Option<word>) {
    return .None;      // equivalent to Option.None
}

The same shorthand works in patterns:

function isNone(o: Option<word>) returns (bool) {
    match (o) {
        case .None {
            return true;
        }
        case .Some(_) {
            return false;
        }
    }
}

The compiler reports an error if the expected type is not known or if the constructor name is ambiguous.

Type Synonyms

A type synonym introduces a new name for an existing type. Synonyms are purely a compile-time device: the compiler expands them before type checking and they leave no trace in the generated code.

type Int = word;
type Point = pair<Int, Int>;

function makePoint(x: Int, y: Int) returns (Point) {
    return (x, y);
}

function getX(p: Point) returns (Int) {
    match (p) {
        case (x, _) {
            return x;
        }
    }
}

Synonyms can have type parameters, written in parentheses after the name:

type Map(k, v) = pair<k, v>;   // toy example

Warning Recursive type synonyms are not allowed. A synonym must not refer directly or indirectly to itself. Attempting to define type A = B; and type B = A; simultaneously is a compile-time error.

Runtime Encoding

Algebraic data types compile to a uniform binary encoding in the generated Hull/Yul code.

Sum types (types with more than one constructor) are encoded as nested binary sums using inl (left injection) and inr (right injection). A type with n constructors becomes a right-nested binary tree of depth ⌈log₂ n⌉. For example, a three-constructor type enum T { A, B, C } is encoded as:

A  →  inl ()
B  →  inr (inl ())
C  →  inr (inr ())

Product types (constructor fields, tuples) are encoded as right-nested pairs. The three-field constructor enum T { T(word, bool, word) } becomes pair<word, pair<bool, word>>.

This uniform encoding is what the match compiler and the Hull back-end operate on. It is not visible at the SAIL level.