open import 1Lab.Reflection.Solver
open import 1Lab.Reflection
open import 1Lab.Prelude hiding (id ; _∘_)

open import Cat.Base

open import Data.Bool
open import Data.List

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 NbE (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 $C$ . What this means is that, while $f \circ g$ is some unknowable inhabitant of Hom, $f `\circ g$ represents an inhabitant of Hom which is known to be a composition of (the trees that represent) $f$ and $g$ . 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 $C$ . 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)

  nf : Expr A B → Hom A B
  nf e = eval e id

  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
    solve : (f g : Expr A B) → eval f id ≡ eval g id → embed f ≡ embed g
    solve f g p = sym (eval-sound f) ·· p ·· (eval-sound g)

    solve-filler : (f g : Expr A B) → (p : eval f id ≡ eval g id) → Square (eval-sound f) p (solve f g p) (eval-sound g)
    solve-filler f g p j i = ··-filler (sym (eval-sound f)) p (eval-sound g) j i

The cursed part🔗

module Reflection where

  pattern category-args xs =
    _ h0∷ _ h0∷ _ v∷ xs

  pattern “id” =
    def (quote Precategory.id) (category-args (_ h∷ []))

  pattern “∘” f g =
    def (quote Precategory._∘_) (category-args (_ h∷ _ h∷ _ h∷ f v∷ g v∷ []))

  mk-category-args : Term → List (Arg Term) → List (Arg Term)
  mk-category-args cat xs = unknown h∷ unknown h∷ cat v∷ xs

  “solve” : Term → Term → Term → Term
  “solve” cat lhs rhs = def (quote NbE.solve) (mk-category-args cat $ infer-hidden 2 $ lhs v∷ rhs v∷ def (quote refl) [] v∷ [])

  “nf” : Term → Term → Term
  “nf” cat e = def (quote NbE.nf) (mk-category-args cat $ infer-hidden 2 $ e v∷ [])

  build-expr : Term → Term
  build-expr “id” = con (quote NbE.`id) []
  build-expr (“∘” f g) = con (quote NbE._`∘_) (build-expr f v∷ build-expr g v∷ [] )
  build-expr f = con (quote NbE._↑) (f v∷ [])

  dont-reduce : List Name
  dont-reduce = quote Precategory.id ∷ quote Precategory._∘_ ∷ []

  cat-solver : Term → SimpleSolver
  cat-solver cat .SimpleSolver.dont-reduce = dont-reduce
  cat-solver cat .SimpleSolver.build-expr tm = returnTC $ build-expr tm
  cat-solver cat .SimpleSolver.invoke-solver = “solve” cat
  cat-solver cat .SimpleSolver.invoke-normalisier = “nf” cat

  repr-macro : Term → Term → Term → TC ⊤
  repr-macro cat f _ =
    mk-simple-repr (cat-solver cat) f

  simplify-macro : Term → Term → Term → TC ⊤
  simplify-macro cat f hole =
    mk-simple-normalise (cat-solver cat) f hole

  solve-macro : Term → Term → TC ⊤
  solve-macro cat hole =
    mk-simple-solver (cat-solver cat) hole

macro
  repr-cat! : Term → Term → Term → TC ⊤
  repr-cat! cat f = Reflection.repr-macro cat f

  simpl-cat! : Term → Term → Term → TC ⊤
  simpl-cat! cat f = Reflection.simplify-macro cat f

  cat! : Term → Term → TC ⊤
  cat! = Reflection.solve-macro

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 = cat! C