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.