User-defined data types

A user-defined data type is introduced with the type keyword and a modifier unique or structural. The modifier indicates if the type is unique by its name, or if it is unique only by its structure. It is optional for unique types, since that is the more common case. (See Types for an informal description of Unison's type system.)

For example:

structural type Optional a
structural type Optional a
  = lib.base.Optional.None
  | lib.base.Optional.Some a

or

type UserId
type UserId
  = docs.languageReference.userDefinedDataTypes.UserId.Email Text
  | docs.languageReference.userDefinedDataTypes.UserId.Phone Nat

The = sign splits the definition into a left-hand side and a right-hand side, much like term definitions.

The left-hand side is the data type being defined. It gives a name for the data type and declares a new type constructor with that name (here it's named Optional), followed by names for any type arguments (here there is one and it’s called a). These names are bound as type variables in the right-hand side. The right-hand side may also refer to the name given to the type in the left-hand side, in which case it is a recursive type declaration. Note that the fully saturated type construction Optional Nat is a type, whereas Optional by itself is a type constructor, not a type (it requires a type argument in order to construct a type).

The right-hand side consists of zero or more data constructors separated by |. These are data constructors for the type, or ways in which values of the type can be constructed. Each case declares a name for a data constructor (here the data constructors are Optional.None and Some), followed by the types of the arguments to the constructor.

When Unison compiles a type definition, it generates a term for each data constructor. Here they are the terms Some : a -> Optional a, and Optional.None : Optional a. It also generates patterns for matching on data (see Pattern Matching).

Note that these terms and patterns receive qualified names: if the type named x.y.Z has a data constructor C, the generated term and pattern for C will be named x.y.Z.C.

The general form of a type declaration is as follows:

<unique|structural<[<regular-identifier>]?>?> type TypeConstructor p1 p2 … pn
  = DataConstructor_1
  | DataConstructor_2
  ..
  | DataConstructor_n

Generalized algebraic data types (GADTs)

The where form of a data declaration gives each constructor an explicit type, including its result type. Constructors can specialize the type's parameters, called indices, to different types:

type Expr a where
  NatLit : Nat -> Expr Nat
  BoolLit : Boolean -> Expr Boolean
  Add : Expr Nat -> Expr Nat -> Expr Nat
  If : Expr Boolean -> Expr a -> Expr a -> Expr a

Here NatLit constructs Expr Nat, BoolLit constructs Expr Boolean, and If is polymorphic in its result index. Indices can also be compound types or repeated type variables. The structural and unique modifiers apply to where declarations as they do to = declarations.

Matching a constructor refines the index within that branch. A match that depends on this refinement needs the type of the value being matched to be known; a function signature such as eval : Expr a -> a supplies it. Matches that return the same type regardless of the index can still have their types inferred.

Exhaustiveness checking uses the index to rule out impossible constructors. For example, a match on Expr Nat needs NatLit, Add, and If cases, but no BoolLit case.

See GADTs in the language guide for a complete evaluator, annotation examples, structured indices, and equality witnesses.