Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
syntax description
a == b A type asserting that a is equal to b
refl(~x) A proof that x == x
sym(~e) Given e : a == b, proves b == a
cong(~f, ~e) For any f, given e : a == b, proves f(a) == f(b)
t :: rewrite x in P(x) with e Given e : a == b and t : P(a), proves P(b)

Here, a == b is a type specifying that a is equal to b. It is not a proof, it is merely "a question". To prove it, you must construct a term x of type a == b. The only way to do it directly is with refl(~t), which proves that a term is equal to itself. That is, for any t, proves t == t. So, for example:

main : 1 == 1

That means refl(~1) is a proof that 1 == 1. As you can see, we can have values inside types: that's perfectly normal in Formality.

Equalities are useful to, among other things, restrict the domain of a function. For example:

mul_small : {x : Word, y : Word, ~e : (x + y) == 10} -> Word
  x * y

main : Word
  mul_small(3, 7, ~refl(~10))

This "small multiplication" function can only be called if its first two arguments add to 10. This is enforced by the presence of the third argument, e, which is erased (due to the ~). In other words, differently than a classic "assert", this restriction is checked statically and has no runtime costs. As an exercise, try changing the arguments of mul_small on the program above and see what happens.

Equality can be used and manipuled with 3 primitives. The sym primitive just flips the sides of an equality. The cong primitive just appends a function to both sides. The rewrite primitive allows us to substitute equal terms in arbitrary types. It consists of a term to be casted (t), a variable (x), a template (P(x)) and an equality proof (e), and performs the following operation:

// Step 1: assert that `e`'s type is an equality.
// Step 2: replace the template's variable by the left-side of the equality.
// Step 3: assert that the type of `a` matches the type above.
// Step 4: replace the template's variable by the right-side of the equality.
// Step 5: cast `t` to the type above.

For example, suppose that we had a function that received a x : Word and a y : Word that added to 9, and we wanted to call small_mul with them. We could try this:

main : {x : Word, y : Word, ~e : (x + y) == 9} -> Word
  mul_small(x + y, 1, ~e)

But we'd have the following error:

Type mismatch.
- Found type... x + y == 9
- Instead of... (x + y) + 1 == 10

That's because e is a proof that x + y == 9, not that (x + y) + 1 == 10. But since 9 is smaller than 10, we should be able to call mul_small on x + y. With rewrite, we can do that as follows:

main : {x : Word, y : Word, ~xy_is_9 : (x + y) == 9} -> Word
// The term to be casted.
  let t = refl(~10)

// The rewrite equality.
  let e = sym(~xy_is_9)

//  Step 1: asserted `e`'s type is an equality (`9 == x + y`).
//  Step 2: replacing `k` on the template by `9`, we get `(9 + 1) == 10`.
//  Step 3: asserted that `t : 10 == 10` matches the type above (by reduction).
//  Step 4: replacing `k` on the template by `x + y`, we get `((x + y) + 1) == 10`.
//  Step 5: `t` is casted to the type above.
  let t = t :: rewrite k in (k + 1) == 10 with e

//Since `T : ((x + y) + 1) == 10`, we can call `mul_small` with `(x + y)` and `1`.
  mul_small(x + y, 1, ~t)

In short, it allowed us to replace 9 by x + y on t : (9 + 1) == 10 by exploiting the e : 9 == x + y argument. Note that, here, t is an equality too, but that's not mandatory; it could have been any type that had a 9 inside it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.