# Inductive types and pattern matching

In this chapter, you’ll learn how to define new types in F*. These
types are called *inductive types*, or, more informally,
datatypes. We’ll also learn how to define functions over these
inductive types by pattern matching and to prove properties about
them.

Note

We’ll only cover the most basic forms of inductive types here. In particular, the types we show here will not make use of indexing or any other form of dependent types—we’ll leave that for a later chapter.

## Enumerations

We’ve seen that `unit`

is the type with just one element `()`

and
that `bool`

is the type with two elements, `true`

and `false`

.

You can define your own types with an enumeration of elements, like so.

```
type three =
| One_of_three : three
| Two_of_three : three
| Three_of_three : three
```

This introduces a new type `three : Type`

, and three *distinct*
constants `One_of_three : three`

, `Two_of_three : three`

,
`Three_of_three : three`

. These constants are also called
“constructors” or “data constructors”. The name of a constructor must
begin with an uppercase letter.

Note

In this case, it may seem redundant to have to write the type of
each constructor repeatedly—of course they’re all just constructors
of the type `three`

. In this case, F* will allow you to just
write

```
type three =
| One_of_three
| Two_of_three
| Three_of_three
```

However, in general, as we start to use indexed types, each constructor can build a different instance of the defined type, so it will be important to have a way to specify the result type of each constructor. For uniformity, throughout this book, we’ll always annotate the types of constructors, even when not strictly necessary.

F* can prove that they are distinct and that these are the only terms
of type `three`

.

```
let distinct = assert (One_of_three <> Two_of_three /\
Two_of_three <> Three_of_three /\
Three_of_three <> One_of_three)
let exhaustive (x:three) = assert (x = One_of_three \/
x = Two_of_three \/
x = Three_of_three)
```

To write functions that case analyze these new types, one uses the
`match`

construct. The syntax of `match`

in F* is very similar to
OCaml or F#. We’ll assume that you’re familiar with its basics. As we
go, we’ll learn about more advanced ways to use `match`

.

Here are some examples.

```
let is_one (x:three)
: bool
= match x with
| One_of_three -> true
| _ -> false
let is_two (x:three)
: bool
= match x with
| Two_of_three -> true
| _ -> false
let is_three (x:three)
: bool
= match x with
| Three_of_three -> true
| _ -> false
```

### Discriminators

These functions test whether `x : three`

matches a given
constructor, returning a `bool`

in each case. Since it’s so common
to write functions that test whether a value of an inductive type
matches one of its constructors, F* automatically generates these
functions for you. For example, instead of writing

```
let three_as_int (x:three)
: int
= if is_one x then 1
else if is_two x then 2
else 3
```

One can write:

```
let three_as_int' (x:three)
: int
= if One_of_three? x then 1
else if Two_of_three? x then 2
else 3
```

In other words, for every constructor `T`

of an inductive type
`t`

, F* generates a function named `T?`

(called a “discriminator”)
which tests if a `v:t`

matches `T`

.

### Exhaustiveness

Of course, an even more direct way of writing `three_as_int`

is

```
let three_as_int'' (x:three)
: int
= match x with
| One_of_three -> 1
| Two_of_three -> 2
| Three_of_three -> 3
```

Every time you use a `match`

, F* will make sure to prove that you
are handling all possible cases. Try omitting one of the cases in
`three_as_int`

above and see what happens.

Exhaustiveness checking in F* is a semantic check and can use the SMT solver to prove that all cases are handled appropriately. For example, you can write this:

```
let only_two_as_int (x:three { not (Three_of_three? x) })
: int
= match x with
| One_of_three -> 1
| Two_of_three -> 2
```

The refinement on the argument allows F* to prove that the
`Three_of_three`

case in the pattern is not required, since that
branch would be unreachable anyway.

## Tuples

The next step from enumerations is to define composite types, e.g., types that are made from pairs, triples, quadruples, etc. of other types. Here’s how

```
type tup2 (a:Type) (b:Type) =
| Tup2 : fst:a -> snd:b -> tup2 a b
type tup3 a b c =
| Tup3 : fst:a -> snd:b -> thd:c -> tup3 a b c
```

The type definition for `tup2 a b`

states that for any types ```
a :
Type
```

and `b : Type`

, `Tup2 : a -> b -> tup2 a b`

. That is,
`Tup2`

is a constructor of `tup2`

, such that given `x:a`

and
`y:b`

, `Tup2 x y : tup2 a b`

.

The other types `tup3`

and `tup4`

are similar—the type
annotations on the bound variables can be inferred.

These are inductive types with just one case—so the discriminators
`Tup2?`

, `Tup3?`

, and `Tup4?`

aren’t particularly useful. But,
we need a way to extract, or *project*, the components of a tuple. You
can do that with a `match`

.

```
let tup2_fst #a #b (x:tup2 a b)
: a
= match x with
| Tup2 fst _ -> fst
let tup2_snd #a #b (x:tup2 a b)
: b
= match x with
| Tup2 _ snd -> snd
let tup3_fst #a #b #c (x:tup3 a b c)
: a
= match x with
| Tup3 fst _ _ -> fst
let tup3_snd #a #b #c (x:tup3 a b c)
: b
= match x with
| Tup3 _ snd _ -> snd
let tup3_third #a #b #c (x:tup3 a b c)
: c
= match x with
| Tup3 _ _ thd -> thd
```

### Projectors

These projectors are common enough that F* auto-generates them for
you. In particular, for any data constructor `T`

of type
`x1:t1 -> ... -> xn:tn -> t`

, F* auto-generates the following function:

`T?.xi : y:t{T? y} -> ti`

That is, `T?.xi`

is a function which when applied to a `y:t`

in
case `T? y`

, returns the `xi`

component of `T x1 ... xn`

.

In the case of our `tup2`

and `tup3`

types, we have

`Tup2?.fst`

,`Tup2?.snd`

`Tup3?.fst`

,`Tup3?.snd`

,`Tup3?.thd`

### Syntax for tuples

Since tuples are so common, the module `FStar.Pervasives.Native.fst`

defines tuple types up to arity 14. So, you shouldn’t have to define
`tup2`

and `tup3`

etc. by yourself.

The tuple types in `FStar.Pervasives.Native`

come with syntactic
sugar.

You can write

`a & b`

instead of the`tup2 a b`

;`a & b & c`

instead of`tup3 a b c`

; and so on, up to arity 14.You can write

`x, y`

instead of`Tup2 x y`

;`x, y, z`

instead of`Tup3 x y z`

; an so on, up to arity 14.You can write

`x._1`

,`x._2`

,`x._3`

, etc. to project the field`i`

of a tuple whose arity is at least`i`

.

That said, if you’re using tuples beyond arity 4 or 5, it’s probably a
good idea to define a *record*, as we’ll see next—since it can be hard
to remember what the components of a large tuple represent.

### Records

A record is just a tuple with user-chosen names for its fields and with special syntax for constructing then and projecting their fields. Here’s an example.

```
type point3D = { x:int; y:int; z:int}
let origin = { y=0; x=0; z=0 }
let dot (p0 p1:point3D) = p0.x * p1.x + p0.y * p1.y + p0.z * p1.z
let translate_X (p:point3D) (shift:int) = { p with x = p.x + shift}
let is_origin (x:point3D) =
match x with
| {z=0;y=0;x=0} -> true
| _ -> false
```

A record type is defined using curly braces

`{}`

. See`type point3D`

A record value is also constructed using curly braces, with an assignment for each field of the record. The fields need not be given in order. See

`origin`

.To access the fields of a record, you can use the dot notation

`p.x`

; See`dot`

, which computes a dot product using dot notation.Records also support the

`with`

notation to construct a new record whose fields are the same as the old record, except for those fields mentioned after the`with`

. That is,`translate_X p shift`

returns`{ x = p.x + shift; y = p.y; z = p.z}`

.Records can also be used to pattern match a value. For example, in

`is_origin`

, we match the fields of the record (in any order) against some patterns.

## Options

Another common type from F*’s standard library is the `option`

type,
which is useful to represent a possibly missing value.

Consider implementing a function to divide `x / y`

, for two integers
`x`

and `y`

. This function cannot be defined when `y`

is zero,
but it can be defined partially, by excluding the case where ```
y =
0
```

, as shown below. (Of course, one can also refine the domain of the
function to forbid `y = 0`

, but we’re just trying to illustrate the
`option`

type here.)

```
let try_divide (x y:int)
: option int
= if y = 0 then None else Some (x / y)
let divide (x:int) (y:int{y<>0}) = x / y
```

Like most other functional languages, F* does not have a `null`

value. Whenever a value may possibly be `null`

, one typically uses
the `option`

type, using `None`

to signify null and `Some v`

for
the non-null case.

## Unions, or the `either`

type

`FStar.Pervasives`

also defines the `either`

type, shown below.

```
type either a b =
| Inl : v: a -> either a b
| Inr : v: b -> either a b
```

The type `either a b`

represents a value that could either be ```
Inl
v
```

with `v:a`

, or `Inr v`

with `v:b`

. That is, `either a b`

is a tagged union of the `a`

and `b`

. It’s easy to write functions
to analyze the tag `Inl`

(meaning it’s “in the left case”) or
`Inr`

(“in the right case”) and compute with the underlying
values. Here’s an example:

```
let same_case #a #b #c #d (x:either a b) (y:either c d)
: bool
= match x, y with
| Inl _, Inl _
| Inr _, Inr _ -> true
| _ -> false
let sum (x:either bool int) (y:either bool int{same_case x y})
: z:either bool int{ Inl? z <==> Inl? x}
= match x, y with
| Inl xl, Inl yl -> Inl (xl || yl)
| Inr xr, Inr yr -> Inr (xr + yr)
```

The `same_case x y`

function decides if the two unions are both
simultaneously in the left or right case.

Then, in `sum x y`

, with a refinement that `x`

and `y`

are in
the same case, we can handle just two cases (when they are both in
left, or both in right) and F* can prove that the case analysis is
exhaustive. In the left case, the underlying values are boolean, so we
combine them with `||`

; in the right case, the underlying values are
integers, so we combine them with `+`

; and return them with the
appropriate tag. The type of the result ```
z:either bool int{ Inl? z <==>
Inl? x}
```

shows that the result has the same case as `x`

(and hence
also `y`

). We could have written the result type as ```
z:either bool
int { same_case z x }
```

.

## Lists

All the types we’ve see far have been inductive only in a degenerate sense—the constructors do not refer to the types they construct. Now, for our first truly inductive type, a list.

Here’s the definition of `list`

from `Prims`

:

```
type list a =
| Nil : list a
| Cons : hd:a -> tl:list a -> list a
```

The `list`

type is available implicitly in all F* programs and we
have special (but standard) syntax for the list constructors:

`[]`

is`Nil`

`[v1; ...; vn]`

is`Cons v1 ... (Cons vn Nil)`

`hd :: tl`

is`Cons hd tl`

.

You can always just write out the constructors like Nil and Cons
explicitly, if you find that useful (e.g., to partially apply ```
Cons
hd : list a -> list a
```

).

### Length of a list

Let’s write some simple functions on lists, starting with computing the length of a list.

```
let rec length #a (l:list a)
: nat
= match l with
| [] -> 0
| _ :: tl -> 1 + length tl
```

The `length`

function is recursive and implicitly polymorphic in a
type `a`

. For any list `l : list a`

, `length l`

returns a
`nat`

. The definition pattern matches on the list and calls
`length`

recursively on the tail of list, until the `[]`

case is
reached.

## Exercises

Click here for the exercise file.

Here’s the definition of `append`

, a function that concatenates two
lists. Can you give it a type that proves it always returns a list
whose length is the sum of the lengths of its arguments.

```
let rec append l1 l2
= match l1 with
| [] -> l2
| hd :: tl -> hd :: append tl l2
```

**Answer**

```
val append (#a:Type) (l1 l2:list a)
: l:list a { length l = length l1 + length l2 }
```