Equality

Equality is a subtle issue that pervades the design of all dependent type theories, and F* is no exception. In this first chapter, we briefly touch upon two different kinds of equality in F*, providing some basic information sufficient for the simplest usages. In a subsequent chapter, we’ll cover equality in much greater depth.

Decidable equality and eqtype

We’ve implicitly used the equality operator = already (e.g., when defining factorial). This is the boolean equality operator. Given two terms e₁ : t and e₂ : t, so long as t supports a notion of decidable equality, (e₁ = e₂) : bool.

To see why not all types support decidably equality, consider t to be a function type, like int -> int. To decide if two functions f₁, f₂ : int -> int are equal, we’d have to apply them to all the infinitely many integers and compare their results—clearly, this is not decidable.

The type eqtype is the type of types that support decidably equality. That is, given e₁ : t and e₂ : t, it is only permissible to compare e₁ = e₂ if t : eqtype.

For any type definition, F* automatically computes whether or not that type is an eqtype. We’ll explain later exactly how F* decides whether or not a type is an eqtype. Roughly, for F* has built-in knowledge that various primitive types like integers and booleans support decidable equality. When defining a new type, F* checks that all values of the new type are composed structurally of terms that support decidable equality. In particular, if an e : t may contain a sub-term that is a function, then t cannot be an eqtype.

As such, the type of the decidable equality operator is

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

That is, x = y is well-typed only when x : a and y : a and a : eqtype.

Note

We see here a bit of F* syntax for defining infix operators. Rather than only using the val or let notation with alphanumeric identifiers, the notation ( = ) introduces an infix operator defined with non-alphanumeric symbols. You can read more about this here.

Propositional equality

F* offers another notion of equality, propositional equality, written ==. For any type t, given terms e₁, e₂ : t, the proposition e₁ == e₂ asserts the (possibly undecidable) equality of e₁ and e₂. The type of the propositional equality operator is shown below:

val ( == ) (#a:Type) (x:a) (y:a) : prop

Unlike decidable equality (=), propositional equality is defined for all types. The result type of (==) is prop, the type of propositions. We’ll learn more about that in the next chapter.