# Equality Types

In an early section we learned that F*
supports at least two kinds of equality. In this section, we look in
detail at definitional equality, propositional equality, extensional
equality of functions, and decidable equality. These topics are fairly
technical, but are core features of the language and their treatment
in F* makes essential use of an indexed inductive type, ```
equals #t x
y
```

, a proposition asserting the equality of `x:t`

and `y:t`

.

Depending on your level of comfort with functional programming and dependent types, you may want to skip or just skim this chapter on a first reading, returning to it for reference if something is unclear.

## Definitional Equality

One of the main distinctive feature of a type theory like F* (or Coq,
Lean, Agda etc., and in contrast with foundations like set theory) is
that *computation* is a primitive notion within the theory, such that
lambda terms that are related by reduction are considered
identical. For example, there is no way to distinguish within the
theory between \((\lambda x.x) 0\) and \(0\), since the former
reduces in a single step of computation to the latter. Terms that are
related by reduction are called *definitionally equal*, and this is
the most primitive notion of equality in the language. Definitional
equality is a congruence, in the sense that within any context
\(T[]\), \(T[n]\) is definitionally equal to \(T[m]\),
when \(n\) and \(m\) are definitionally equal.

Since definitionally equal terms are identical, all type theories,
including F*, will implicit allow treating a term `v:t`

as if it had
type `t'`

, provided `t`

and `t'`

are definitionally equal.

Let’s look at a few examples, starting again with our type of length-indexed vectors.

```
type vec (a:Type) : nat -> Type =
| Nil : vec a 0
| Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)
```

As the two examples below show a `v:vec a n`

is also has type ```
vec
a m
```

when `n`

and `m`

are definitionally equal.

```
let conv_vec_0 (#a:Type) (v:vec a ((fun x -> x) 0))
: vec a 0
= v
let conv_vec_1 (#a:Type) (v:vec a ((fun x -> x + 1) 0))
: vec a 1
= v
```

In the first case, a single step of computation (a function
application, or \(\beta\)-reduction) suffices; while the second
case requires a \(\beta\)-reduction followed by a step of integer
arithmetic. In fact, any computational step, including unfolding
defintions, conditionals, fixpoint reduction etc. are all allowed when
deciding if terms are definitionally equivalent—the code below
illustrates how F* implicitly reduces the `factorial`

function when
deciding if two terms are definitionally equal.

```
let rec factorial (n:nat)
: nat
= if n = 0 then 1
else n * factorial (n - 1)
let conv_vec_6 (#a:Type) (v:vec a (factorial 3))
: vec a 6
= v
```

Of course, there is nothing particularly special about the `vec`

type or its indices. Definitional equality applies everywhere, as
illustrated below.

```
let conv_int (x : (fun b -> if b then int else bool) true)
: int
= x + 1
```

Here, when adding `1`

to `x`

, F* implicitly converts the type of
`x`

to `int`

by performing a \(\beta\)-reduction followed by a
case analysis.

## Propositional Equality

Definitional equality is so primitive in the language that there is no
way to even state within the terms that two terms are definitional
equal, i.e., there is no way to state within the logic that two terms
are related to each other by reduction. The closest one can get
stating that two terms are equal is through a notion called a
*provable equality* or propositional equality.

In thinking of propositions as types, we mentioned at the very
start of the book, that one can think of a type `t`

as a
proposition, or a statement of a theorem, and `e : t`

as a proof of
the theorem `t`

. So, one might ask, what type corresponds to the
equality proposition and how are proofs of equality represented?

The listing below shows the definition of an inductive type ```
equals
#a x y
```

representing the equality proposotion between `x:a`

and
`y:a`

. Its single constructor `Reflexivity`

is an equality proof.

```
type equals (#a:Type) : a -> a -> Type =
| Reflexivity : #x:a -> equals x x
```

Its easy to construct some simple equality proofs. In the second case,
just as with our vector examples, F* accepts `Reflexivity #_ #6`

as
having type `equals (factorial 3) 6`

, since `equals 6 6`

is
definitionally equal to `equals (factorial 3) 6`

.

```
let z_equals_z
: equals 0 0
= Reflexivity
let fact_3_eq_6
: equals (factorial 3) 6
= Reflexivity #_ #6
```

Although the only constructor of `equals`

is `Reflexivity`

, as the
the following code shows, `equals`

is actually an equivalence
relation, satisfying (in addition to reflexivity) the laws of symmetry
and transitivity.

```
let reflexivity #a (x:a)
: equals x x
= Reflexivity
let symmetry #a (x y : a) (pf:equals x y)
: equals y x
= Reflexivity
let transitivity #a (x y z : a) (pf1:equals x y) (pf2:equals y z)
: equals x z
= Reflexivity
```

This might seem like magic: how is it is that we can derive symmetry and transitivity from reflexivity alone? The answer lies in how F* interprets inductive type definitions.

In particular, given an inductive type definition of type \(T~\overline{p}\), where \(\overline{p}\) is a list of parameters and, F* includes an axiom stating that any value \(v: T~\overline{p}\) must be an application of one of the constructors of \(T\), \(D~\overline{v} : T~\overline{p'}\), such that \(\overline{p} = \overline{p'}\).

In the case of equality proofs, this allows F* to conclude that every
equality proof is actually an instance of `Reflexivity`

, as shown
below.

```
let uip_refl #a (x y:a) (pf:equals x y)
: equals pf (Reflexivity #a #x)
= Reflexivity
```

Spend a minute looking at the statement above: the return type is a
statement of equality about equality proofs. Write down a version of
`uip_refl`

making all implicit arguments explicit.

**Answer**

```
let uip_refl_explicit #a (x y:a) (pf:equals x y)
: equals #(equals x y) pf (Reflexivity #a #x)
= Reflexivity #(equals x y) #(Reflexivity #a #x)
```

In fact, from `uip_refl`

, a stronger statement showing that all
equality proofs are equal is also provable. The property below is
known as the *uniqueness of identity proofs* (UIP) and is at the core
of what makes F* an extensional type theory.

```
let uip #a (x y:a) (pf0 pf1:equals x y)
: equals pf0 pf1
= Reflexivity
```

The F* module `Prims`

, the very first module in every program’s
dependence graph, defines the `equals`

type as shown here. The
provable equality predicate `(==)`

that we’ve used in several
examples already is just a squashed equality proof, as shown below.

```
let ( == ) #a (x y : a) = squash (equals x y)
```

In what follows, we’ll mostly use squashed equalities, except where we wish to emphasize the reflexivity proofs.

## Equality Reflection

What makes F* an *extensional* type theory (and unlike the
*intensional* type theories implemented by Coq, Lean, Agda, etc.) is a
feature known as equality reflection. Whereas intensional type
theories treat definitional and provable equalities separate, in F*
terms that are provably equal are also considered definitionally
equal. That is, if in a given context `x == y`

is derivable, the
`x`

is also definitionally equal to `y`

. This has some
wide-reaching consequences.

### Implicit conversions using provable equalities

Recall from the start of the chapter that `v:vec a ((fun x -> x) 0)`

is implicitly convertible to the type `vec a 0`

, since the two types
are related by congruence and reduction. However, as the examples
below show, if `a == b`

is derivable in the context, then
`v:a`

can be implicity converted to the type `b`

.

```
let pconv_vec_z (#a:Type) (#n:nat) (_:(n == 0)) (v:vec a n)
: vec a 0
= v
let pconv_vec_nm (#a:Type) (#n #m:nat) (_:(n == m)) (v:vec a n)
: vec a m
= v
let pconv_int (#a:Type) (_:(a == int)) (x:a)
: int
= x + 1
let pconv_ab (#a #b:Type) (_:(a == b)) (v:a)
: b
= v
```

We do not require a proof of `a == b`

to be literally bound in the
context. As the example below shows, the hypothesis `h`

is used in
conjunction with the control flow of the program to prove that in the
`then`

branch `aa : int`

and in the `else`

branch `bb : int`

.

```
let pconv_der (#a #b:Type)
(x y:int)
(h:((x > 0 ==> a == int) /\
(y > 0 ==> b == int) /\
(x > 0 \/ y > 0)))
(aa:a)
(bb:b)
: int
= if x > 0 then aa - 1 else bb + 1
```

In fact, with our understanding of equality proofs, we can better
explain how case analysis works in F*. In the code above, the
`then`

-branch is typechecked in a context including a hypothesis
`h_then: squash (equals (x > 0) true)`

, while the `else`

branch
includes the hypothesis `h_else: squash (equals (x > 0) false)`

. The
presence of these additional control-flow hypotheses, in conjunction
with whatever else is in the context (in particular hypothesis `h`

)
allows us to derive `(a == int)`

and `(b == int)`

in the
respective branches and convert the types of `aa`

and `bb`

accordingly.

### Undecidability and Weak Normalization

Implicit conversions with provable equalities are very convenient—we have relied on it without noticing in nearly all our examples so far, starting from the simplest examples about lists to vectors and Merkle trees, and some might say this is the one key feature which gives F* its programming-oriented flavor.

However, as the previous example hinted, it is, in general,
undecidable to determine if `a == b`

is derivable in a given
context. In practice, however, through the use of an SMT solver, F*
can often figure out when terms are provably equal and convert using
it. But, it cannot always do this. In such cases, the F* standard
library offers the following primitive (in FStar.Pervasives), which
allows the user to write `coerce_eq pf x`

, to explicitly coerce the
type of `x`

using the equality proof `pf`

.

```
let coerce_eq (#a #b:Type) (_:squash (a == b)) (x:a) : b = x
```

Another consequence of equality reflection is the loss of strong
normalization. Intensional type theories enjoy a nice property
ensuring that every term will reduce to a canonical normal form, no
matter the order of evaluation. F* does not have this property, since
some terms, under certain evaluation orders, can reduce
infinitely. However, metatheory developed for F* proves that closed
terms (terms without free variables) in the `Tot`

effect do not
reduce infinitely, and as a corollary, there are no closed proofs of
`False`

.

F* includes various heuristics to avoid getting stuck in an infinite loop when reducing open terms, but one can craft examples to make F*’s reduction macinery loop forever. As such, deciding if possibly open terms have the same normal form is also undecidable in F*.

## Functional Extensionality

Functional extensionality is a principle that asserts the provable equality of functions that are pointwise equal. That is, for functions \(f\) and \(g\), \(\forall x. f x == g x\) implies \(f == g\).

This principle is provable as a theorem in F*, but only for function literals, or, equivalently, \(\eta\)-expanded functions. That is, the following is a theorem in F*.

```
let eta (#a:Type) (#b: a -> Type) (f: (x:a -> b x)) = fun x -> f x
let funext_on_eta (#a : Type) (#b: a -> Type) (f g : (x:a -> b x))
(hyp : (x:a -> Lemma (f x == g x)))
: squash (eta f == eta g)
= _ by (norm [delta_only [`%eta]];
pointwise (fun _ ->
try_with
(fun _ -> mapply (quote hyp))
(fun _ -> trefl()));
trefl())
```

Note

Note, the proof of the theorem makes use of tactics, a topic we’ll
cover in a later chapter. You do not need to understand it in
detail, yet. The proof roughly says to descend into every sub-term
of the goal and try to rewrite it using the pointwise equality
hypothesis `hyp`

, and if it fails to just rewrite the sub-term to
itself.

Unfortunately, functional extensionality does not apply to all functions. That is, the following is not provable in F* nor is it sound to assume it as an axiom.

```
let funext =
#a:Type ->
#b:(a -> Type) ->
f:(x:a -> b x) ->
g:(x:a -> b x) ->
Lemma (requires (forall (x:a). f x == g x))
(ensures f == g)
```

The problem is illustrated by the following counterexample, which
allows deriving `False`

in a context where `funext`

is valid.

```
let f (x:nat) : int = 0
let g (x:nat) : int = if x = 0 then 1 else 0
let pos = x:nat{x > 0}
let full_funext_false (ax:funext)
: False
= ax #pos f g;
assert (f == g);
assert (f 0 == g 0);
false_elim()
```

The proof works by exploiting the interaction with refinement
subtyping. `f`

and `g`

are clearly not pointwise equal on the
entire domain of natural numbers, yet they are pointwise equal on the
positive natural numbers. However, from `ax #pos f g`

we gain that
`f == g`

, and in particular that `f 0 == g 0`

, which is false.

Note

The trouble arises in part because although `ax:funext`

proves
`squash (equals #(pos -> int) f g)`

, F*’s encoding of the
equality to the SMT solver (whose equality is untyped) treats the
equality as `squash (equals #(nat -> int) f g)`

, which leads to
the contradiction.

Further, \(\eta\)-equivalent functions in F* are not considered
provably equal. Otherwise, in combination with `funext_on_eta`

, an
\(\eta\)-equivalence principle leads to the same contradiction as
`funext_false`

, as shown below.

```
let eta_equiv =
#a:Type ->
#b:(a -> Type) ->
f:(x:a -> b x) ->
Lemma (f == eta f)
let eta_equiv_false (ax:eta_equiv)
: False
= funext_on_eta #pos f g (fun x -> ());
ax #pos f;
ax #pos g;
assert (f == g);
assert (f 0 == g 0);
false_elim()
```

The F* standard library module `FStar.FunctionalExtensionality`

provides more information and several utilities to work with
functional extensionality on \(\eta\)-expanded functions.

Thanks in particular to Aseem Rastogi and Dominique Unruh for many insights and discussions related to functional extensionality.

## Exercise

Leibniz equality `leq x y`

, relates two terms `x:a`

and `y:a`

if
for all predicates `p:a -> Type`

, `p a`

implies `p b`

. That is,
if no predicate can distinguish `x`

and `y`

, the they must be
equal.

Define Leibniz equality and prove that it is an equivalence relation.

Then prove that Leibniz equality and the equality predicate ```
equals x
y
```

defined above are isomorphic, in the sense that ```
leq x y ->
equals x y
```

and `equals x y -> leq x y`

.

**Hint**

The section on Leibniz equality here tells you how to do it in Agda.

```
let lbz_eq (#a:Type) (x y:a) = p:(a -> Type) -> p x -> p y
// lbz_eq is an equivalence relation
let lbz_eq_refl #a (x:a)
: lbz_eq x x
= fun p px -> px
let lbz_eq_trans #a (x y z:a) (pf1:lbz_eq x y) (pf2:lbz_eq y z)
: lbz_eq x z
= fun p px -> pf2 p (pf1 p px)
let lbz_eq_sym #a (x y:a) (pf:lbz_eq x y)
: lbz_eq y x
= fun p -> pf (fun (z:a) -> (p z -> p x)) (fun (px: p x) -> px)
// equals and lbz_eq are isomorphic
let equals_lbz_eq (#a:Type) (x y:a) (pf:equals x y)
: lbz_eq x y
= fun p px -> px
let lbz_eq_equals (#a:Type) (x y:a) (pf:lbz_eq x y)
: equals x y
= pf (fun (z:a) -> equals x z) Reflexivity
```

## Decidable equality and equality qualifiers

To end this chapter, we discuss a third kind of equality in F*, the
polymorphic *decidable equality* with the signature shown below taken
from the the F* module `Prims`

.

```
val ( = ) (#a:eqtype) (x y:a) : bool
```

On `eqtype`

, i.e., `a:Type{hasEq a}`

, decidable quality `(=)`

and provable equality coincide, as shown below.

```
let dec_equals (#a:eqtype) (x y:a) (_:squash (x = y))
: equals x y
= Reflexivity
let equals_dec (#a:eqtype) (x y:a) (_:equals x y)
: squash (x = y)
= ()
```

That is, for the class of `eqtype`

, `x = y`

returns a boolean
value that decides equality. Decidable equality and `eqtype`

were
first covered in an earlier chapter, where we
mentioned that several primitive types, like `int`

and `bool`

all
validate the `hasEq`

predicate and are, hence, instances of `eqtype`

.

When introducing a new inductive type definition, F* tries to
determine whether or not the type supports decidable equality based on
a structural equality of the representation of the values of that
type. If so, the type is considered an `eqtype`

and uses of the ```
(
= )
```

operator are compiled at runtime to structural comparison of
values provided by the target language chosen, e.g., OCaml, F#, or C.

The criterion used to determine whether or not the type supports equality decidable is the following.

Given an inductive type definition of \(T\) with parameters \(\overline{p}\) and indexes \(~\overline{q}\), for each constructor of \(D\) with arguments \(\overline{v:t_v}\),

Assume, or every type parameter \(t \in \overline{p}\), \(\mathsf{hasEq}~t\).

Assume, for recursive types, for all \(\overline{q}\), \(\mathsf{hasEq}~(T~\overline{p}~\overline{q})\).

For all arguments \(\overline{v:t_v}\), prove \(\mathsf{hasEq}~t_v\).

If the proof in step 3 suceeds for all constructors, then F* introduces an axiom \(\forall~\overline{p}~\overline{q}. (\forall t \in \overline{p}. \mathsf{hasEq}~t) \Rightarrow \mathsf{hasEq}~(T~\overline{p}~\overline{q})\).

If the check in step 3 fails for any constructor, F* reports an error which the user can address by adding one of two qualifiers to the type.

`noeq`

: This qualifier instructs F* to consider that the type does not support decidable equality, e.g., if one of the constructors contains a function, as show below.noeq type itree (a:Type) = | End : itree a | Node : hd:nat -> tl:(nat -> itree a) -> itree a

`unopteq`

: This qualifier instructs F* to determine whether a given instance of the type supports equality, even when some of its parameters are not themselves instances of`eqtype`

. This can be useful in situations such as the following:unopteq type t (f: Type -> Type) = | T : f bool -> t f let _ = assert (hasEq (t list)) [@@expect_failure] let _ = assert (hasEq (fun x -> x -> x))

This wiki page provides more information about equality qualifiers on inductive types.