4.2. Algebraic datatypes🔗

A datatype declares a value built from a fixed set of constructors. Laurel generates a constructor, a tester, and one selector per field:

The checked selector carries a precondition that the value really was built with a constructor containing that field, so reading it is a proof obligation. The unchecked ! variant skips that obligation; use the checked one unless the constructor is already established.

datatype Option<T> {
  Nothing(),
  Some(value: T)
}

procedure unwrapOr(o: Option<int>, fallback: int): int
{
  return if Option..isSome(o)
    then Option..value(o)
    else fallback
};

Datatypes have structural equality — two values are equal when they have the same constructor and equal arguments — which is what distinguishes them from composites. Recursive and mutually recursive datatypes are supported.

Two naming rules are easy to trip over. Constructor names are program-global, so they must not collide across datatypes. And field names must be unique across all constructors of one datatype, because every field generates one datatype-wide selector <Datatype>..<field>: a declaration Left(value: T), Right(value: T) is rejected, because both fields would define Datatype..value. Use distinct names such as leftValue and rightValue.

Laurel has no pattern-matching syntax. Testers and selectors, combined with if, are how a datatype is taken apart.