Data Types¶
A data type, also known as an inductive type, is a type with elements constructed from a finite set of constructors.
In the following example, we define a data type Bool
with two constructors,
true
and false
.
type Bool :=
 true : Bool
 false : Bool;
A declaration of a data type
consists of the keyword type
, followed by a unique name, type parameters, and
constructors.
type <name> <typeparameters> :=
 <constructor1> : <type1>
 ...
 <constructorn> : <typen>;
The syntax for declaring a data type varies (see the ADT syntax and record syntax) but the most general syntax is the one above.
In this syntax:

<name>
represents a unique name for the declared data type. 
<typeparameters>
denote type parameters in the formA B C ...
or with typing information(A : Type)
. These parameters are optional and define the return type of the constructors, i.e.,<name> <typeparameters>
. 
<constructor1>
...<constructorn>
are the constructors of the data type. Each constructor has a unique name and a type, which can be the type of the declared data type or a function type from the types of the arguments to the type of the declared data type.
Note
A data type declaration implicitly declares a module with the same name as the data type, containing the symbols of the constructors, and the type of the data type itself. One can open this module to access these symbols or hide it to prevent access to them.
Example data types¶
The Unit
type, the simplest data type, has a single constructor named unit
.
type Unit := unit : Unit;
We then declare the Nat
type, representing unary natural numbers. It
introduces two constructors: zero
and suc
. For instance, suc zero
represents one, while suc (suc zero)
represents two.
type Nat :=
 zero : Nat
 suc : Nat > Nat;
These constructors function as regular functions or patterns in pattern matching when defining functions. Here is an example of a function adding two natural numbers:
syntax operator + additive;
+ : Nat > Nat > Nat
 zero b := b
 (suc a) b := suc (a + b);
ADT syntax¶
As an alternative to the above syntax, we can use a more familiar and compact syntax for declaring data types. This syntax is inspired by ADT syntax in Haskell.
type <name> <typeparameters> :=
 <constructor1> <arg11> ... <arg1n>
 ...
 <constructorN> <argn1> ... <argnn>;
Different from the previous presentation, here the constructors do not have typing information.
If a type constructor as above has no arguments, then its type is the type of the data type being declared. In the case the type constructor has arguments, then its type is the function type from the types of the arguments to the type of the data type being declared.
For example, the Nat
type can be declared as follows:
type Nat :=
 Z
 S Nat;
Another example is the List
type, which is polymorphic in the type of its
elements.
type List A :=
 Nil
 Cons A (List A);
Polymorphic data type¶
A data type can possess type parameters. When a data type has a type parameter
A
, it is referred to as polymorphic in A
.
A classic example of this concept is the List
type, which is polymorphic in
the type of its list elements.
syntax operator :: cons;
type List (A : Type) :=
 nil : List A
 :: : A > List A > List A;
The following function determines whether an element is in a list or not.
import Stdlib.Data.Bool open using {Bool; false; };
elem {A} (eq : A > A > Bool) (s : A) : List A > Bool
 nil := false
 (x :: xs) := eq s x  elem eq s xs;
For more examples of inductive types and how to use them, see the Juvix standard library.