# 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

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
```

```val append (#a:Type) (l1 l2:list a)