Using the compiler to prove the correctness of a program is what static types are all about. In this blog post we'll take that concept one step further and actually use the type system to construct a type level constraint. This constraint, namely that a type is one of several types, will cause the compiler to fail not at runtime but at compile time, thus forming a proof that a system is undeniably working as intended.
To read this post I will assume that you understand implicit parameters and that you're familiar with the type class pattern as found in Scala. Furthermore, I will also assume you can read and understand a recursively defined function. Finally, I expect you to be aware of implicit resolution order semantics (but not have memorized nearly half of it.) After that, it's all about taking these concepts and applying them at the type level. In fact, I'd say it's a bit like learning a language within a language.
The Proof
The first thing we want to do is set up a type class which represents that a type belongs to a set of types:
This says given a collection of types embodied by the Items type and a test type denoted by Obj, find an implicit of the trait OneOf which proves that Obj is contained within Items. Or, at least, it will eventually say that. Right now it just looks to you like a useless object containing a type member and a function that discards the implicit parameter passed to it.
(Included is a type alias for Tuple2 which I hope will make things easier to understand as I build out the logic. I generally don't suggest using symbols for types (or classes, ahem, Scalaz) unless you actually want to confuse your colleagues. In that case, may I introduce you to the IOCCC.)
The first stage of defining the proof is to consider a pair of types as the basis set (hence, Tuple2.) We can place the implicit search within the companion object so that if either the left or the right type, denoted below as L or R, matches Obj, the implicit is always available in scope:
The companion object is further separated into two cases such that the implicit definition in the object body is searched first, followed by the trait. This is to avoid an implicit ambiguity brought on by having both L and R be equivalent types, i.e. Int and Int.
Next we can relax the condition on the types such that they play well with inheritance. That is, we want to be able to say that a type Dog is within a pair Animal | Plant.
To generalize to more than two types, we can use the previously defined conditionals (namely left or right equivalence in a set of two) as the basis for a recursive definition. In doing so we'll form an inductive proof:
The final step is the recurrence relationship. It splits the search space down the structure of the group of types so that if the left hand type, L, is ever the same as Obj, then a solution is found. Only at the last segment, when there are but two types to be searched do we need check the right most type. The additional implicit parameter is discarded, we only need to know that it existed to be able to say that it exists for the entire group.
To see this in action, take the following bit of code:
together with the previously given definition for OneOf and play around with the test cases. The first three should compile without issue. The final will not.
Conclusion
This basic construction is the template strategy for many type level inductive proofs. Form a basis set for a solution (in our case the solution space was binary) and build a search using a recursive structure as a stepping mechanism. It is no different than a recursive function on a list. To wit, the list is a list of types, not values.
Do note, the intent of this post was to educate and not provide a production ready solution. This implementation will not support the search for higher kinded types either has the search parameter Obj type nor as a member of the group of types Items. If you're interested in seeing more examples of these types of things, checkout out the implementation details of Miles Sabin's Shapeless or my own AutoLifts projects.