Equality Types

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.

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.

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

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

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

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())

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.

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.

Exercise file

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}\),

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

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

3. 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.

1. 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
   

2. 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.