Defining Data Types in Juvix

A crucial aspect of any programming language is the ability to define custom data types. In Juvix, these are known as inductive types. An inductive type is a type with elements constructed from a finite set of constructors.

Consider as a first example where we define a data type Bool with two constructors, true and false.

type Bool :=
  | true : Bool
  | false : Bool;

Syntax of Data Type Declaration

General Declaration

The declaration of a data type in Juvix consists of the keyword type, followed by a unique name, optional type parameters, and constructors.

type <name> <type-parameters> :=
    | <constructor1> : <type1>
    | ...
    | <constructorn> : <typen>;

In this syntax:

• <name> represents a unique name for the declared data type.
• <type-parameters> denote optional type parameters in the form A B C ... or with typing information (A : Type). These parameters define the return type of the constructors, i.e., <name> <type-parameters>.
• <constructor1> through <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.

While there are variations in the syntax for declaring a data type (see the ADT syntax and record syntax), the most general syntax is the one outlined above.

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 of 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> <type-parameters> :=
  | <constructor1> <arg1-1> ... <arg1-n>
  | ...
  | <constructorN> <argn-1> ... <argn-n>;

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:

module Nat-ADT;
  type Nat :=
    | Z
    | S Nat;
end;

Another example is the List type, which is polymorphic in the type of its elements.

module List-ADT;
  type List A :=
    | Nil
    | Cons A (List A);
end;

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.

module membership;
  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;
end;

For more examples of inductive types and how to use them, see the Juvix standard library.