open import 1Lab.Reflection open import 1Lab.Prelude hiding (id ; _β_) open import Cat.Base open import Data.Bool module Cat.Solver where
Solver for Categoriesπ
This module is split pretty cleanly into two halves: the first half implements an algorithm for reducing, in a systematic way, problems involving associativity and identity of composition in a precategory. The latter half, significantly more cursed, uses this infrastructure to automatically solve equality goals of this form.
With a precategory in hand, we by defining a language of composition.
module _ (Cat : Precategory o h) where open Precategory Cat
data Expr : Ob β Ob β Type (o β h) where `id : Expr A A _`β_ : Expr B C β Expr A B β Expr A C _β : Hom A B β Expr A B infixr 40 _`β_ infix 50 _β
A term of type Expr represents, in a symbolic way, a composite of morphisms in our category . What this means is that, while is some unknowable inhabitant of Hom, represents an inhabitant of Hom which is known to be a composition of (the trees that represent) and . We can now define βtwoβ ways of computing the morphism that an Expr represents. The first is a straightforward embedding:
embed : Expr A B β Hom A B embed `id = id embed (f β) = f embed (f `β g) = embed f β embed g
The second computation is a bit less obvious. If youβre a programmer, it should be familiar under the name βcontinuation passing style.β Categorically, it can be seen as embedding into the presheaf category of . In either case, the difference is that instead of computing a single morphism, we compute a transformation of hom-spaces:
eval : Expr B C β Hom A B β Hom A C eval `id f = f eval (f β) g = f β g eval (f `β g) h = eval f (eval g h) eval-sound-k : (e : Expr B C) (f : Hom A B) β eval e id β f β‘ eval e f eval-sound-k `id f = idl _ eval-sound-k (x β) f = ap (_β f) (idr x) eval-sound-k (f `β g) h = eval f (eval g id) β h β‘β¨ ap (_β h) (sym (eval-sound-k f (eval g id))) β©β‘ (eval f id β eval g id) β h β‘β¨ sym (assoc _ _ _) β©β‘ eval f id β eval g id β h β‘β¨ ap (_ β_) (eval-sound-k g h) β©β‘ eval f id β eval g h β‘β¨ eval-sound-k f _ β©β‘ eval (f `β g) h β
Working this out in a back-of-the-envelope calculation, one sees that eval f id
should compute the same morphism as embed f
. Indeed, thatβs the case! Since embed is the βintended semantics,β and eval is an βoptimised evaluator,β we call this result soundness. We can prove it by induction on the expression. Here are the two straightforward cases, and why they work:
eval-sound : (e : Expr A B) β eval e id β‘ embed e eval-sound `id = refl -- eval `id computes away eval-sound (x β) = idr _ -- must show f = f β id
Now comes the complicated part. First, weβll factor out proving that nested eval is the same as eval of a composition to a helper lemma. Then comes the actual inductive argument: We apply our lemma (still to be defined!), then we can apply the induction hypothesis, getting us to our goal.
eval-sound (f `β g) = eval f (eval g id) β‘β¨ sym (eval-sound-k f (eval g id)) β©β‘ eval f id β eval g id β‘β¨ apβ _β_ (eval-sound f) (eval-sound g) β©β‘ embed (f `β g) β
We now have a general theorem for solving associativity and identity problems! If two expressions compute the same transformation of hom-sets, then they represent the same morphism.
abstract associate : (f g : Expr A B) β eval f id β‘ eval g id β embed f β‘ embed g associate f g p = sym (eval-sound f) Β·Β· p Β·Β· eval-sound g
The cursed partπ
Now we hook up associate to an Agda macro. Like all metaprogramming, itβs not pretty, but Iβve written comments around it to hopefully explain things a bit.
record CategoryNames : Type where field is-β : Name β Bool is-id : Name β Bool build-matcher : Name β Maybe Name β Name β Bool build-matcher n nothing x = n name=? x build-matcher n (just m) x = or (n name=? x) (m name=? x) find-generic-names : Name β Name β Term β TC CategoryNames find-generic-names star id mon = do β-altName β normalise (def star (unknown hβ· unknown hβ· mon vβ· [])) Ξ΅-altName β normalise (def id (unknown hβ· unknown hβ· mon vβ· [])) -- typeError (termErr β-altName β· termErr Ξ΅-altName β· []) returnTC record { is-β = build-matcher star (getName β-altName) ; is-id = build-matcher id (getName Ξ΅-altName) } find-category-names : Term β TC CategoryNames find-category-names = find-generic-names (quote Precategory._β_) (quote Precategory.id)
The trick above was stolen from the Agda standard library monoid solver. Given the term representing the category, we evaluate the projections (thatβs the -altNames
) in case they compute away to something else. This lets us not miss solutions when working with a concrete category, that might have names other than Precategory._β_ and Precategory.id.
Now we can turn to building an Expr (well, a Term representing an Expr: a representation of a representation of an arrow!) given a Term. We do this with mutual recursion, to make stuff even more complicated.
private module _ (names : CategoryNames) where open CategoryNames names build-expr : Term β Term build-β : List (Arg Term) β Term ``id : Term -- Constant representation of `id ``id = con (quote `id) [] build-expr (def x as) with is-β x | is-id x ... | false | false = con (quote _β) (def x as vβ· []) ... | false | true = ``id ... | true | q = build-β as
If weβre looking at a def (an applied defined function) or a con (an applied co/inductive constructor). If weβre looking at some random old term, then we lift it (with _β). If itβs the identity map, then we use our constant repr. of id, otherwise weβre looking at a composition.
build-expr (con x as) with is-β x | is-id x ... | false | false = con (quote _β) (def x as vβ· []) ... | false | true = ``id ... | true | q = build-β as build-expr x = con (quote _β) (x vβ· []) build-β (x vβ· y vβ· []) = con (quote _`β_) (build-expr x vβ· build-expr y vβ· []) build-β (_ β· xs) = build-β xs build-β _ = unknown get-boundary : Term β TC (Maybe (Term Γ Term)) get-boundary tm@(def (quote PathP) (_ hβ· T vβ· x vβ· y vβ· [])) = do unify tm (def (quote _β‘_) (x vβ· y vβ· [])) returnTC (just (x , y)) get-boundary _ = returnTC nothing
Then you essentially slap all of that together into a little macro.
solve-generic : (Term β TC CategoryNames) β (Term β Term) β Term β Term β TC β€ solve-generic find mkcat category hole = do goal β inferType hole >>= normalise names β find category just (lhs , rhs) β get-boundary goal where nothing β typeError (strErr "Can't solve: " β· termErr goal β· []) let rep = build-expr names unify hole (def (quote associate) (mkcat category vβ· rep lhs vβ· rep rhs vβ· def (quote refl) [] vβ· [])) macro solve : Term β Term β TC β€ solve = solve-generic find-category-names (Ξ» x β x)
Demoπ
As a quick demonstration (and sanity check/future proofing/integration testing/what have you):
module _ (C : Precategory o h) where private module C = Precategory C variable A B : C.Ob a b c d : C.Hom A B test : a C.β (b C.β (c C.β C.id) C.β C.id C.β (d C.β C.id)) β‘ a C.β b C.β c C.β d test = solve C