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 CC. What this means is that, while f∘gf \circ g is some unknowable inhabitant of Hom, fβ€˜βˆ˜gf `\circ g represents an inhabitant of Hom which is known to be a composition of (the trees that represent) ff and gg. 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 CC. 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