Who says Agda doesn't have tactics? 4-ish mechanisms for generating proofs in Agda

GeneratingCode.agda

-- A demonstration of Agda's mechanisms for generating proofs:
-- * 1. fromMaybe
-- * 2a. macros
-- * 2b. type-aware macros
-- * 2c. stuck macros
--
-- Tested using Agda-2.6.1.1 and agda-stdlib-1.4

module GeneratingCode where


-- First, let's give a concrete example of the problem we are trying to solve.
--
-- Here is a typical definition of the simply-typed lambda-calculus with
-- deBruijn variables.

open import Agda.Builtin.List
  using (List; []; _∷_)
open import Data.List.Relation.Unary.Any
  using (here; there)
open import Data.Nat
  using (ℕ; zero; suc)
open import Relation.Binary.PropositionalEquality
  renaming (setoid to ≡-setoid)

data Tp : Set where
  unit : Tp
  _↝_  : Tp → Tp → Tp
infixr 6 _↝_

open import Data.List.Membership.Setoid (≡-setoid Tp)
  using (_∈_)

data STLC (Γ : List Tp) : Tp → Set where
  var  : ∀ {τ}
       → τ ∈ Γ
       → STLC Γ τ
  unit : STLC Γ unit
  lam  : ∀ {τ₁ τ₂}
       → STLC (τ₁ ∷ Γ) τ₂
       → STLC Γ (τ₁ ↝ τ₂)
  _$_  : ∀ {τ₁ τ₂}
       → STLC Γ (τ₁ ↝ τ₂)
       → STLC Γ τ₁
       → STLC Γ τ₂
infixr 0 _$_


-- And here are a few example lambda-calculus expressions. Note how using the
-- var constructor is very verbose, because it needs a proof of (τ ∈ Γ). In the
-- rest of this file, we will explore ways to make this less verbose by
-- generating those proofs.

const-unit : ∀ {Γ a}
           → STLC Γ (a ↝ unit)
const-unit = lam unit

id : ∀ {Γ a}
   → STLC Γ (a ↝ a)
id = lam (var (here refl))

three : ∀ {Γ a}
      → STLC Γ ((a ↝ a) ↝ a ↝ a)
three {a = a} = lam (lam
              ( let f : STLC _ (a ↝ a)
                    f = var (there (here refl))
                    x : STLC _ a
                    x = var (here refl)
                in f $ f $ f $ x
              ))


----------------------------
-- Mechanism 1: fromMaybe --
----------------------------

-- Agda doesn't have tactics, but it has something similar: we can write our
-- own program which searches for a proof at compile time. If the search
-- succeeds with a "just", we insert the proof into the program, and if it
-- fails with a "nothing"... something else happens, and compilation fails with
-- a type error.
--
-- We will use this recipe to shorten
--
--   var (there (there (here refl)))
--
-- to
--
--   varAt 2
--
-- using a very straightforward "search" which simply generates the requested
-- number of 'there' constructors, while double-checking that this does not
-- index past the end of Γ.

open import Category.Monad
  using (RawMonad)
open import Data.Bool.Base
  using (T)
open import Data.Maybe
  using (nothing; just; fromMaybe; is-just; to-witness-T)
  renaming (Maybe to level-polymorphic-Maybe)

Maybe : Set → Set
Maybe = level-polymorphic-Maybe

-- So, our goal is to generate a proof of "τ ∈ Γ", for some "τ". First, we need
-- to write a function which computes that "τ".

lkp : ℕ → List Tp → Maybe Tp
lkp _       []      = nothing
lkp zero    (x ∷ _) = just x
lkp (suc i) (_ ∷ Γ) = lkp i Γ

-- "lkp i Γ" can fail if "i" points beyond the length of "Γ", and that's fine,
-- because we're allowed to abort our search with a "nothing".

-- Next, let's construct our value of type "τ ∈ Γ" for that specific "τ". If
-- "lkp i Γ" failed, we simply fail with "nothing" again; but at the
-- type-level, the situation is a bit more complicated because we still need to
-- say what the "τ" of our "Maybe (τ ∈ Γ)" output should be in that case. Here,
-- I use "fromMaybe" to make the output type be "Maybe (unit ∈ Γ)" in that
-- case. It could be anything, it doesn't matter, because we're not going to be
-- providing a proof of "unit ∈ Γ" in that case. We just need something which
-- is a valid type.

lkpElem : (i : ℕ) → (Γ : List Tp)
        → Maybe (fromMaybe unit (lkp i Γ) ∈ Γ)
lkpElem _       []      = nothing
lkpElem zero    (x ∷ _) = just (here refl)
lkpElem (suc i) (_ ∷ Γ) with lkpElem i Γ
... | nothing  = nothing
... | just x∈Γ = just (there x∈Γ)

-- Finally, we can write our "varAt" helper function. We want a call to look
-- like "varAt 2", so obviously it takes a "ℕ" as one of its input... but
-- here's the trick: it also takes a second implicit argument after that! Agda
-- fills in all the implicit inputs whenever they are unambiguous, and in this
-- case, we were careful to ask for a value of a type which will be unambiguous
-- if our proof search succeeds. If "lkpElem i Γ" returns a "just", then
-- "is-just (just ...)" becomes "True", and "T True" becomes the unit type "⊤",
-- which is easy for Agda to fill-in automatically.

varAt : ∀ {Γ}
      → (i : ℕ)
      → {prf : T (is-just (lkpElem i Γ))}
      → STLC Γ (fromMaybe unit (lkp i Γ))
varAt {Γ} i {prf} = var (to-witness-T (lkpElem i Γ) prf)

-- Here are our example lambda-calculus expressions again, using "varAt"
-- successfully.

id1 : ∀ {a}
    → STLC [] (a ↝ a)
id1 = lam (varAt 0)

three1 : ∀ {Γ a}
       → STLC Γ ((a ↝ a) ↝ a ↝ a)
three1 {a = a} = lam (lam
               ( let f : STLC _ (a ↝ a)
                     f = varAt 1
                     x : STLC _ a
                     x = varAt 0
                 in f $ f $ f $ x
               ))

-- If our search is unsuccessful, then the "T (is-just nothing)" becomes "⊥",
-- which will appear as an unsolved meta.
--
--   -- Unsolved meta
--   const-unit1 : ∀ {a}
--               → STLC [] (a ↝ unit)
--   const-unit1 = lam (varAt 42)
--
-- Under some circumstances, a different type error appears before the unsolved
-- meta. For example, "STLC Γ (fromMaybe unit nothing)" becomes "STLC Γ unit",
-- but for "id′" we need an "STLC Γ a", and that error takes precedence.
--
--   -- unit != a of type Tp
--   id1′ : ∀ {a}
--        → STLC [] (a ↝ a)
--   id1′ = lam (varAt 1)
--
-- In addition to our search returning a "just" or returning "nothing", there
-- is a third possibility: the search can get stuck if one of its inputs is an
-- unknown type variable. In that case, the type error will include some
-- internal details about the implementation of "fromMaybe", along with the
-- stuck expression, in this case "lkp 0 Γ".
--
--   -- Data.Maybe.maybe (λ x → x) unit (lkp 0 Γ) != a of type Tp
--   id1′′ : ∀ {Γ a}
--         → STLC Γ (a ↝ a)
--   id1′′ = lam (varAt 1)


--------------------------
-- Mechanism 2a: macros --
--------------------------

-- We again want
--
--   varMacro 2
--
-- to expand to
--
--   var (there (there (here refl)))
--
-- This time we don't generate the value "var (there (there (here refl)))",
-- instead we generate the AST of the expression "var (there (there (here refl)))".
-- The difference is that "var (here refl)" and "var (there (here refl))" have
-- different types (they point to different entries in "Γ"), while their ASTs
-- both have type "Term".

open import Data.Unit
  using (⊤; tt)
open import Reflection
  renaming (arg to mk-arg; var to mk-var)
  hiding (_>>=_; _>>_; return)
open import Reflection.TypeChecking.Monad.Categorical
  using ()
  renaming (monad to TC-monad)

-- "Term" values are very verbose, so let's first write a few helpers.

arg : Term → Arg Term
arg = mk-arg (arg-info visible relevant)

var-term : Term → Term
var-term x = con (quote var) (arg x ∷ [])

there-term : Term → Term
there-term x = con (quote there) (arg x ∷ [])

here-term : Term → Term
here-term x = con (quote here) (arg x ∷ [])

refl-term : Term
refl-term = con (quote refl) []

elem-term : ℕ → Term
elem-term zero    = here-term refl-term
elem-term (suc n) = there-term (elem-term n)

-- We are now ready to write our macro. It does not _return_ a value of type
-- "Term", instead it receives a hole which it can fill.

macro
  varMacro : ℕ → Term → TC ⊤
  varMacro n hole = do
    _ ← unify hole (var-term (elem-term n))
    return tt
    where open RawMonad TC-monad

-- Here are our example lambda-calculus expressions once again, using
-- "varMacro" successfully.

id2a : ∀ {Γ a}
     → STLC Γ (a ↝ a)
id2a = lam (varMacro 0)

three2a : ∀ {Γ a}
        → STLC Γ ((a ↝ a) ↝ a ↝ a)
three2a {a = a} = lam (lam
                ( let f : STLC _ (a ↝ a)
                      f = varMacro 1
                      x : STLC _ a
                      x = varMacro 0
                  in f $ f $ f $ x
                ))

-- What happens when we use "varMacro" unsuccessfully? The same thing as if we
-- had written the incorrect proof ourselves.
--
--   -- _ ∷ _ != []
--   id2a′ : ∀ {a}
--         → STLC [] (a ↝ a)
--   id2a′ = lam (var (there (there (here refl))))
--
--   -- _ ∷ _ != []
--   id2a′′ : ∀ {a}
--          → STLC [] (a ↝ a)
--   id2a′′ = lam (varMacro 2)


-------------------------------------
-- Mechanism 2b: type-aware macros --
-------------------------------------

-- So far, we did not have to search very hard for a proof because the ℕ
-- argument told us exactly which proof to generate. This time, let's write a
-- version which does not take an argument:
--
--   varAuto
--
-- will expand to
--
--   var (there (there (here refl)))
--
-- if the first entry in "Γ" which has the appropriate type is at position 2.
-- To do this, the macro needs to know what the appropriate type is. It can
-- obtain this information by asking Agda to infer the type of the hole it was
-- given.

open import Agda.Builtin.Reflection
  using (primQNameEquality)
open import Data.Bool
  using (Bool; false; true; _∧_)
open import Data.List
  using (and; map; zipWith)
open import Data.Maybe.Categorical
  using ()
  renaming (monad to Maybe-monad)
open import Data.Product
  using (_×_; _,_)
open import Function.Base
  using (case_of_)

-- "Term" values being verbose, we also need some helpers for examining them.

un-arg : {A : Set} → Arg A → A
un-arg (mk-arg _ a) = a

get-args : Term → Maybe (List Term)
get-args (mk-var _ args) = just (map un-arg args)
get-args (con    _ args) = just (map un-arg args)
get-args (def    _ args) = just (map un-arg args)
-- For simplicity, I ignore the other constructors, since they do not come up
-- in our examples.
get-args _ = nothing

-- Next, we need a function which checks if two "Term" values are equal. There
-- is a library which uses some of the mechanisms described in this file to
-- automatically derive an Eq instance for custom datatypes, similar to
-- "deriving Eq" in Haskell:
--
--   https://github.com/effectfully/Generic
--
-- Unfortunately, "Term" is a bit too magical for that library, so we have to
-- define equality by hand.

name-eq? : Name → Name → Bool
name-eq? = primQNameEquality

nat-eq? : ℕ → ℕ → Bool
nat-eq? zero    zero    = true
nat-eq? (suc x) (suc y) = nat-eq? x y
nat-eq? _       _       = false

-- Hush the termination checker, who doesn't see that "zipWith" only calls
-- "arg-eq?" on smaller "Term" values.
{-# TERMINATING #-}
mutual
  term-eq? : Term → Term → Bool
  term-eq? (mk-var x1 args1)
           (mk-var x2 args2) = nat-eq? x1 x2
                             ∧ and (zipWith arg-eq? args1 args2)
  term-eq? (con    x1 args1)
           (con    x2 args2) = primQNameEquality x1 x2
                             ∧ and (zipWith arg-eq? args1 args2)
  term-eq? (def    x1 args1)
           (def    x2 args2) = primQNameEquality x1 x2
                             ∧ and (zipWith arg-eq? args1 args2)
  term-eq? _ _ = false

  arg-eq? : Arg Term → Arg Term → Bool
  arg-eq? (mk-arg _ a1) (mk-arg _ a2) = term-eq? a1 a2

-- Next, let's go through "Γ", looking for an entry which is "term-eq? to "τ".

cons-name : Name
cons-name = quote _∷_

find-index : Term → Term → Maybe ℕ
find-index needle (con conName (_ ∷ _ ∷ mk-arg _ hd ∷ mk-arg _ tl ∷ [])) = do
  true ← return (name-eq? conName cons-name)
    where _ → nothing
  case term-eq? needle hd of λ
    { true → do
        return zero
    ; false → do
        i ← find-index needle tl
        return (suc i)
    }
  where open RawMonad {M = Maybe} Maybe-monad
find-index _ _ = nothing

-- We are now ready to write our macro. Given its intended use, I assume that
-- the hole's inferred type has the shape "STLC Γ τ" for some concrete choice of
-- "Γ" and "τ". In the case of "f = varAuto" in "three2b", the inferred type is
-- "STLC (a ∷ a ↝ a ∷ Γ) (a ↝ a)". We find the position of "a ↝ a" in that
-- list, and conclude that "i" must be "1".

macro
  varAuto : Term → TC ⊤
  varAuto hole = do
    stlcGammaTau ← inferType hole
    just (Γ ∷ τ ∷ []) ← return (get-args stlcGammaTau)
      where _ → typeError ( strErr "varAuto: expected STLC Γ τ, got"
                          ∷ termErr stlcGammaTau
                          ∷ []
                          )
    just i ← return (find-index τ Γ)
      where _ → typeError ( strErr "varAuto: type"
                          ∷ termErr τ
                          ∷ strErr "not found in context"
                          ∷ termErr Γ
                          ∷ []
                          )
    _ ← unify hole (var-term (elem-term i))
    return tt
    where open RawMonad TC-monad

-- Here are our example lambda-calculus expressions one more time, using
-- "varAuto" successfully.

id2b : ∀ {Γ a}
     → STLC Γ (a ↝ a)
id2b = lam varAuto

three2b : ∀ {Γ a}
        → STLC Γ ((a ↝ a) ↝ a ↝ a)
three2b {Γ} {a} = lam (lam
                ( let f : STLC (a ∷ a ↝ a ∷ Γ) (a ↝ a)
                      f = varAuto
                  in f $ f $ f $ varAuto
                ))

-- When the search aborts with "nothing", in this case because we are looking
-- for "unit" in the context "a ∷ []", we get our custom type error.
--
--   -- varAuto: type unit not found in context (a ∷ [])
--   const-unit2b : ∀ {a}
--                → STLC [] (a ↝ unit)
--   const-unit2b = lam varAuto
--
-- Due to the way in which we defined "find-index", we also abort the search if
-- we encounter a type variable, so this search for "unit" in the context
-- "a ∷ Γ" fails in the exact same way.
--
--   -- varAuto: type unit not found in context (a ∷ Γ)
--   const-unit2b′ : ∀ {Γ a}
--                 → STLC Γ (a ↝ unit)
--   const-unit2b′ = lam varAuto
--
-- For the same reason, we also abort the search if we encounter a
-- meta-variable, that is, a type which has not yet been solved. This is why
-- the type signature of "f" in "three2b" spells out the context instead of
-- letting Agda infer it from how "f" is used. If we do let Agda infer the
-- context, then it just so happens that Agda expands our macro before it
-- solves that meta-variable, and so the search aborts prematurely.
--
--   -- varAuto: type a ↝ a not found in context _387
--   three2b′ : ∀ {Γ a}
--            → STLC Γ ((a ↝ a) ↝ a ↝ a)
--   three2b′ {a = a} = lam (lam
--                    ( let f : STLC _ (a ↝ a)
--                          f = varAuto
--                      in f $ f $ f $ varAuto
--                    ))
--
-- For this reason, type-aware macros can be a bit brittle: a seemingly-innocent
-- refactoring can cause the code to no longer type-check, because it affects
-- the order in which Agda solves the meta-variables.
-- See [my talk on the topic](https://www.youtube.com/watch?v=nUvKoG_V_U0) for
-- details.


--------------------------------
-- Mechanism 2c: stuck macros --
--------------------------------

-- If you have watched the talk above, you might now wonder if Agda supports
-- stuck macros. Agda does not force your macros to do the right thing like I
-- advocate in the talk, but at least it allows them to do the right thing,
-- which is to suspend the macro until all the meta-variables it depends on
-- have been solved.

mutual
  force : Term → TC ⊤
  force (mk-var _ args) = force-list args
  force (con    _ args) = force-list args
  force (def    _ args) = force-list args
  force (meta   x _   ) = blockOnMeta x
  force _ = return tt
    where open RawMonad TC-monad

  force-list : List (Arg Term) → TC ⊤
  force-list [] = do
    return tt
    where open RawMonad TC-monad
  force-list (mk-arg _ x ∷ xs) = do
    force x
    force-list xs
    where open RawMonad TC-monad

macro
  varStuck : Term → TC ⊤
  varStuck hole = do
    stlcGammaTau ← inferType hole

    -- In the talk, I advocate suspending the macro whenever it attempts to
    -- pattern-match on a "Type"; which, in a dependently-typed language, is the
    -- same thing as a "Term". For simplicity, here I am doing this eagerly
    -- rather than lazily, by looking for metas anywhere inside the inferred
    -- type before I do any pattern-matching on any part of it. This way, I can
    -- reuse the definitions of "find-index" and friends from the previous
    -- section.
    force stlcGammaTau

    just (Γ ∷ τ ∷ []) ← return (get-args stlcGammaTau)
      where _ → typeError ( strErr "varStuck: expected STLC Γ τ, got"
                          ∷ termErr stlcGammaTau
                          ∷ []
                          )
    just i ← return (find-index τ Γ)
      where _ → typeError ( strErr "varStuck: type"
                          ∷ termErr τ
                          ∷ strErr "not found in context"
                          ∷ termErr Γ
                          ∷ []
                          )
    _ ← unify hole (var-term (elem-term i))
    return tt
    where open RawMonad TC-monad

-- Here are our example lambda-calculus expressions once last time, using
-- "varStuck" successfully.

id2c : ∀ {Γ a}
     → STLC Γ (a ↝ a)
id2c = lam varStuck

three2c : ∀ {Γ a}
        → STLC Γ ((a ↝ a) ↝ a ↝ a)
three2c {a = a} = lam (lam
                ( let f : STLC _ (a ↝ a)
                      f = varStuck
                  in f $ f $ f $ varStuck
                ))

-- A slightly trickier case in which we let Agda infer that the second
-- "varStuck" must have type "a ↝ a".
one2c : ∀ {Γ a}
      → STLC Γ ((a ↝ a) ↝ a ↝ a)
one2c {a = a} = lam (lam
              ( let x : STLC _ a
                    x = varStuck
                in varStuck $ x
              ))

-- The "f : STLC _ (a ↝ a)" failure case from before is now successful, but we
-- there is another failure case to consider. Since our macro is suspended until
-- Agda solves all the relevant meta-variables, we now have to worry about the
-- case in which Agda is not able to solve all the meta-variables we have
-- forced. In that case, our macro will never run, and we get a longer error
-- message awkwardly explaining the problem.
--
--   -- Failed to solve the following constraints:
--   --   unquote (λ hole → <the entire desugared definition of varStuck>)
--   -- Unsolved metas
--   three2c′ : ∀ {Γ a}
--            → STLC Γ ((a ↝ a) ↝ a ↝ a)
--   three2c′ = lam (lam
--            ( varStuck $ varStuck
--            ))

Bonus:

3. proof via canonical forms