In the last blog post I described how to create a proof that a type belongs to a group of types. In this post, I'll describe how to constrain a method such that we can extend a representative type set in a manner that enforces a uniqueness property of each subsequent type set. Then I'll describe how to constrain that group so that a single type appears only once.
As in the last post I'm going to make several assumptions about your level of Scala knowledge. I'm going to assume that you understand implicit parameters and that you're familiar with the type class pattern as found in Scala. I'm going to assume you're aware of the Aux type pattern or at least heard of type refinements (this one's new.) I'll 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.)
The Proof
First, let us define what we mean by a unique set and the single operation we define on it to extend the collection of types such that the uniqueness property of each type within the type set is preserved
This says that given out TSet, we can add a type to the collection as long as an implicit Merge can be found. It also provides the description of the Merge type class; one that contains an abstract type member. The result of the merge member function depends on the abstract type Out, more specifically known as a path dependent type, since the answer will change for each supplied type parameter.
(As before I've included a type alias for Tuple2 which I hope will make reading the code easier to digest.)
Merging is an action with an invariant which must be proven to be true (or at least defined to be true, semantics.) As a first step towards building the full proof we can consider an attempt to add a single type to a type set containing only two types:
There are three cases which must be handled: the added type is equivalent to the first type in the set, the added type is equivalent to the second type in the set and finally the added type does not exist in the set. Unlike the OneOf cases, we don't need to worry that the two types in the set are equivalent and safely nest them within the direct companion object definition. The Out parameter is defined as the logical result, if it already exists we don't include it twice.
(A point of clarify: we're using the Aux type pattern here because it's good practice for reasons outside the scope of this post. If you don't understand why we would want it, have a gander at the first video in the video section which discusses it in some depth.)
The second stage of building out this proof is generalizing it to an arbitrary sized type set of types:
Added to the logical paths are two more branches: the condition where the set contains only a single element and it is the same as the added type and the recursive search into the type set which inserts the type if and only if it does not already exist.
Here the Out parameter is being used as a means of passing type level information between different iterations of the type computation much in the same way as an accumulator in a recursive function. If the type being added ultimately does not exist then at some stage an implicit search will yield a result with that type appended. If it does exist then the original type will be recursively rebuilt.
Finally, to complete the proof and come full circle, we must handle when the merged parameter is itself a type set:
Two more branches have been added, this time taking priority over all other added branches. The first branch handles the case where the type set being merged contains only a single item. In this case we reuse the logic which we had previously constructed up until this point. It is more or less unpacking the type within the type constructor.
The second logical branch added exists in a seemingly bizarro world of recursion and Aux pattern type madness. To break this down, the first implicit parameter is repacking everything but the first type parameter back into a TSet so that a new search can be made. The second implicit parameter uses the first type in the TSet with the results generated from the first implicit parameter (this is why it's expressed in an Aux type) to produce the final result.
(If you're still confused as to what's happening with the Aux type watch the video or skim to the middle and read here.)
Conclusion
This builds upon the previous blog post to give a more challenging example of type level proofs/inductive logic. It covered not only all the cases of the previous proof but delved into using the Aux type pattern popularized in the Shapeless library to deconstruct a nested type within an already recursively structured type level computation. At each stage the invariant that a single type should not appear more than once in the final result was obeyed.
Do note, the point of this post was educational. The code here lacks several niceties, namely how to preclude non-unique types in the definition of TSet. If you're interested in seeing more examples of type level computations take a gander at the aforementioned Shapeless or my own Autolifts project.