Last week I talked about currying using Coq's Canonical Structures. This got me thinking about how to get something similar working in Agda. It turns out that the recently introduced REWRITE pragma is just what is needed to replicate this use case.
Let us start with a quick reminder of the problem at hand: the goal is to be able to write a map function working on lists and automatically currying its argument as much as possible. Why you ask? Well because we really don't want to have to define map_tuple, map_triple and so on with all the possible nestings imaginable.
The first thing to do is to introduce a record Curry describing the sort of domains we may curry. You may recognise the structure we used in the previous blog post: this record packs a domain (dom), a type constructor (cur) and a proof (prf) that for any codomain cod, one may turn an element of type cur cod into a function from dom to cod.
record Curry : Set₁ where field dom : Set cur : Set → Set prf : (cod : Set) (f : cur cod) → dom → cod
The next step is to define instances of Curry. The most obvious instance is probably the one doing nothing: for any domain A, we can define cur to be the function which associates A → cod to each codomain cod. The proof that one can turn A → cod into cur cod is then trivial.
curryDefault : (A : Set) → Curry curryDefault A = record { dom = A ; cur = λ cod → A → cod ; prf = λ cod → id }
We then explain how to combine two instances of Curry by taking, as domain, the product of their respective domains. The definitions of cur and prf become a bit more involved but should be understandable.
curryPair : (A B : Curry) → Curry curryPair A B = record { dom = dom A × dom B ; cur = λ cod → cur A (cur B cod) ; prf = λ cod f p → prf B cod (prf A (cur B cod) f (fst p)) (snd p) }
A REWRITE pragma has recently been introduced to allow the user to define a binary relation characterizing equations the typechecker should internalise. The primary goal is, as far as I know, to allow homotopy type theorists to have a bit of fun with an equality that looks like it computes. But there's no reason to leave it to them! Obviously, this is an unsafe feature and if you are not careful when picking your rewrite rules, you will get the typechecker into an infinite loop. It happened to me a couple of times whilst drafting this program.
The sole purpose of the Canonical relation we introduce is to guide the rewriting process. As such, we don't care about its implementation and can simply postulate it. We also introduce a Target precisely identifying the candidates for rewriting in order to avoid to send Agda into an infinite loop by reapplying the default rule over and over again.
postulate Canonical : (A B : Curry) → Set Target : (A : Set) → Curry
We can then define two rewrite rules based on our previous combinators. The order in which they are introduced matters and that is why we start with the one dealing with pairs so that we only ever use curryDefault when reaching a base type or a type variable.
postulate CanonicalProd : {A B : Set} → Canonical (Target (A × B)) (curryPair (Target A) (Target B)) CanonicalDefault : {A : Set} → Canonical (Target A) (curryDefault A)
Finally, we use the appropriate pragmas to declare Canonical as the relation characterizing the equations which should be internalised and tell Agda to use CanonicalProd and CanonicalDefault as rewrite rules.
{-# BUILTIN REWRITE Canonical #-} {-# REWRITE CanonicalProd #-} {-# REWRITE CanonicalDefault #-}
It is now time to define our generic mapping function. Just like last time, it is preferable to defined a flippedMap in order to fire the easy constraint List (Target A) first. We define flippedMap with a domain A which we now to be Curry and use its prf field to transport the function passed as an argument.
flippedMap : {A : Curry} {B : Set} (xs : List (dom A)) (f : cur A B) → List B flippedMap {A} xs f = map (prf A _ f) xs
We then introduce a slight variation on flippedMap which turns its argument into a Target. This is a great occasion to add a bit of syntactic sugar putting the arguments back in their right order. We choose to stick to applicative style combinators and use _⟨$⟩_.
flippedMap' : {A B : Set} (xs : List (dom (Target A))) (f : cur (Target A) B) → List B flippedMap' {A} = flippedMap {Target A} syntax flippedMap' xs f = f ⟨$⟩ xs
We can now have a look at a couple of small examples. It should be noted that our typechecking-time magic does not break anything: these examples still compute! Indeed normalising example₁ yields 3 ∷ 5 ∷ [] whilst doing the same for example₂ gives us 17 ∷ 30 ∷ [].
example₁ : List ℕ example₁ = _+_ ⟨$⟩ (1 , 2) ∷ (2 , 3) ∷ [] example₂ : List ℕ example₂ = (λ k l m n → k * l + m * n) ⟨$⟩ ((1 , 2) , (3 , 5)) ∷ ((2 , 3) , (4 , 6)) ∷ []