The type checking monad

Content created by Fredrik Bakke and Fernando Chu.

Created on 2023-04-27.
Last modified on 2023-09-10.

{-# OPTIONS --no-exact-split #-}

module reflection.type-checking-monad where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels

open import lists.lists

open import primitives.strings

open import reflection.arguments
open import reflection.definitions
open import reflection.metavariables
open import reflection.names
open import reflection.terms

Idea

The type-checking monad TC allows us to interact directly with Agda's type checking mechanism. Additionally to primitives (see below), Agda includes the the keyword unquote to manually unquote an element from TC unit.

Definition

data ErrorPart : UU lzero where
  strErr : String → ErrorPart
  termErr : Term → ErrorPart
  pattErr : Pattern → ErrorPart
  nameErr : Name → ErrorPart

postulate
  -- The type checking monad
  TC : ∀ {a} → UU a → UU a
  returnTC : ∀ {a} {A : UU a} → A → TC A
  bindTC : ∀ {a b} {A : UU a} {B : UU b} → TC A → (A → TC B) → TC B
  -- Tries the unify the first term with the second
  unify : Term → Term → TC unit
  -- Gives an error
  typeError : ∀ {a} {A : UU a} → list ErrorPart → TC A
  -- Infers the type of a goal
  inferType : Term → TC Term
  checkType : Term → Term → TC Term
  normalise : Term → TC Term
  reduce : Term → TC Term
  -- Tries the first computation, if it fails tries the second
  catchTC : ∀ {a} {A : UU a} → TC A → TC A → TC A
  quoteTC : ∀ {a} {A : UU a} → A → TC Term
  unquoteTC : ∀ {a} {A : UU a} → Term → TC A
  quoteωTC : ∀ {A : UUω} → A → TC Term
  getContext : TC Telescope
  extendContext : ∀ {a} {A : UU a} → String → Arg Term → TC A → TC A
  inContext : ∀ {a} {A : UU a} → Telescope → TC A → TC A
  freshName : String → TC Name
  declareDef : Arg Name → Term → TC unit
  declarePostulate : Arg Name → Term → TC unit
  defineFun : Name → list Clause → TC unit
  getType : Name → TC Term
  getDefinition : Name → TC Definition
  blockOnMeta : ∀ {a} {A : UU a} → Meta → TC A
  commitTC : TC unit
  isMacro : Name → TC bool

  formatErrorParts : list ErrorPart → TC String

  -- Prints the third argument if the corresponding verbosity level is turned
  -- on (with the -v flag to Agda).
  debugPrint : String → ℕ → list ErrorPart → TC unit

  -- If 'true', makes the following primitives also normalise
  -- their results: inferType, checkType, quoteTC, getType, and getContext
  withNormalisation : ∀ {a} {A : UU a} → bool → TC A → TC A
  askNormalisation : TC bool

  -- If 'true', makes the following primitives to reconstruct hidden arguments:
  -- getDefinition, normalise, reduce, inferType, checkType and getContext
  withReconstructed : ∀ {a} {A : UU a} → bool → TC A → TC A
  askReconstructed : TC bool

  -- Whether implicit arguments at the end should be turned into metavariables
  withExpandLast : ∀ {a} {A : UU a} → bool → TC A → TC A
  askExpandLast : TC bool

  -- White/blacklist specific definitions for reduction while executing the TC computation
  -- 'true' for whitelist, 'false' for blacklist
  withReduceDefs : ∀ {a} {A : UU a} → (Σ bool λ _ → list Name) → TC A → TC A
  askReduceDefs : TC (Σ bool λ _ → list Name)

  -- Fail if the given computation gives rise to new, unsolved
  -- "blocking" constraints.
  noConstraints : ∀ {a} {A : UU a} → TC A → TC A

  -- Run the given TC action and return the first component. Resets to
  -- the old TC state if the second component is 'false', or keep the
  -- new TC state if it is 'true'.
  runSpeculative : ∀ {a} {A : UU a} → TC (Σ A λ _ → bool) → TC A

  -- Get a list of all possible instance candidates for the given meta
  -- variable (it does not have to be an instance meta).
  getInstances : Meta → TC (list Term)

  declareData : Name → ℕ → Term → TC unit
  defineData : Name → list (Σ Name (λ _ → Term)) → TC unit
Bindings 
{-# BUILTIN AGDAERRORPART ErrorPart #-}
{-# BUILTIN AGDAERRORPARTSTRING strErr #-}
{-# BUILTIN AGDAERRORPARTTERM termErr #-}
{-# BUILTIN AGDAERRORPARTPATT pattErr #-}
{-# BUILTIN AGDAERRORPARTNAME nameErr #-}

{-# BUILTIN AGDATCM TC #-}
{-# BUILTIN AGDATCMRETURN returnTC #-}
{-# BUILTIN AGDATCMBIND bindTC #-}
{-# BUILTIN AGDATCMUNIFY unify #-}
{-# BUILTIN AGDATCMTYPEERROR typeError #-}
{-# BUILTIN AGDATCMINFERTYPE inferType #-}
{-# BUILTIN AGDATCMCHECKTYPE checkType #-}
{-# BUILTIN AGDATCMNORMALISE normalise #-}
{-# BUILTIN AGDATCMREDUCE reduce #-}
{-# BUILTIN AGDATCMCATCHERROR catchTC #-}
{-# BUILTIN AGDATCMQUOTETERM quoteTC #-}
{-# BUILTIN AGDATCMUNQUOTETERM unquoteTC #-}
{-# BUILTIN AGDATCMQUOTEOMEGATERM quoteωTC #-}
{-# BUILTIN AGDATCMGETCONTEXT getContext #-}
{-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-}
{-# BUILTIN AGDATCMINCONTEXT inContext #-}
{-# BUILTIN AGDATCMFRESHNAME freshName #-}
{-# BUILTIN AGDATCMDECLAREDEF declareDef #-}
{-# BUILTIN AGDATCMDECLAREPOSTULATE declarePostulate #-}
{-# BUILTIN AGDATCMDEFINEFUN defineFun #-}
{-# BUILTIN AGDATCMGETTYPE getType #-}
{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
{-# BUILTIN AGDATCMBLOCKONMETA blockOnMeta #-}
{-# BUILTIN AGDATCMCOMMIT commitTC #-}
{-# BUILTIN AGDATCMISMACRO isMacro #-}
{-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-}
{-# BUILTIN AGDATCMFORMATERRORPARTS formatErrorParts #-}
{-# BUILTIN AGDATCMDEBUGPRINT debugPrint #-}
-- {-# BUILTIN AGDATCMWITHRECONSTRUCTED withReconstructed #-}
-- {-# BUILTIN AGDATCMWITHEXPANDLAST withExpandLast #-}
-- {-# BUILTIN AGDATCMWITHREDUCEDEFS withReduceDefs #-}
-- {-# BUILTIN AGDATCMASKNORMALISATION askNormalisation #-}
-- {-# BUILTIN AGDATCMASKRECONSTRUCTED askReconstructed #-}
-- {-# BUILTIN AGDATCMASKEXPANDLAST askExpandLast #-}
-- {-# BUILTIN AGDATCMASKREDUCEDEFS askReduceDefs #-}
{-# BUILTIN AGDATCMNOCONSTRAINTS noConstraints #-}
{-# BUILTIN AGDATCMRUNSPECULATIVE runSpeculative #-}
{-# BUILTIN AGDATCMGETINSTANCES getInstances #-}
{-# BUILTIN AGDATCMDECLAREDATA declareData #-}
{-# BUILTIN AGDATCMDEFINEDATA defineData #-}

Monad syntax

infixl 15 _<|>_
_<|>_ : {l : Level} {A : UU l} → TC A → TC A → TC A
_<|>_ = catchTC

infixl 10 _>>=_ _>>_ _<&>_
_>>=_ :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  TC A → (A → TC B) → TC B
_>>=_ = bindTC

_>>_ :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  TC A → TC B → TC B
xs >> ys = bindTC xs (λ _ → ys)

_<&>_ :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  TC A → (A → B) → TC B
xs <&> f = bindTC xs (λ x → returnTC (f x))

Examples

The following examples show how the type-checking monad can be used. They were adapted from alhassy's gentle intro to reflection.

Unifying a goal with a constant

Manually

private
  numTCM : Term → TC unit
  numTCM h = unify (quoteTerm 314) h

  _ : unquote numTCM ＝ 314
  _ = refl

By use of a macro

  macro
    numTCM' : Term → TC unit
    numTCM' h = unify (quoteTerm 1) h

  _ : numTCM' ＝ 1
  _ = refl

Modifying a term

  macro
    swap-add : Term → Term → TC unit
    swap-add (def (quote add-ℕ) (cons a (cons b nil))) hole =
      unify hole (def (quote add-ℕ) (cons b (cons a nil)))
    {-# CATCHALL #-}
    swap-add v hole = unify hole v

  ex1 : (a b : ℕ) → swap-add (add-ℕ a b) ＝ (add-ℕ b a)
  ex1 a b = refl

  ex2 : (a b : ℕ) → swap-add a ＝ a
  ex2 a b = refl

Trying a path

The following example tries to solve a goal by using path p or inv p. This example was addapted from

  private
    infixr 10 _∷_
    pattern _∷_ x xs = cons x xs

  ＝-type-info : Term → TC (Arg Term × (Arg Term × (Term × Term)))
  ＝-type-info
    ( def (quote _＝_) (𝓁 ∷ 𝒯 ∷ (arg _ l) ∷ (arg _ r) ∷ nil)) =
    returnTC (𝓁 , 𝒯 , l , r)
  ＝-type-info _ = typeError (unit-list (strErr "Term is not a ＝-type."))

  macro
    try-path! : Term → Term → TC unit
    try-path! p goal =
      ( unify goal p) <|>
      ( do
        p-type ← inferType p
        𝓁 , 𝒯 , l , r ← ＝-type-info p-type
        unify goal
          ( def (quote inv)
            ( 𝓁 ∷ 𝒯 ∷ hidden-Arg l ∷ hidden-Arg r ∷ visible-Arg p ∷ nil)))

  module _ (a b : ℕ) (p : a ＝ b) where
    ex3 : Id a b
    ex3 = try-path! p

    ex4 : Id b a
    ex4 = try-path! p

Getting the lhs and rhs of a goal

boundary-TCM : Term → TC (Term × Term)
boundary-TCM
  ( def
    ( quote Id)
    ( 𝓁 ∷ 𝒯 ∷ arg _ l ∷ arg _ r ∷ nil)) =
  returnTC (l , r)
boundary-TCM t =
  typeError
    ( strErr "The term\n " ∷
      termErr t ∷
      strErr "\nis not a ＝-type." ∷
      nil)

Recent changes