Skip to content

A slow-paced introduction to reflection in Agda. ---Tactics!

Notifications You must be signed in to change notification settings

alhassy/gentle-intro-to-reflection

Folders and files

NameName
Last commit message
Last commit date

Latest commit

ย 

History

14 Commits
ย 
ย 
ย 
ย 
ย 
ย 
ย 
ย 

Repository files navigation

A slow-paced introduction to reflection in Agda. โ€”Tactics!

**Abstract**

One proof for two different theorems!

Let's learn how we can do that in Agda.

This tutorial is the result of mostly experimenting with the documentation on Agda's reflection mechanism, which essentially only exposes the reflection interface and provides a few tiny examples. The goal of this tutorial is to contain a diverse variety of examples, along with occasional exercises for the reader.

Examples include:

  • String manipulation of built-in identifier names. ๐Ÿ“
  • Handy dandy combinators for AST formation: ๐“‹๐“‡๐’ถ, ฮป๐“‹_โ†ฆ_, โ€ฆ. ๐Ÿ› 
  • Numerous examples of quotation of terms and types. ๐ŸŽฏ
  • Wholesale derivation of singleton types for an example datatype, along with derivable proofs ๐Ÿ’› ๐ŸŽต
  • Automating proofs that are only refl with pattern matching ๐Ÿ„
  • Discussion of C-style macros in Agda ๐ŸŒต
  • Abstracting proofs patterns without syntactic overhead using macros ๐Ÿ’ช ๐ŸŽผ
  • Remarks on what I could not do, possibly since it cannot be done ๐Ÿ˜ญ

Everything here works with Agda version 2.6.0. This document is a literate Agda file written using the (poorly coded) org-agda framework.

A pure .agda file can be found here.

Table of Contents

  1. Imports
  2. Introduction
  3. NAME โ”€Type of known identifiers
  4. Arg โ”€Type of arguments
  5. Term โ”€Type of terms
    1. Example: Simple Types
    2. Example: Simple Terms
    3. A relationship between quote and quoteTerm
    4. Example: Lambda Terms
  6. Metaprogramming with The Typechecking Monad TC
  7. Unquoting โ”€Making new functions & types
  8. Sidequest: Avoid tedious refl proofs
  9. Macros โ”€Abstracting Proof Patterns
    1. C-style macros
    2. Tedious Repetitive Proofs No More!
  10. Our First Real Proof Tactic
  11. Heuristic for Writing a Macro
  12. What about somewhere deep within a subexpression?

Imports

First, some necessary imports:

module gentle-intro-to-reflection where

import Level as Level
open import Reflection hiding (name; Type)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Unary using (Decidable)
open import Relation.Nullary

open import Data.Unit
open import Data.Nat as Nat hiding (_โŠ“_)
open import Data.Bool
open import Data.Product
open import Data.List as List
open import Data.Char as Char
open import Data.String as String

Introduction

Reflection is the ability to convert program code into an abstract syntax, a data structure that can be manipulated like any other.

Consider, for example, the tedium of writing a decidable equality for an enumerated type. Besides being tedious and error-prone, the inexpressibility of what should be a mechanically-derivable concept obscures the corresponding general principle underlying it, thus foregoing any machine assistance in ensuring any correctness or safety-ness guarantees. Reflection allows a more economical and disciplined approach.

It is the aim of this tutorial to show how to get started with reflection in Agda. To the best of my knowledge there is no up to date tutorial on this matter.

There are three main types in Agda's reflection mechanism: Name, Arg, Term. We will learn about them with the aid of this following simple enumerated typed, as well as other standard types.

data RGB : Set where
  Red Green Blue : RGB

NAME โ”€Type of known identifiers

Name is the type of quoting identifiers, Agda names. Elements of this type can be formed and pattern matched using the quote keyword.

a-name : Name
a-name = quote โ„•

isNat : Name โ†’ Bool
isNat (quote โ„•) = true
isNat _         = false

-- bad : Set โ†’ Name
-- bad s = quote s  {- s is not known -}
  • NAME comes equipped with equality, ordering, and a show function.
  • Quote will not work on function arguments; the identifier must be known.

Let's show names:

_ : showName (quote _โ‰ก_) โ‰ก "Agda.Builtin.Equality._โ‰ก_"
_ = refl

_ : showName (quote Red) โ‰ก "gentle-intro-to-reflection.RGB.Red"
_ = refl

It would be nice to have Red be shown as just โ€œRGB.Redโ€.

First, let's introduce some โ€˜programmingโ€™ helpers to treat Agda strings as if they where Haskell strings, and likewise to treat predicates as decidables.

{- Like โ€œ$โ€ but for strings. -}
_โŸจ๐’ฎโŸฉ_ : (List Char โ†’ List Char) โ†’ String โ†’ String
f โŸจ๐’ฎโŸฉ s = fromList (f (toList s))

{- This should be in the standard library; I could not locate it. -}
toDec : โˆ€ {โ„“} {A : Set โ„“} โ†’ (p : A โ†’ Bool) โ†’ Decidable {โ„“} {A} (ฮป a โ†’ p a โ‰ก true)
toDec p x with p x
toDec p x | false = no ฮป ()
toDec p x | true = yes refl

We can now easily obtain the module's name, then drop it from the data constructor's name.

module-name : String
module-name = takeWhile (toDec (ฮป c โ†’ not (c Char.== '.'))) โŸจ๐’ฎโŸฉ showName (quote Red)

_ : module-name โ‰ก "gentle-intro-to-reflection"
_ = refl

strName : Name โ†’ String
strName n = drop (1 + String.length module-name) โŸจ๐’ฎโŸฉ showName n
{- The โ€œ1 +โ€ is for the โ€œ.โ€ seperator in qualified names. -}

_ : strName (quote Red) โ‰ก "RGB.Red"
_ = refl

NAME essentially provides us with the internal representation of a known name, for which we can query to obtain its definition or type. Later we will show how to get the type constructors of โ„• from its name.

Arg โ”€Type of arguments

Arguments in Agda may be hidden or computationally irrelevant. This information is captured by the Arg type.

{- Arguments can be (visible), {hidden}, or โฆƒinstanceโฆ„ -}
data Visibility : Set where
  visible hidden instanceโ€ฒ : Visibility

{-Arguments can be relevant or irrelevant: -}
data Relevance : Set where
  relevant irrelevant : Relevance

{- Visibility and relevance characterise the behaviour of an argument: -}
data ArgInfo : Set where
  arg-info : (v : Visibility) (r : Relevance) โ†’ ArgInfo

data Arg (A : Set) : Set where
  arg : (i : ArgInfo) (x : A) โ†’ Arg A

For example, let's create some helpers that make arguments of any given type A:

{- ๐“‹isible ๐“‡elevant ๐’ถrgument -}
๐“‹๐“‡๐’ถ : {A : Set} โ†’ A โ†’ Arg A
๐“‹๐“‡๐’ถ = arg (arg-info visible relevant)

{- ๐’ฝidden ๐“‡elevant ๐’ถrgument -}
๐’ฝ๐“‡๐’ถ : {A : Set} โ†’ A โ†’ Arg A
๐’ฝ๐“‡๐’ถ = arg (arg-info hidden relevant)

Below are the variable counterparts, for the Term datatype, which will be discussed shortly.

  • Variables are De Bruijn indexed and may be applied to a list of arguments.

  • The index n refers to the argument that is n locations away from โ€˜hereโ€™.

    {- ๐“‹isible ๐“‡elevant ๐“‹ariable -} ๐“‹๐“‡๐“‹ : (debruijn : โ„•) (args : List (Arg Term)) โ†’ Arg Term ๐“‹๐“‡๐“‹ n args = arg (arg-info visible relevant) (var n args)

    {- ๐’ฝidden ๐“‡elevant ๐“‹ariable -} ๐’ฝ๐“‡๐“‹ : (debruijn : โ„•) (args : List (Arg Term)) โ†’ Arg Term ๐’ฝ๐“‡๐“‹ n args = arg (arg-info hidden relevant) (var n args)

Term โ”€Type of terms

We use the quoteTerm keyword to turn a well-typed fragment of code โ€”concrete syntaxโ€” into a value of the Term datatype โ€”the abstract syntax. Here's the definition of Term:

data Term where

  {- A variable has a De Bruijn index and may be applied to arguments. -}
  var       : (x : โ„•)  (args : List (Arg Term)) โ†’ Term

  {- Constructors and definitions may be applied to a list of arguments. -}
  con       : (c : Name) (args : List (Arg Term)) โ†’ Term
  def       : (f : Name) (args : List (Arg Term)) โ†’ Term

  {- ฮป-abstractions bind one varaible; โ€œtโ€ is the string name of the variable
along with the body of the lambda.
  -}
  lam       : (v : Visibility) (t : Abs Term) โ†’ Term  {- Abs A  โ‰…  String ร— A -}
  pat-lam   : (cs : List Clause) (args : List (Arg Term)) โ†’ Term

  {- Telescopes, or function types; ฮป-abstraction for types. -}
  pi        : (a : Arg Type) (b : Abs Type) โ†’ Term

  {- โ€œSet nโ€ or some term that denotes a type -}
  agda-sort : (s : Sort) โ†’ Term

  {- Metavariables; introduced via quoteTerm -}
  meta      : (x : Meta) โ†’ List (Arg Term) โ†’ Term

  {- Literal  โ‰…  โ„• | Word64 | Float | Char | String | Name | Meta -}
  lit       : (l : Literal) โ†’ Term

  {- Items not representable by this AST; e.g., a hole. -}
  unknown   : Term {- Treated as '_' when unquoting. -}

data Sort where
  set     : (t : Term) โ†’ Sort {- A Set of a given (possibly neutral) level. -}
  lit     : (n : Nat) โ†’ Sort  {- A Set of a given concrete level. -}
  unknown : Sort

data Clause where
  clause        : (ps : List (Arg Pattern)) (t : Term) โ†’ Clause
  absurd-clause : (ps : List (Arg Pattern)) โ†’ Clause

Example: Simple Types

Here are three examples of โ€œdefโ€ined names, the first two do not take an argument. The last takes a visible and relevant argument, ๐“‹๐“‡๐’ถ, that is a literal natural.

import Data.Vec as V
import Data.Fin as F

_ : quoteTerm โ„• โ‰ก def (quote โ„•) []
_ = refl

_ : quoteTerm V.Vec โ‰ก def (quote V.Vec) []
_ = refl

_ : quoteTerm (F.Fin 3) โ‰ก def (quote F.Fin) (๐“‹๐“‡๐’ถ (lit (nat 3)) โˆท [])
_ = refl

Example: Simple Terms

Elementary numeric quotations:

_ : quoteTerm 1 โ‰ก lit (nat 1)
_ = refl

_ :    quoteTerm (suc zero)
 โ‰ก con (quote suc) (arg (arg-info visible relevant) (quoteTerm zero) โˆท [])
_ = refl

{- Using our helper ๐“‹๐“‡๐’ถ -}
_ : quoteTerm (suc zero) โ‰ก con (quote suc) (๐“‹๐“‡๐’ถ (quoteTerm zero) โˆท [])
_ = refl

The first example below demonstrates that true is a type โ€œconโ€structor that takes no arguments, whence the []. The second example shows that _โ‰ก_ is a defined name, not currently applied to any arguments. The final example has propositional equality applied to two arguments.

_ : quoteTerm true โ‰ก con (quote true) []
_ = refl

_ : quoteTerm _โ‰ก_ โ‰ก def (quote _โ‰ก_) []
_ = refl

_ :   quoteTerm ("b" โ‰ก "a")
โ‰ก def (quote _โ‰ก_)
  ( ๐’ฝ๐“‡๐’ถ (def (quote Level.zero) [])
  โˆท ๐’ฝ๐“‡๐’ถ (def (quote String) [])
  โˆท ๐“‹๐“‡๐’ถ (lit (string "b"))
  โˆท ๐“‹๐“‡๐’ถ (lit (string "a")) โˆท [])
_ = refl

Notice that a propositional equality actually has four arguments โ”€a level, a type, and two argumentsโ”€ where the former two happen to be inferrable from the latter. Here is a more polymorphic example:

_ : โˆ€ {level : Level.Level}{Type : Set level} (x y : Type)
โ†’   quoteTerm (x โ‰ก y)
   โ‰ก def (quote _โ‰ก_)
       (๐’ฝ๐“‡๐“‹ 3 [] โˆท ๐’ฝ๐“‡๐“‹ 2 [] โˆท ๐“‹๐“‡๐“‹ 1 [] โˆท ๐“‹๐“‡๐“‹ 0 [] โˆท [])

_ = ฮป x y โ†’ refl

Remember that a De Bruijn index n refers to the lambda variable that is n+1 lambdas away from its use site. For example, ๐“‹๐“‡๐“‹ 1 means starting at the โ‹ฏ โ‰ก โ‹ฏ, go 1+1 lambdas away to get the variable x.

We will demonstrate an example of a section, say โ‰ก_ "b", below when discussing lambda abstractions.

A relationship between quote and quoteTerm

Known names ๐’ป in a quoted term are denoted by a quote ๐’ป in the AST representation.

For example โ”€I will use this ๐’ปโ„ด๐“ƒ๐“‰ for my postulated itemsโ”€

postulate ๐’œ โ„ฌ : Set
postulate ๐’ป : ๐’œ โ†’ โ„ฌ
_ : quoteTerm ๐’ป โ‰ก def (quote ๐’ป) []
_ = refl

In contrast, names that vary are denoted by a var constructor in the AST representation.

module _ {A B : Set} {f : A โ†’ B} where
  _ : quoteTerm f โ‰ก var 0 []
  _ = refl

Example: Lambda Terms

First we show how reduction with lambdas works then we show how lambda functions are represented as Term values.

quoteTerm typechecks and normalises its argument before yielding a Term value.

_ : quoteTerm ((ฮป x โ†’ x) "nice") โ‰ก lit (string "nice")
_ = refl

Eta-reduction happens, f โ‰ˆ ฮป x โ†’ f x.

id : {A : Set} โ†’ A โ†’ A
id x = x

_ :   quoteTerm (ฮป (x : โ„•) โ†’ id x)
โ‰ก def (quote id) (๐’ฝ๐“‡๐’ถ (def (quote โ„•) []) โˆท [])
_ = refl

No delta-reduction happens; function definitions are not elaborated.

_ :   quoteTerm (id "a")
โ‰ก def (quote id)
    (๐’ฝ๐“‡๐’ถ (def (quote String) []) โˆท  ๐“‹๐“‡๐’ถ (lit (string "a")) โˆท [])
_ = refl

Here is a simple identity function on the Booleans. A โ€œlamโ€bda with a โ€œvisibleโ€ โ€œabsโ€tract argument named "x" is introduced having as body merely being the 0 nearest-bound variable, applied to an empty list of arguments.

_ : quoteTerm (ฮป (x : Bool) โ†’ x) โ‰ก lam visible (abs "x" (var 0 []))
_ = refl

Here is a more complicated lambda abstraction: Note that f a is represented as the variable 0 lambdas away from the body applied to the variable 1 lambda away from the body.

_ : quoteTerm (ฮป (a : โ„•) (f : โ„• โ†’ โ„•) โ†’ f a)
โ‰ก  lam visible (abs "a"
     (lam visible (abs "f"
       (var 0 (arg (arg-info visible relevant) (var 1 []) โˆท [])))))
_ = refl

This is rather messy, let's introduce some syntactic sugar to make it more readable.

infixr 5 ฮป๐“‹_โ†ฆ_  ฮป๐’ฝ_โ†ฆ_

ฮป๐“‹_โ†ฆ_  ฮป๐’ฝ_โ†ฆ_ : String โ†’ Term โ†’ Term
ฮป๐“‹ x โ†ฆ body  = lam visible (abs x body)
ฮป๐’ฝ x โ†ฆ body  = lam hidden (abs x body)

Now the previous example is a bit easier on the eyes:

_ :   quoteTerm (ฮป (a : โ„•) (f : โ„• โ†’ โ„•) โ†’ f a)
โ‰ก ฮป๐“‹ "a" โ†ฆ ฮป๐“‹ "f" โ†ฆ var 0 [ ๐“‹๐“‡๐’ถ (var 1 []) ]
_ = refl

Using that delicious sugar, let's look at the constant function a number of ways.

_ : {A B : Set} โ†’   quoteTerm (ฮป (a : A) (b : B) โ†’ a)
	      โ‰ก ฮป๐“‹ "a" โ†ฆ (ฮป๐“‹ "b" โ†ฆ var 1 [])
_ = refl

_ :  quoteTerm (ฮป {A B : Set} (a : A) (_ : B) โ†’ a)
โ‰ก (ฮป๐’ฝ "A" โ†ฆ (ฮป๐’ฝ "B" โ†ฆ (ฮป๐“‹ "a" โ†ฆ (ฮป๐“‹ "_" โ†ฆ var 1 []))))
_ = refl

const : {A B : Set} โ†’ A โ†’ B โ†’ A
const a _ = a

_ : quoteTerm const โ‰ก def (quote const) []
_ = refl

Finally, here's an example of a section.

_ :   quoteTerm (_โ‰ก "b")
โ‰ก ฮป๐“‹ "section" โ†ฆ
   (def (quote _โ‰ก_)
    (๐’ฝ๐“‡๐’ถ (def (quote Level.zero) []) โˆท
     ๐’ฝ๐“‡๐’ถ (def (quote String) []) โˆท
     ๐“‹๐“‡๐’ถ (var 0 []) โˆท
     ๐“‹๐“‡๐’ถ (lit (string "b")) โˆท []))
_ = refl

Metaprogramming with The Typechecking Monad TC

The TC monad provides an interface to Agda's type checker.

postulate
  TC       : โˆ€ {a} โ†’ Set a โ†’ Set a
  returnTC : โˆ€ {a} {A : Set a} โ†’ A โ†’ TC A
  bindTC   : โˆ€ {a b} {A : Set a} {B : Set b} โ†’ TC A โ†’ (A โ†’ TC B) โ†’ TC B

In order to use do-notation we need to have the following definitions in scope.

_>>=_        : โˆ€ {a b} {A : Set a} {B : Set b} โ†’ TC A โ†’ (A โ†’ TC B) โ†’ TC B
_>>=_ = bindTC

_>>_        : โˆ€ {a b} {A : Set a} {B : Set b} โ†’ TC A โ†’ TC B โ†’ TC B
_>>_  = ฮป p q โ†’ p >>= (ฮป _ โ†’ q)

The primitives of TC can be seen on the documentation page; below are a few notable ones that we may use. Other primitives include support for the current context, type errors, and metavariables.

postulate
  {- Take what you have and try to make it fit into the current goal. -}
  unify : (have : Term) (goal : Term) โ†’ TC โŠค

  {- Try first computation, if it crashes with a type error, try the second. -}
  catchTC : โˆ€ {a} {A : Set a} โ†’ TC A โ†’ TC A โ†’ TC A

  {- Infer the type of a given term. -}
  inferType : Term โ†’ TC Type

  {- Check a term against a given type. This may resolve implicit arguments
 in the term, so a new refined term is returned. Can be used to create
 new metavariables: newMeta t = checkType unknown t -}
  checkType : Term โ†’ Type โ†’ TC Term

  {- Compute the normal form of a term. -}
  normalise : Term โ†’ TC Term

  {- Quote a value, returning the corresponding Term. -}
  quoteTC : โˆ€ {a} {A : Set a} โ†’ A โ†’ TC Term

  {- Unquote a Term, returning the corresponding value. -}
  unquoteTC : โˆ€ {a} {A : Set a} โ†’ Term โ†’ TC A

  {- Create a fresh name. -}
  freshName : String โ†’ TC Name

  {- Declare a new function of the given type. The function must be defined
 later using 'defineFun'. Takes an Arg Name to allow declaring instances
 and irrelevant functions. The Visibility of the Arg must not be hidden. -}
  declareDef : Arg Name โ†’ Type โ†’ TC โŠค

  {- Define a declared function. The function may have been declared using
 'declareDef' or with an explicit type signature in the program. -}
  defineFun : Name โ†’ List Clause โ†’ TC โŠค

  {- Get the type of a defined name. Replaces 'primNameType'. -}
  getType : Name โ†’ TC Type

  {- Get the definition of a defined name. Replaces 'primNameDefinition'. -}
  getDefinition : Name โ†’ TC Definition

  {-  Change the behaviour of inferType, checkType, quoteTC, getContext
  to normalise (or not) their results. The default behaviour is no
  normalisation. -}
  withNormalisation : โˆ€ {a} {A : Set a} โ†’ Bool โ†’ TC A โ†’ TC A

TC computations, or โ€œmetaprogramsโ€, can be run by declaring them as macros or by unquoting. Let's begin with the former.

Unquoting โ”€Making new functions & types

Recall our RGB example type was a simple enumeration consisting of Red, Green, Blue. Consider the singleton type:

data IsRed : RGB โ†’ Set where
  yes : IsRed Red

The name Red completely determines this datatype; so let's try to generate it mechanically. Unfortunately, as far as I could tell, there is currently no way to unquote data declarations. As such, we'll settle for the following isomorphic functional formulation:

IsRed : RGB โ†’ Set
IsRed x = x โ‰ก Red

First, let's quote the relevant parts, for readability.

โ€œโ„“โ‚€โ€ : Arg Term
โ€œโ„“โ‚€โ€ = ๐’ฝ๐“‡๐’ถ (def (quote Level.zero) [])

โ€œRGBโ€ : Arg Term
โ€œRGBโ€ = ๐’ฝ๐“‡๐’ถ (def (quote RGB) [])

โ€œRedโ€ : Arg Term
โ€œRedโ€ = ๐“‹๐“‡๐’ถ (con (quote Red) [])

The first two have a nearly identical definition and it would be nice to mechanically derive themโ€ฆ

Anyhow, we use the unquoteDecl keyword, which allows us to obtain a NAME value, IsRed. We then quote the desired type, declare a function of that type, then define it using the provided NAME.

unquoteDecl IsRed =
  do ty โ† quoteTC (RGB โ†’ Set)
 declareDef (๐“‹๐“‡๐’ถ IsRed) ty
 defineFun IsRed   [ clause [ ๐“‹๐“‡๐’ถ (var "x") ] (def (quote _โ‰ก_) (โ€œโ„“โ‚€โ€ โˆท โ€œRGBโ€ โˆท โ€œRedโ€ โˆท ๐“‹๐“‡๐“‹ 0 [] โˆท [])) ]

Let's try out our newly declared type.

red-is-a-solution : IsRed Red
red-is-a-solution = refl

green-is-not-a-solution : ยฌ (IsRed Green)
green-is-not-a-solution = ฮป ()

red-is-the-only-solution : โˆ€ {c} โ†’ IsRed c โ†’ c โ‰ก Red
red-is-the-only-solution refl = refl

There is a major problem with using unquoteDef outright like this: We cannot step-wise refine our program using holes ?, since that would result in unsolved meta-variables. Instead, we split this process into two stages: A programming stage, then an unquotation stage.

{- Definition stage, we can use โ€˜?โ€™ as we form this program. -}
define-Is : Name โ†’ Name โ†’ TC โŠค
define-Is is-name qcolour = defineFun is-name
  [ clause [ ๐“‹๐“‡๐’ถ (var "x") ] (def (quote _โ‰ก_) (โ€œโ„“โ‚€โ€ โˆท โ€œRGBโ€ โˆท ๐“‹๐“‡๐’ถ (con qcolour []) โˆท ๐“‹๐“‡๐“‹ 0 [] โˆท [])) ]

declare-Is : Name โ†’ Name โ†’ TC โŠค
declare-Is is-name qcolour =
  do let ฮท = is-name
 ฯ„ โ† quoteTC (RGB โ†’ Set)
 declareDef (๐“‹๐“‡๐’ถ ฮท) ฯ„
 defineFun is-name
   [ clause [ ๐“‹๐“‡๐’ถ (var "x") ]
     (def (quote _โ‰ก_) (โ€œโ„“โ‚€โ€ โˆท โ€œRGBโ€ โˆท ๐“‹๐“‡๐’ถ (con qcolour []) โˆท ๐“‹๐“‡๐“‹ 0 [] โˆท [])) ]

{- Unquotation stage -}
IsRedโ€ฒ : RGB โ†’ Set
unquoteDef IsRedโ€ฒ = define-Is IsRedโ€ฒ (quote Red)

{- Trying it out -}
_ : IsRedโ€ฒ Red
_ = refl

Notice that if we use โ€œunquoteDefโ€, we must provide a type signature. We only do so for illustration; the next code block avoids such a redundancy by using โ€œunquoteDeclโ€.

The above general approach lends itself nicely to the other data constructors as well:

unquoteDecl IsBlue  = declare-Is IsBlue  (quote Blue)
unquoteDecl IsGreen = declare-Is IsGreen (quote Green)

{- Example use -}
disjoint-rgb  : โˆ€{c} โ†’ ยฌ (IsBlue c ร— IsGreen c)
disjoint-rgb (refl , ())

The next natural step is to avoid manually invoking declare-Is for each constructor. Unfortunately, it seems fresh names are not accessible, for some reason. ๐Ÿ˜ข

For example, you would think the following would produce a function named gentle-intro-to-reflection.identity. Yet, it is not in scope. I even tried extracting the definition to its own file and no luck.

unquoteDecl {- identity -}
  = do {- let ฮท = identity -}
   ฮท โ† freshName "identity"
   ฯ„ โ† quoteTC (โˆ€ {A : Set} โ†’ A โ†’ A)
   declareDef (๐“‹๐“‡๐’ถ ฮท) ฯ„
   defineFun ฮท [ clause [ ๐“‹๐“‡๐’ถ (var "x") ] (var 0 []) ]

{- โ€œidentityโ€ is not in scope!?
_ : โˆ€ {x : โ„•}  โ†’  identity x  โ‰ก  x
_ = refl
-}

Exercises:

  1. Comment out the freshName line above and uncomment the surrounding artifacts to so that the above unit test goes through.

  2. Using that as a template, unquote a function everywhere-0 : โ„• โ†’ โ„• that is constantly 0.

  3. Unquote the constant combinator K : {A B : Set} โ†’ A โ†’ B โ†’ A.

    unquoteDecl everywhere-0 = do โ‹ฏ

    _ : everywhere-0 3 โ‰ก 0 _ = refl

    unquoteDecl K = do โ‹ฏ

    _ : K 3 "cat" โ‰ก 3 _ = refl

Bonus: Proofs of a singleton type such as IsRed are essentially the same for all singleton types over RGB. Write, in two stages, a metaprogram that demonstrates each singleton type has a single member โ”€c.f., red-is-the-only-solution from above. Hint: This question is as easy as the ones before it.

{- Programming stage }
declare-unique : Name โ†’ (RGB โ†’ Set) โ†’ RGB โ†’ TC โŠค
declare-unique it S colour =
  = do โ‹ฏ

{- Unquotation stage -}
unquoteDecl red-unique = declare-unique red-unique IsRed Red
unquoteDecl green-unique = declare-unique green-unique IsGreen Green
unquoteDecl blue-unique = declare-unique blue-unique IsBlue Blue

{- Test -}
_ : โˆ€ {c} โ†’ IsGreen c โ†’ c โ‰ก Green
_ = green-unique

Sidequest: Avoid tedious refl proofs

Time for a breather (โ€ขฬ€แด—โ€ขฬ)ูˆ

Look around your code base for a function that makes explicit pattern matching, such as:

just-Red : RGB โ†’ RGB
just-Red Red   = Red
just-Red Green = Red
just-Red Blue  = Red

only-Blue : RGB โ†’ RGB
only-Blue Blue = Blue
only-Blue _   = Blue

Such functions have properties which cannot be proven unless we pattern match on the arguments they pattern match. For example, that the above function is constantly Red requires pattern matching then a refl for each clause.

just-Red-is-constant : โˆ€{c} โ†’ just-Red c โ‰ก Red
just-Red-is-constant {Red}   = refl
just-Red-is-constant {Green} = refl
just-Red-is-constant {Blue}  = refl

{- Yuck, another tedious proof -}
only-Blue-is-constant : โˆ€{c} โ†’ only-Blue c โ‰ก Blue
only-Blue-is-constant {Blue}  = refl
only-Blue-is-constant {Red}   = refl
only-Blue-is-constant {Green} = refl

In such cases, we can encode the general design decisions ---pattern match and yield reflโ€” then apply the schema to each use case.

Here's the schema:

constructors : Definition โ†’ List Name
constructors (data-type pars cs) = cs
constructors _ = []

by-refls : Name โ†’ Term โ†’ TC โŠค
by-refls nom thm-you-hope-is-provable-by-refls
 = let mk-cls : Name โ†’ Clause
   mk-cls qcolour = clause [ ๐’ฝ๐“‡๐’ถ (con qcolour []) ] (con (quote refl) [])
   in
   do let ฮท = nom
  ฮด โ† getDefinition (quote RGB)
  let clauses = List.map mk-cls (constructors ฮด)
  declareDef (๐“‹๐“‡๐’ถ ฮท) thm-you-hope-is-provable-by-refls
  defineFun ฮท clauses

Here's a use case.

_ : โˆ€{c} โ†’ just-Red c โ‰ก Red
_ = nice
  where unquoteDecl nice = by-refls nice (quoteTerm (โˆ€{c} โ†’ just-Red c โ‰ก Red))

Note:

  1. The first nice refers to the function created by the RHS of the unquote.

  2. The RHS nice refers to the Name value provided by the LHS.

  3. The LHS nice is a declaration of a Name value.

This is rather clunky since the theorem to be proven was repeated twice โ”€repetition is a signal that something's wrong! In the next section we use macros to avoid such repetiton, as well as the quoteTerm keyword.

Note that we use a where clause since unquotation cannot occur in a let, for some reason.

Here's another use case of the proof pattern (โ€ขฬ€แด—โ€ขฬ)ูˆ

_ : โˆ€{c} โ†’ only-Blue c โ‰ก Blue
_ = nice
  where unquoteDecl nice = by-refls nice (quoteTerm โˆ€{c} โ†’ only-Blue c โ‰ก Blue)

One proof pattern, multiple invocations! Super neat stuff ๐Ÿ˜

Macros โ”€Abstracting Proof Patterns

Macros are functions of type ฯ„โ‚€ โ†’ ฯ„โ‚ โ†’ โ‹ฏ โ†’ Term โ†’ TC โŠค that are defined in a macro block. The last argument is supplied by the type checker and denotes the โ€œgoalโ€ of where the macro is placed: One generally unifies what they have with the goal, what is desired in the use site.

Why the macro block?

  • Metaprograms can be run in a term position.

  • Without the macro block, we run computations using the unquote keyword.

  • Quotations are performed automatically; e.g., if f : Term โ†’ Name โ†’ Bool โ†’ Term โ†’ TC โŠค then an application f u v w desugars into unquote (f (quoteTerm u) (quote v) w).

    No syntactic overhead: Macros are applied like normal functions.

Macros cannot be recursive; instead one defines a recursive function outside the macro block then has the macro call the recursive function.

C-style macros

In the C language one defines a macro, say, by #define luckyNum 1972 then later uses it simply by the name luckyNum. Without macros, we have syntactic overhead using the unquote keyword:

luckyNumโ‚€ : Term โ†’ TC โŠค
luckyNumโ‚€ h = unify h (quoteTerm 55)

numโ‚€ : โ„•
numโ‚€ = unquote luckyNumโ‚€

Instead, we can achieve C-style behaviour by placing our metaprogramming code within a macro block.

macro
  luckyNum : Term โ†’ TC โŠค
  luckyNum h = unify h (quoteTerm 55)

num : โ„•
num = luckyNum

Unlike C, all code fragments must be well-defined.

Exercise: Write a macro to always yield the first argument in a function. The second example shows how it can be used to access implicit arguments without mentioning them :b

macro
  first : Term โ†’ TC โŠค
  first goal = โ‹ฏ

myconst : {A B : Set} โ†’ A โ†’ B โ†’ A
myconst = ฮป x โ†’ ฮป y โ†’ first

mysum : ({x} y : โ„•) โ†’ โ„•
mysum y = y + first

C-style macros โ”€unifying against a concretely quoted termโ”€ are helpful when learning reflection. For example, define a macro use that yields different strings according to the shape of their input โ”€this exercise increases familiarity with the Term type. Hint: Pattern match on the first argument ;-)

macro
  use : Term โ†’ Term โ†’ TC โŠค
  use = โ‹ฏ

{- Fully defined, no arguments. -}

2+2โ‰ˆ4 : 2 + 2 โ‰ก 4
2+2โ‰ˆ4 = refl

_ : use 2+2โ‰ˆ4 โ‰ก "Nice"
_ = refl

{- โ€˜pโ€™ has arguments. -}

_ : {x y : โ„•} {p : x โ‰ก y} โ†’ use p โ‰ก "WoahThere"
_ = refl

Tedious Repetitive Proofs No More!

Suppose we wish to prove that addition, multiplication, and exponentiation have right units 0, 1, and 1 respectively. We obtain the following nearly identical proofs!

+-rid : โˆ€{n} โ†’ n + 0 โ‰ก n
+-rid {zero}  = refl
+-rid {suc n} = cong suc +-rid

*-rid : โˆ€{n} โ†’ n * 1 โ‰ก n
*-rid {zero}  = refl
*-rid {suc n} = cong suc *-rid

^-rid : โˆ€{n} โ†’ n ^ 1 โ‰ก n
^-rid {zero}  = refl
^-rid {suc n} = cong suc ^-rid

There is clearly a pattern here screaming to be abstracted, let's comply โ™ฅโ€ฟโ™ฅ

The natural course of action in a functional language is to try a higher-order combinator:

{- โ€œfor loopsโ€ or โ€œInduction for โ„•โ€ -}
foldn : (P : โ„• โ†’ Set) (base : P zero) (ind : โˆ€ n โ†’ P n โ†’ P (suc n))
  โ†’ โˆ€(n : โ„•) โ†’ P n
foldn P base ind zero    = base
foldn P base ind (suc n) = ind n (foldn P base ind n)

Now the proofs are shorter:

_ : โˆ€ (x : โ„•) โ†’ x + 0 โ‰ก x
_ = foldn _ refl (ฮป _ โ†’ cong suc)    {- This and next two are the same -}

_ : โˆ€ (x : โ„•) โ†’ x * 1 โ‰ก x
_ = foldn _ refl (ฮป _ โ†’ cong suc)    {- Yup, same proof as previous -}

_ : โˆ€ (x : โ„•) โ†’ x ^ 1 โ‰ก x
_ = foldn _ refl (ฮป _ โ†’ cong suc)    {- No change, same proof as previous -}

Unfortunately, we are manually copy-pasting the same proof pattern.

When you see repetition, copy-pasting, know that there is room for improvement! (โ€ขฬ€แด—โ€ขฬ)ูˆ

Don't repeat yourself!

Repetition can be mitigated a number of ways, including typeclasses or metaprogramming, for example. The latter requires possibly less thought and it's the topic of this article, so let's do that ๐Ÿ˜„

Exercise: Following the template of the previous exercises, fill in the missing parts below. Hint: It's nearly the same level of difficulty as the previous exercises.

make-rid : (let A = โ„•) (_โŠ•_ : A โ†’ A โ†’ A) (e : A) โ†’ Name โ†’ TC โŠค
make-rid _โŠ•_ e nom
 = do โ‹ฏ

_ : โˆ€{x : โ„•} โ†’ x + 0 โ‰ก x
_ = nice where unquoteDecl nice = make-rid _+_ 0 nice

There's too much syntactic overhead here, let's use macros instead.

macro
  _trivially-has-rid_ : (let A = โ„•) (_โŠ•_ : A โ†’ A โ†’ A) (e : A) โ†’ Term โ†’ TC โŠค
  _trivially-has-rid_ _โŠ•_ e goal
   = do ฯ„ โ† quoteTC (ฮป(x : โ„•) โ†’ x โŠ• e โ‰ก x)
    unify goal (def (quote foldn)            {- Using foldn    -}
      ( ๐“‹๐“‡๐’ถ ฯ„                                {- Type P         -}
      โˆท ๐“‹๐“‡๐’ถ (con (quote refl) [])            {- Base case      -}
      โˆท ๐“‹๐“‡๐’ถ (ฮป๐“‹ "_" โ†ฆ quoteTerm (cong suc))  {- Inductive step -}
      โˆท []))

Now the proofs have minimal repetition and the proof pattern is written only once:

_ : โˆ€ (x : โ„•) โ†’ x + 0 โ‰ก x
_ = _+_ trivially-has-rid 0

_ : โˆ€ (x : โ„•) โ†’ x * 1 โ‰ก x
_ = _*_ trivially-has-rid 1

_ : โˆ€ (x : โ„•) โ†’ x * 1 โ‰ก x
_ = _^_ trivially-has-rid 1

Note we could look at the type of the goal, find the operator _โŠ•_ and the unit; they need not be passed in. Later we will see how to reach into the goal type and pull pieces of it out for manipulation (โ€ขฬ€แด—โ€ขฬ)ูˆ

It would have been ideal if we could have defined our macro without using foldn; I could not figure out how to do that. ๐Ÿ˜ง

Before one abstracts a pattern into a macro, it's useful to have a few instances of the pattern beforehand. When abstracting, one may want to compare how we think versus how Agda's thinking. For example, you may have noticed that in the previous macro, Agda normalised the expression suc n + 0 into suc (n + 0) by invoking the definition of _+_. We may inspect the goal of a function with the quoteGoal โ‹ฏ in โ‹ฏ syntax:

+-ridโ€ฒ : โˆ€{n} โ†’ n + 0 โ‰ก n
+-ridโ€ฒ {zero}  = refl
+-ridโ€ฒ {suc n} = quoteGoal e in
  let
suc-n : Term
suc-n = con (quote suc) [ ๐“‹๐“‡๐’ถ (var 0 []) ]

lhs : Term
lhs = def (quote _+_) (๐“‹๐“‡๐’ถ suc-n โˆท ๐“‹๐“‡๐’ถ (lit (nat 0)) โˆท [])

{- Check our understanding of what the goal is โ€œeโ€. -}
_ : e โ‰ก def (quote _โ‰ก_)
	     (๐’ฝ๐“‡๐’ถ (quoteTerm Level.zero) โˆท ๐’ฝ๐“‡๐’ถ (quoteTerm โ„•)
	     โˆท ๐“‹๐“‡๐’ถ lhs โˆท ๐“‹๐“‡๐’ถ suc-n โˆท [])
_ = refl

{- What does it look normalised. -}
_ :   quoteTerm (suc (n + 0) โ‰ก n)
     โ‰ก unquote ฮป goal โ†’ (do g โ† normalise goal; unify g goal)
_ = refl
  in
  cong suc +-ridโ€ฒ

It would be really nice to simply replace the last line by a macro, say induction. Unfortunately, for that I would need to obtain the name +-ridโ€ฒ, which as far as I could tell is not possible with the current reflection mechanism.

Our First Real Proof Tactic

When we have a proof p : x โ‰ก y it is a nuisance to have to write sym p to prove y โ‰ก x โ”€we have to remember which โ€˜directionโ€™ p. Let's alleviate such a small burden, then use the tools here to alleviate a larger burden later; namely, rewriting subexpressions.

Given p : x โ‰ก y, we cannot simply yield def (quote sym) [ ๐“‹๐“‡๐’ถ p ] since sym actually takes four arguments โ”€compare when we quoted _โ‰ก_ earlier. Instead, we infer type of p to be, say, quoteTerm (_โ‰ก_ {โ„“} {A} x y). Then we can correctly provide all the required arguments.

โ‰ก-type-info : Term โ†’ TC (Arg Term ร— Arg Term ร— Term ร— Term)
โ‰ก-type-info (def (quote _โ‰ก_) (๐“ โˆท ๐’ฏ โˆท arg _ l โˆท arg _ r โˆท [])) = returnTC (๐“ , ๐’ฏ , l , r)
โ‰ก-type-info _ = typeError [ strErr "Term is not a โ‰ก-type." ]

What if later we decided that we did not want a proof of x โ‰ก y, but rather of x โ‰ก y. In this case, the orginal proof p suffices. Rather than rewriting our proof term, our macro could try providing it if the symmetry application fails.

{- Syntactic sugar for trying a computation, if it fails then try the other one -}
try-fun : โˆ€ {a} {A : Set a} โ†’ TC A โ†’ TC A โ†’ TC A
try-fun = catchTC

syntax try-fun t f = try t or-else f

With the setup in hand, we can now form our macro:

macro
  applyโ‚ : Term โ†’ Term โ†’ TC โŠค
  applyโ‚ p goal = try (do ฯ„ โ† inferType p
		      ๐“ , ๐’ฏ , l , r โ† โ‰ก-type-info ฯ„
		      unify goal (def (quote sym) (๐“ โˆท ๐’ฏ โˆท ๐’ฝ๐“‡๐’ถ l โˆท ๐’ฝ๐“‡๐’ถ r โˆท ๐“‹๐“‡๐’ถ p โˆท [])))
	      or-else
		   unify goal p

For example:

postulate ๐“ ๐“Ž : โ„•
postulate ๐“† : ๐“ + 2 โ‰ก ๐“Ž

{- Same proof yields two theorems! (เธ‡เฒ _เฒ )เธ‡ -}
_ : ๐“Ž โ‰ก ๐“ + 2
_ = applyโ‚ ๐“†

_ : ๐“ + 2 โ‰ก ๐“Ž
_ = applyโ‚ ๐“†

Let's furnish ourselves with the ability to inspect the produced proofs.

{- Type annotation -}
syntax has A a = a โˆถ A

has : โˆ€ (A : Set) (a : A) โ†’ A
has A a = a

We are using the โ€˜ghost colonโ€™ obtained with input \:.

Let's try this on an arbitrary type:

woah : {A : Set} (x y : A) โ†’ x โ‰ก y โ†’ (y โ‰ก x) ร— (x โ‰ก y)
woah x y p = applyโ‚ p , applyโ‚ p

  where -- Each invocation generates a different proof, indeed:

  first-pf : (applyโ‚ p โˆถ (y โ‰ก x)) โ‰ก sym p
  first-pf = refl

  second-pf : (applyโ‚ p โˆถ (x โ‰ก y)) โ‰ก p
  second-pf = refl

It is interesting to note that on non โ‰ก-terms, applyโ‚ is just a no-op. Why might this be the case?

_ : โˆ€ {A : Set} {x : A} โ†’ applyโ‚ x โ‰ก x
_ = refl

_ : applyโ‚ "huh" โ‰ก "huh"
_ = refl

Exercise: When we manually form a proof invoking symmetry we simply write, for example, sym p and the implict arguments are inferred. We can actually do the same thing here! We were a bit dishonest above. ๐Ÿ‘‚ Rewrite applyโ‚, call it applyโ‚‚, so that the ~try block is a single, unparenthesised, unify call.

Exercise: Extend the previous macro so that we can prove statements of the form x โ‰ก x regardless of what p proves. Aesthetics hint: try_or-else_ doesn't need brackets in this case, at all.

macro
  applyโ‚ƒ : Term โ†’ Term โ†’ TC โŠค
  applyโ‚ƒ p goal = โ‹ฏ

yummah : {A : Set} {x y : A} (p : x โ‰ก y)  โ†’  x โ‰ก y  ร—  y โ‰ก x  ร—  y โ‰ก y
yummah p = applyโ‚ƒ p , applyโ‚ƒ p , applyโ‚ƒ p

Exercise: Write the following seemingly silly macro. Hint: You cannot use the โ‰ก-type-info method directly, instead you must invoke getType beforehand.

โ‰ก-type-infoโ€ฒ : Name โ†’ TC (Arg Term ร— Arg Term ร— Term ร— Term)
โ‰ก-type-infoโ€ฒ = โ‹ฏ

macro
  sumSides : Name โ†’ Term โ†’ TC โŠค
  sumSides n goal = โ‹ฏ

_ : sumSides ๐“† โ‰ก ๐“ + 2 + ๐“Ž
_ = refl

Exercise: Write two macros, left and right, such that sumSides q โ‰ก left q + right q, where q is a known name. These two macros provide the left and right hand sides of the โ‰ก-term they are given.

Heuristic for Writing a Macro

I have found the following stepwise refinement approach to be useful in constructing macros. โ”€Test Driven Development in a proof-centric settingโ”€

  1. Write a no-op macro: mymacro p goal = unify p goal.
  2. Write the test case mymacro p โ‰ก p.
  3. Feel good, you've succeeded.
  4. Alter the test ever so slightly to become closer to your goal.
  5. The test now breaks, go fix it.
  6. Go to step 3.

For example, suppose we wish to consider proofs p of expressions of the form h x โ‰ก y and our macro is intended to obtain the function h. We proceed as follows:

  1. Postulate x, y, h, p so the problem is well posed.

  2. Use the above approach to form a no-op macro.

  3. Refine the test to mymacro p โ‰ก ฮป e โ†’ 0 and refine the macro as well.

  4. Refine the test to mymacro p โ‰ก ฮป e โ†’ e and refine the macro as well.

  5. Eventually succeeded in passing the desired test mymacro p โ‰ก ฮป e โ†’ h e โ”€then eta reduce.

    Along the way, it may be useful to return the string name of h or rewrite the test as _โ‰ก_ {Level.zero} {โ„• โ†’ โ„•} (mymacro p) โ‰ก โ‹ฏ. This may provide insight on how to repair or continue with macro construction.

  6. Throw away the postultes, one at a time, making them arguments declared in the test; refine macro each time so the test continues to pass as each postulate is removed. Each postulate removal may require existing helper functions to be altered.

  7. We have considered function applications, then variable funcctions, finally consider constructors. Ensure tests cover all these, for this particular problem.

Exercise: Carry this through to produce the above discussed example macro, call it โ‰ก-head. To help you on your way, here is a useful function:

{- If we have โ€œf $ argsโ€ return โ€œfโ€. -}
$-head : Term โ†’ Term
$-head (var v args) = var v []
$-head (con c args) = con c []
$-head (def f args) = def f []
$-head (pat-lam cs args) = pat-lam cs []
$-head t = t

With the ability to obtain functions being applied in propositional equalities, we can now turn to lifiting a proof from x โ‰ก y to suffice proving f x โ‰ก f y. We start with the desired goal and use the stepwise refinement approach outlined earlier to arrive at:

macro
  applyโ‚„ : Term โ†’ Term โ†’ TC โŠค
  applyโ‚„ p goal = try (do ฯ„ โ† inferType goal
		      _ , _ , l , r โ† โ‰ก-type-info ฯ„
		      unify goal ((def (quote cong) (๐“‹๐“‡๐’ถ ($-head l) โˆท ๐“‹๐“‡๐’ถ p โˆท []))))
	      or-else unify goal p

_ : โˆ€ {x y : โ„•} {f : โ„• โ†’ โ„•} (p : x โ‰ก y)  โ†’ f x โ‰ก f y
_ = ฮป p โ†’ applyโ‚„ p

_ : โˆ€ {x y : โ„•} {f g : โ„• โ†’ โ„•} (p : x โ‰ก y)
โ†’  x โ‰ก y
-- โ†’  f x โ‰ก g y {- โ€œapplyโ‚„ pโ€ now has a unification error ^_^ -}
_ = ฮป p โ†’ applyโ‚„ p

What about somewhere deep within a subexpression?

Consider,

  suc X + (X * suc X + suc X)
โ‰กโŸจ cong (ฮป it โ†’ suc X + it) (+-suc _ _) โŸฉ
  suc X + suc (X * suc X + X)

Can we find (ฮป it โ†’ suc X + it) mechanically ;-)

Using the same refinement apporach outlined earlier, we begin with the following working code then slowly, one piece at a time, replace the whole thing with an unquote (unify (quoteTerm โ‹ฏworkingCodeHereโ‹ฏ)). Then we push the quoteTerm further in as much as possible and construct the helper functions to make this transation transpire.

open import Data.Nat.Properties
{- +-suc : โˆ€ m n โ†’ m + suc n โ‰ก suc (m + n) -}

testโ‚€ : โˆ€ {m n k : โ„•} โ†’ k + (m + suc n) โ‰ก k + suc (m + n)
testโ‚€ {m} {n} {k} = cong (k +_) (+-suc m n)

Let's follow the aforementioned approach by starting out with some postulates.

postulate ๐’ณ : โ„•
postulate ๐’ข : suc ๐’ณ + (๐’ณ * suc ๐’ณ + suc ๐’ณ)  โ‰ก  suc ๐’ณ + suc (๐’ณ * suc ๐’ณ + ๐’ณ)

๐’ฎ๐’ณ : Arg Term
๐’ฎ๐’ณ = ๐“‹๐“‡๐’ถ (con (quote suc) [ ๐“‹๐“‡๐’ถ (quoteTerm ๐’ณ) ])

๐’ขหก ๐’ขสณ : Term
๐’ขหก = def (quote _+_) (๐’ฎ๐’ณ โˆท ๐“‹๐“‡๐’ถ (def (quote _+_) (๐“‹๐“‡๐’ถ (def (quote _*_) (๐“‹๐“‡๐’ถ (quoteTerm ๐’ณ) โˆท ๐’ฎ๐’ณ โˆท [])) โˆท ๐’ฎ๐’ณ โˆท [])) โˆท [])
๐’ขสณ = def (quote _+_) (๐’ฎ๐’ณ โˆท ๐“‹๐“‡๐’ถ (con (quote suc) [ ๐“‹๐“‡๐’ถ (def (quote _+_) (๐“‹๐“‡๐’ถ (def (quote _*_) (๐“‹๐“‡๐’ถ (quoteTerm ๐’ณ) โˆท ๐’ฎ๐’ณ โˆท [])) โˆท ๐“‹๐“‡๐’ถ (quoteTerm ๐’ณ) โˆท [])) ]) โˆท [])

It seems that the left and right sides of ๐’ข โ€œmeetโ€ at def (quote _+_) (๐’ฎ๐’ณ โˆท []): We check the equality of the quoted operator, _+_, then recursively check the arguments. Whence the following naive algorithm:

{- Should definitely be in the standard library -}
โŒŠ_โŒ‹ : โˆ€ {a} {A : Set a} โ†’ Dec A โ†’ Bool
โŒŠ yes p โŒ‹ = true
โŒŠ no ยฌp โŒ‹ = false

import Agda.Builtin.Reflection as Builtin

_$-โ‰Ÿ_ : Term โ†’ Term โ†’ Bool
con c args $-โ‰Ÿ con cโ€ฒ argsโ€ฒ = Builtin.primQNameEquality c cโ€ฒ
def f args $-โ‰Ÿ def fโ€ฒ argsโ€ฒ = Builtin.primQNameEquality f fโ€ฒ
var x args $-โ‰Ÿ var xโ€ฒ argsโ€ฒ = โŒŠ x Nat.โ‰Ÿ xโ€ฒ โŒ‹
_ $-โ‰Ÿ _ = false

{- Only gets heads and as much common args, not anywhere deep. :'( -}
infix 5 _โŠ“_
{-# TERMINATING #-} {- Fix this by adding fuel (con c args) โ‰” 1 + length args -}
_โŠ“_ : Term โ†’ Term โ†’ Term
l โŠ“ r with l $-โ‰Ÿ r | l | r
...| false | x | y = unknown
...| true | var f args | var fโ€ฒ argsโ€ฒ = var f (List.zipWith (ฮป{ (arg i!! t) (arg j!! s) โ†’ arg i!! (t โŠ“ s) }) args argsโ€ฒ)
...| true | con f args | con fโ€ฒ argsโ€ฒ = con f (List.zipWith (ฮป{ (arg i!! t) (arg j!! s) โ†’ arg i!! (t โŠ“ s) }) args argsโ€ฒ)
...| true | def f args | def fโ€ฒ argsโ€ฒ = def f (List.zipWith (ฮป{ (arg i!! t) (arg j!! s) โ†’ arg i!! (t โŠ“ s) }) args argsโ€ฒ)
...| true | ll | _ = ll {- Left biased; using โ€˜unknownโ€™ does not ensure idempotence. -}

The bodies have names involving !!, this is to indicate a location of improvement. Indeed, this naive algorithm ignores visibility and relevance of arguments โ”€far from ideal.

Joyously this works! ๐Ÿ˜‚

_ : ๐’ขหก โŠ“ ๐’ขสณ โ‰ก def (quote _+_) (๐’ฎ๐’ณ โˆท ๐“‹๐“‡๐’ถ unknown โˆท [])
_ = refl

{- test using argument function ๐’ถ and argument number X -}
_ : {X : โ„•} {๐’ถ : โ„• โ†’ โ„•}
  โ†’
let gl = quoteTerm (๐’ถ X + (X * ๐’ถ X + ๐’ถ X))
    gr = quoteTerm (๐’ถ X + ๐’ถ (X * ๐’ถ X + X))
in gl โŠ“ gr โ‰ก def (quote _+_) (๐“‹๐“‡๐’ถ (var 0 [ ๐“‹๐“‡๐’ถ (var 1 []) ]) โˆท ๐“‹๐“‡๐’ถ unknown โˆท [])
_ = refl

The unknown terms are far from desirable โ”€we ought to replace them with sections; i.e., an anonoymous lambda. My naive algorithm to achieve a section from a term containing โ€˜unknownโ€™s is as follows:

  1. Replace every unknown with a De Bruijn index.
  2. Then, find out how many unknowns there are, and for each, stick an anonoymous lambda at the front.
    • Sticking a lambda at the front breaks existing De Bruijn indices, so increment them for each lambda.

There is clear inefficiency here, but I'm not aiming to be efficient, just believable to some degree.

{- โ€˜unknownโ€™ goes to a variable, a De Bruijn index -}
unknown-elim : โ„• โ†’ List (Arg Term) โ†’ List (Arg Term)
unknown-elim n [] = []
unknown-elim n (arg i unknown โˆท xs) = arg i (var n []) โˆท unknown-elim (n + 1) xs
unknown-elim n (arg i (var x args) โˆท xs) = arg i (var (n + suc x) args) โˆท unknown-elim n xs
unknown-elim n (arg i x โˆท xs)       = arg i x โˆท unknown-elim n xs
{- Essentially we want: body(unknownแตข)  โ‡’  ฮป _ โ†’ body(var 0)
   However, now all โ€œvar 0โ€ references in โ€œbodyโ€ refer to the wrong argument;
   they now refer to โ€œone more lambda away than beforeโ€. -}

unknown-count : List (Arg Term) โ†’ โ„•
unknown-count [] = 0
unknown-count (arg i unknown โˆท xs) = 1 + unknown-count xs
unknown-count (arg i _ โˆท xs) = unknown-count xs

unknown-ฮป : โ„• โ†’ Term โ†’ Term
unknown-ฮป zero body = body
unknown-ฮป (suc n) body = unknown-ฮป n (ฮป๐“‹ "section" โ†ฆ body)

{- Replace โ€˜unknownโ€™ with sections -}
patch : Term โ†’ Term
patch it@(def f args) = unknown-ฮป (unknown-count args) (def f (unknown-elim 0 args))
patch it@(var f args) = unknown-ฮป (unknown-count args) (var f (unknown-elim 0 args))
patch it@(con f args) = unknown-ฮป (unknown-count args) (con f (unknown-elim 0 args))
patch t = t

Putting meet, _โŠ“_, and this patch together into a macro:

macro
  spine : Term โ†’ Term โ†’ TC โŠค
  spine p goal
= do ฯ„ โ† inferType p
     _ , _ , l , r โ† โ‰ก-type-info ฯ„
     unify goal (patch (l โŠ“ r))

The expected tests pass โ”€so much joy ๐Ÿ˜‚

_ : spine ๐’ข โ‰ก suc ๐’ณ +_
_ = refl

module testing-postulated-functions where
  postulate ๐’ถ : โ„• โ†’ โ„•
  postulate _๐’ท_ : โ„• โ†’ โ„• โ†’ โ„•
  postulate ๐“ฐ : ๐’ถ ๐’ณ  ๐’ท  ๐’ณ  โ‰ก  ๐’ถ ๐’ณ  ๐’ท  ๐’ถ ๐“

  _ : spine ๐“ฐ โ‰ก (๐’ถ ๐’ณ ๐’ท_)
  _ = refl

_ : {X : โ„•} {G : suc X + (X * suc X + suc X)  โ‰ก  suc X + suc (X * suc X + X)}
  โ†’ quoteTerm G โ‰ก var 0 []
_ = refl

The tests for โ‰ก-head still go through using spine which can thus be thought of as a generalisation ;-)

Now the original problem is dealt with as a macro:

macro
  applyโ‚… : Term โ†’ Term โ†’ TC โŠค
  applyโ‚… p hole
= do ฯ„ โ† inferType hole
     _ , _ , l , r โ† โ‰ก-type-info ฯ„
     unify hole ((def (quote cong)
	  (๐“‹๐“‡๐’ถ (patch (l โŠ“ r)) โˆท ๐“‹๐“‡๐’ถ p โˆท [])))

Curious, why in the following tests we cannot simply use +-suc _ _?

_ : suc ๐’ณ + (๐’ณ * suc ๐’ณ + suc ๐’ณ)  โ‰ก  suc ๐’ณ + suc (๐’ณ * suc ๐’ณ + ๐’ณ)
_ = applyโ‚… (+-suc (๐’ณ * suc ๐’ณ) ๐’ณ)

test : โˆ€ {m n k : โ„•} โ†’ k + (m + suc n) โ‰ก k + suc (m + n)
test {m} {n} {k} = applyโ‚… (+-suc m n)

This is super neat stuff ^_^

About

A slow-paced introduction to reflection in Agda. ---Tactics!

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages