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


#1

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.


#2

I imagine the answer is similar to the answers for typeclasses from Haskell, which is that typeclasses are propositions about types. You can read about typeclasses and Curry-Howard-Lambek on the Haskell Wiki: https://wiki.haskell.org/Curry-Howard-Lambek_correspondence