# What do traits correspond to under the Curry-Howard correspondence?

Do traits have any counterpart under the Curry-Howard correspondence? (Asking for a friend.)

Does this have anything to do with the fabled Martin-Löf type theories? Am I going to need to type umlauts to use Rust?

For readers who aren't familiar with the Curry-Howard correspondence, here's a quick-and-dirty intro:

There's similarity between types as usually discussed in type theory and propositions as usually discussed in formal logic, which is called the Curry-Howard correspondence. Perhaps the germ of the idea is noticing that this function:

``````fn p1<B>() -> B { ... }
``````

can't possibly be implemented. There's no way to produce a value of any type, given that there are no constraints on B at all. However, this one can be implemented:

``````fn p2<A, B>(a: A, f: fn(A) -> B) -> B { ... }
``````

Given an A and a function that produces a B from an A, you can produce a B.

If you draw an analogy between a type like `fn(A) -> B` and the proposition "A implies B", you can look at `p2`'s signature as a way of saying, "If A, and A implies B, then B."

You can carry this analogy pretty far: a type `(A, B)` represents "A and B": if you have a value of that tuple type, then you can certainly produce a value of type A and a value of type B. (Assume everything is `Copy` for now.)

Or, a type like `enum S<A, B> { Sa(A), Sb(B) }` represents "A or B". For example, if you can implement a function like this:

``````fn p3<X, Y, Z>(s: S<X, Y>,
fx: fn(X) -> Z,
fy: fn(Y) -> Z) -> Z { ...}
``````

then that's like proving the proposition, "If X or Y, and X implies Z and Y implies Z, then Z."

The final step is to notice that the code that implements these functions has the same shape as a proof of the proposition that corresponds to the type. For example, we can implement `p3` easily:

``````    match s {
S::Sa(x) => fx(x),
S::Sb(y) => fy(y)
}
``````

This is exactly the proof, "Either X or Y is true: If X is true, that implies Z. If Y is true, that implies Z. Hence, Z."

Non-generic types like `char` correspond to axioms or given facts: you don't need any arguments at all to produce a `char`, and you don't need any proof to produce a fact you were given.

1 Like