Introduction

The other day I was reading this blog post covering existential types in Rust (also known as impl Trait or opaque types). In that blog post, the author makes the following claim.

We’re going to have to take a slight diversion into type theory here because it motivates a result that is perhaps intuitive. The following proposition holds in intuitionistic logic: ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)), which means that according to the Curry–Howard Correspondence, it also holds when considering the proposition as a type.

In particular the ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) caught my eye. While I was working for Originate in San Francisco back in 2017 I used my 20% time project to study Benjamin C. Pierce’s excellent Software Foundations series which teaches how to structure and formally verify software using the Coq Proof Assistant (yes, it’s pronounced exactly how you think, 🙄). It completely changed the way I look at programming for the better but it’s not a skill that I get to practice regularly and as you get older you have to either use it or lose it. So I thought I’d try my hand at seeing if I remembered enough of Coq to be able to prove the above statement.

Trait Dispatch in Rust

To understand why we even care about the above proposition, it’s worth taking a moment to understand how impl Trait is used in Rust, if you’re not interested in Rust and just want to get to the Coq tutorial you should skip this section and jump head to #Coq

In Rust, to abstract over common functionality, we have Traits (interfaces in most other languages). Below is the simple ToString trait from the standard library.

trait ToString {
  fn to_string(&self) -> String;
}

If we want to write a function that accepts things that can be turned into strings we have a few different options depending on whether we want static or dynamic dispatch. To demonstrate the available options we’ll use a contrived toy function yell which turns the input into a string, convert it to all caps, and prints it to stdout.

Static Dispatch

fn yell<S: ToString>(stringable: S) {
  println!(stringable.to_string().to_uppercase())
}

In Rust, generics are monomorphised. The compiler will create a copy and unique name for each type the function is called with, meaning each method call on the trait points to one, and only one function so the call can be statically dispatched. For example

yell(42);
yell("According to all known laws of aviation ...");

This will result in the creation of two functions for each call

fn yell__i32(stringable: i32) {
  println!(stringable.to_string().to_uppercase())
}

fn yell__at_str(stringable: &str) {
  println!(stringable.to_string().to_uppercase())
}

transforming the call site also into their respective monomorphised functions

yell__i32(42);
yell__at_str("According to all known laws of aviation ...");

So when we call the trait method to_string() in each of those monomorphised functions, the rust compiler knows precisely which function call to make and doesn’t require chasing pointers (dynamic dispatch). It also means the stack layouts of calling those functions can differ but we’ll get into that in a moment when talking about trait objects and object safety (spoilers!).

Dynamic Dispatch

Another way to write our yell function is

fn yell(stringable: &dyn ToString) {
  println!(stringable.to_string().to_uppercase())
}

which from the name of this subsection and the use of the dyn keyword may have tipped you off to the fact it uses dynamic dispatch. If you’re familiar with how interfaces work in Golang then you already know what’s going on here.

In this case, rust doesn’t copy the yell method for each type it’s called with but instead &dyn ToString is often what’s known as a “fat pointer”. In that, it contains two pointers, one to the data, and one to the vtable for the methods of the trait.

It’s called “dynamic dispatch” because we don’t know which function we’re going to call until runtime when we follow the vtable pointer to find the particular to_string() method we’re going to call. Most of the time the overhead of this pointer chasing doesn’t matter and your application probably has performance bottlenecks elsewhere, but sometimes every pointer dereference counts.

Object Safety

Beyond questionably legitimate concerns about performance, when you stop to think about how the compiler would layout the stack to call a dynamically dispatched function you may realise a fairly large limitation on what kinds of traits can be dynamically dispatched. They have to be the same size! Or more precisely, the function inputs and outputs must all be of the same size!

Think about the following trait from the standard library

pub trait Clone {
    fn clone(&self) -> Self;
}

What is the amount of space we need to leave on the stack when calling clone()? Well, it returns Self, which is whatever the type that implements clone is, so i32, i64, or String all take up different amounts of space on the stack so it’s impossible for us to figure out how to layout the stack at compile time when we don’t know the size of the type until runtime! This is what’s known in rust as Object Safety. A trait that is not Object Safe contains methods with either its arguments or return values that do not have a constant size across all their possible implementations and therefore it is not safe to turn them into a Trait Object for dynamic dispatch.

In addition to trait methods that return Self, trait methods involving generic arguments or return values are also not “object safe” because the generic methods cannot be monomorphised behind a dynamic dispatch as it brushes up against the halting problem trying to figure how many entries of the monomorphised method are required in the vtable. If you tried to populate the vtable with every possible type in your application for each generic method it would grow enormous!

impl Trait

So now we understand that sometimes we cannot even use dynamic dispatch even if we don’t care about the overhead from pointer chasing. We’re stuck with going back to our static dispatch approach of monomorphising generic functions.

fn yell<S: ToString>(stringable: S) {
  println!(stringable.to_string().to_uppercase())
}

The additional syntactic and mental overhead of tracking those generic parameters isn’t so bad with a single generic parameter, but as the number of generic parameters grows, it can become unwieldy. For example, this function is taken from an application I’m working on that connects several different financial applications and follows the Ports and Adapters (also known as Clean or Hexagonal architecture) pattern of hiding concrete side effects behind simple interfaces and injecting them as needed.

pub fn process<E, B, S>(
    config: transformer::Config,
    expense_tracker: E,
    budget: B,
    state: S,
) -> Result<()>
where
  E: ExpenseTracker,
  B: Budget,
  S: State,
   { ... }

I don’t know about you, but I find that kind of hard to read, especially since we’re introducing generic parameters, E, B, and S and only at the end of the function definition are we giving them proper constraints. Luckily Rust has an answer! impl Trait. We can instead rewrite the above function as.

pub fn process(
    config: transformer::Config,
    expense_tracker: impl ExpenseTracker,
    budget: impl Budget,
    state: impl State,
) -> Result<()>

With this in mind you might be asking yourself why would you ever use dynamic dispatch over static. The main reason is when the dispatch, is well, dynamic! Such as when you have a collection of trait objects.

fn example() {
    let string = "hello";
    let integer = 3 as i32;

    let collection: Vec<&dyn ToString> = vec![&string, &integer];
}

Comparatively it is not possible to create a collection using impl Trait, nor is it possible to express this with generic constraints because the underlying opaque but concrete types are of different sizes.

fn first() -> impl ToString {
   "According to all known laws of aviation ..."
}

fn second() -> impl ToString {
    42
}

fn example() {
    vec![first(), second()];
    //      Error ^^^
    // mismatched types
    // expected opaque type `impl ToString` (opaque type at <src/main.rs:1:15>)
    // found opaque type `impl ToString` (opaque type at <src/main.rs:4:16>)
    // distinct uses of `impl Trait` result in different opaque types
}

But how to understand what impl Trait means? One way to understand it is it’s saying that there exists a type (unnamed) that implements the trait, the fact that it’s unnamed is why impl Trait is often referred to as opaque types, or existential types. We’re taking for granted that a type, some type, exists that satisfies this trait, but is it always safe to take the prior generic function and transform it into the existential form and vice versa? The introductory paragraph claims that it always is ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)), but let’s not take some guy’s word for it, we can do better! Let’s prove it!

Coq

The Coq toolchain is a bit tricky to set up locally, but luckily we don’t have to as there’s an excellent online IDE that we can use instead. I’d highly recommend following along this next section using that or another Coq IDE instead of just trying to understand it by reading. To translate our theorem into a form that Coq understands we can write

Theorem impl_trait_transform:
forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.

First, let’s take a second to understand our proposed theorem.

forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).

The first part, forall (Trait: Type -> Prop) (Result: Prop) is saying that what we want to prove should be true for every possible Trait, and any possible return value, we can’t rely on anything true about any particular trait, our results are universal.

The rest of our theorem is then broken into two halves separated by <->. This is known as material equivalence, or “if and only if”, which is to say the left is true, if and only if the right is true, and visa versa. Therefore to prove it, we have to prove that the left proposition implies the right proposition, and also prove that the right proposition implies the left proposition. So we started trying to prove one thing, and now we have to prove two things! This process is very common in formal verification. To prove your goal, you have to break it apart and prove sub-sections of it. To prove the A & B you have to prove A, and you have to prove B, to prove A | B you can take your pick of A or B whichever you think is easier to prove.

So now we have to prove

- (exists t, Trait(t)) -> Result) -> (forall t, (Trait(t) -> Result)
- (forall t, (Trait(t) -> Result) -> (exists t, Trait(t)) -> Result)

tactic split

A transformation in Coq is called a Tactic. The tactic for splitting our goal into two separate goals like this is unsurprisingly called split. To evaluate your proof up to where your cursor is press CMD+Enter. You should see the goals screen on the right update to reflect the new state of trying to prove our theorem.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.

Should give the output in the goals panel of

2 goals
  Trait : Type -> Prop
  Result : Prop
------------------------
(exists t : Type, Trait t) -> Result) -> forall t : Type, Trait t -> Result

subgoal 2 is:
(forall t : Type, Trait t -> Result) -> (exists t : Type, Trait t) -> Result

First Goal

To focus on one goal at a time we use - to denote each branch of the proof. We’ll use it to focus on the first part of our proof.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  -

Tactic intros

1 goal
Trait: Type -> Prop
Result: Prop
------------------------
((exists t : Type , Trait t)  -> Result) -> forall t : Type , Trait t -> Result

The way to understand trying to prove an implication like A -> B -> C, is that we get to assume, A, and B, when trying to prove C. So with the above goal, we get to assume we already have the two antecedent terms ((exists t : Type , Trait t) -> Result) and forall t : Type , Trait t. The tactic that lets us do this is called intro for one variable at a time, or intros if you want to “introduce” multiple at the same time. Naming these implied assumptions is hard so feel free to name them however you want or leave it blank and let Coq auto name them.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type trait.

Tactic apply

1 goal
Trait : Type -> Prop
Result : Prop
existsTrait : (exists t : Type, Trait t) -> Result
type : Type
trait : Trait type
------------------------
Result

Implications work the opposite way when they’re in our assumptions. Right now our goal is to make a Result, in our assumptions we have an implication existsTrait : (exists t : Type, Trait t) -> Result which can give us a Result if we’re able to prove its antecedent. So by “applying” our assumption, we can shift our goal to trying to prove the assumptions antecedent. Maybe it’s a dead end and we’ll have to backtrack, but Result doesn’t appear anywhere else in our assumptions so it’s worth a try. The tactic to do this is unsurprisingly called apply.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type trait.
    apply existsTrait.

Tactic exists

1 goal
Trait : Type -> Prop
Result : Prop
existsTrait : (exists t : Type, Trait t) -> Result
type : Type
trait : Trait type
------------------------
exists t : Type, Trait t

Now our goal is exists t : Type, Trait t, much like forall and intros, there exists a tactic for dealing with existentially quantified variables, called exists. Although unlike intros, which give us new assumptions, exists demands that we prove that a term exists. It is in some sense the opposite of forall/intros, it consumes a term rather than giving us one. Luckily, after examining our assumptions, we can see that our previous intros gave us an assumption of kind type : Type that matches the kind demanded by the “exists”. So we can get rid of it with exists.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type trait.
    apply existsTrait.
    exists type.

Tactic assumption

1 goal
Trait : Type -> Prop
Result : Prop
exists : Trait(exists t : Type, Trait t) -> Result
type : Type
trait : Trait type
------------------------
Trait type

Now you may notice that our goal exactly matches one of our assumptions. So we can use the tactic assumption to finish this branch of the proof! One down and one to go!

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type trait.
    apply existsTrait.
    exists type.
    assumption.
  -

Second Goal

1 goal
Trait : Type -> Prop
Result : Prop
------------------------
(forall t : Type, Trait t -> Result) -> (exists t : Type, Trait t) -> Result

Now we’re proving that the material equivalence holds in the other direction, and just like the first branch we use intros to move the left-hand side of the implications into our assumptions.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type concreteTrait.
    apply existsTrait.
    exists type.
    assumption.
  - intros anyTrait existsTrait.

Tactic destruct

1 goal
Trait : Type -> Prop
Result : Prop
anyTrait : forall t : Type , Trait t  -> Result
existsTrait : exists t : Type, Trait t
------------------------
Result

At this point you might be tempted to try and apply anyTrait just like we did for our first goal, trying to switch the goal from result to forall t : Type , Trait t, however, this doesn’t work with Coq complaining that Unable to find an instance for the variable t. This is because t is still universally quantified right now, whereas in our first goal t was existentially quantified. So we’re going to need to find ourselves a t: Type before we can shift our goal.

We also have the existsTrait: exists t : Type, Trait t assumption. Luckily, when we have a term like this, we can ask Coq if this expression implies anything else that is not currently in our assumptions. We do this with the inversion or destruct tactics. Coq will auto-name the new assumptions but we can also give them meaningful names with as.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type concreteTrait.
    apply existsTrait.
    exists type.
    assumption.
  - intros anyTrait existsTrait.
    destruct existsTrait as (t, trait).

Tactic apply _ with _

Trait : Type -> Prop
Result : Prop
anyTrait : forall t : Type, Trait t -> Result
t : Type
trait : Trait type
------------------------
Result

Coq has broken apart existsTrait into its two assumptions. So now we have an assumption of kind Type! We can now solve the problem we had before about applying anyTrait.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type concreteTrait.
    apply existsTrait.
    exists type.
    assumption.
  - intros anyTrait existsTrait.
    destruct existsTrait as (t, trait).
    apply anyTrait with t.

Tactic assumption

Trait : Type -> Prop
Result : Prop
anyTrait : forall t : Type, Trait t -> Result
t : Type
trait : Trait t
------------------------
Trait t

Now just like before, our goal matches one of our assumptions, so we can finish up this branch with assumption.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type concreteTrait.
    apply existsTrait.
    exists type.
    assumption.
  - intros anyTrait existsTrait.
    destruct existsTrait as (t, trait).
    apply anyTrait with t.
    assumption.

QED

No more goals.

Now that we’ve proved all of our goals, we get to do the best thing about formal verification. The sweet three-letter acronym. QED.

Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop),
  ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)).
Proof.
  split.
  - intros existsTrait type concreteTrait.
    apply existsTrait.
    exists type.
    assumption.
  - intros anyTrait existsTrait.
    destruct existsTrait as (t, trait).
    apply anyTrait with t.
    assumption.
Qed.

Conclusion

And there you go, we’ve formally verified that our transformation from generic arguments with trait bounds into existential impl Trait arguments is always valid. Of course, Rust would not have implemented the feature had it not made sense, but I think it’s gratifying to be able to prove such a cryptic statement like ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q))

Hopefully, this has given you a bit of a taste of how to reason when it comes to formally verifying programs which is such an interesting but alien style of programming. It feels like playing with Legos where the bricks are parts of your program. You know the final shape you want, you just have to keep exploring how they combine to get there. There is a deep connection between theorem proving and metaprogramming but that’s a story for another time.

If you’d like to explore more formal verification I’d highly recommend checking out Software Foundations or Edwin Brady’s Type-Driven Development with Idris.