I have been meaning to have a look at Canonical Structures at some point since Beta Ziliani told me about 4 years ago that all the Ltac magic I was doing to reify expressions could be handed over to the inference engine. Yesterday I was finally given a simple opportunity to play with them. Here's the result.
Whilst reading a completely unrelated blog post about unit testing in Coq, I stumbled upon a series of almost identical functions named List.map_pair, List.map_triple and List.map_quad. I thought to myself that, surely, it should be possible in a language with type-level computations to do away with the sort of monstrosities one can sometime find in Haskell libraries. Introducing a Universe closed under products can indeed allow the definition of generic (un)currying functions. However we are still left with the burden of reifying the domain of the function we want to curry. Annoying.
That is when Canonical Structures come to the rescue: they are a way to give hints to the unification algorithm when it faces a problem of the shape project ?x ~ term where project is a projection out of a record, ?x is a unification variable and term is... a term. Because this unification step can lead to new ones, we effectively have a way to encode a prolog-like proof search. And we are going to use it to generate the right sort of currying.
This whole development is following quite closely the really good introduction Canonical Structures for the working Coq user. We start by defining a module which contains first and foremost a Record class indexed by a domain Dom and a type constructor Curr such that Curr a is a curried version of the function space Dom -> a as witnessed by the Fun stored in the record.
Module Currying. Record class (Dom : Type) (Curr : Type -> Type) := Class { Fun : forall cod, Curr cod -> (Dom -> cod) }.
We then define a structure called type packing together a Dom, a Curr and the class Dom Curr evidence that they are related.
Structure type := Pack { dom : Type ; curr : Type -> Type ; class_of : class dom curr }.
Now, remember that canonical structures are used to give hints to the unification algorithm when facing project ?x ~ term problems. Having this type structure will allow us to generate dom ?x ~ something unification problems which means that the unification algorithm will be able to infer from the shape of the domain what its curried version is. In order to trigger these unification problems, we are defining a special version of map on list:
Definition flippedmap (Curry : type) : forall cod, list (dom Curry) -> curr Curry cod -> list cod. refine (let 'Pack _ _ (Class fc) := Curry in fun cod xs f => List.map _ xs) ; apply fc, f. Defined.
Multiple things are going on here. First we define the function interactively because we have some nasty type-level dependencies and this post is not about dependent matching in Coq. Second we implemented flippedmap rather than map because taking the function first would create a unification problem curr ?x ~ [some function type] which is obviously harder to resolve than list (dom ?x) ~ list ([some type]).
We can introduce a notation in order to recover the usual arguments order. We then close our Currying module and bring the notation into scope.
Module theory. Notation "f <$> xs" := (flippedmap xs f) (at level 70). End theory. End Currying. Import Currying.theory.
Now that our interface has been defined, it is time to populate it with canonical instances. The first one simply states that given two domains we know how to curry, we can explain how to curry their product. The nesting fun cod => Currying.curr c1 (Currying.curr c2 cod) is chosen so that arguments are kept in the right order.
Definition pair_curry (c1 c2 : Currying.type) : forall cod, Currying.curr c1 (Currying.curr c2 cod) -> (Currying.dom c1 * Currying.dom c2) -> cod. intros cod f (a, b). apply c2 ; [| exact b]. apply c1 ; [| exact a]. exact f. Defined. Canonical Structure CurryingPair (c1 : Currying.type) (c2 : Currying.type) : Currying.type := Currying.Pack (Currying.dom c1 * Currying.dom c2) (fun cod => Currying.curr c1 (Currying.curr c2 cod)) (Currying.Class (pair_curry c1 c2)).
That's all well and good except that we don't know yet how to deal with base types. Should we add an instance for each one of them? And what about type variables? It turns out that we can rely on the fact that these hints are tried in the order they are declared in and introduce a defaulting instance which does not do anything as witnessed by its Fun component which is simply the identity.
Canonical Structure failsafe (a : Type) : Currying.type := Currying.Pack a (fun cod => a -> cod) (Currying.Class (fun _ f => f)).
Thanks to the canonical structures, we can effortlessly recover the functions List.map_pair, List.map_triple and List.map_quad I mentioned earlier:
Definition map_pair {A B C} (f : A -> B -> C) (l : list (A * B)) : list C := f <$> l. Definition map_triple {A B C D} (f : A -> B -> C -> D) (l : list (A * B * C)) : list D := f <$> l. Definition map_quad {A B C D E} (f : A -> B -> C -> D -> E) (l : list (A * B * C * D)) : list E := f <$> l.
But we can also deal with arbitrary nesting patterns:
Definition map_nestedpairs {A B C D E} (f : A -> B -> C -> D -> E) (l : list ((A * B) * (C * D))) : list E := f <$> l.