module BoveReloaded where open import Level renaming (zero to zeroL ; suc to sucL) open import Function open import Data.Empty open import Data.Unit hiding (_≤?_ ; decTotalOrder ; _≤_ ) open import Data.Product open import Data.Sum open import Data.Nat hiding (_≤_) open import Data.Nat.Properties open import Data.List open import Data.List.All open import Relation.Nullary open import Relation.Unary open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Induction open import Induction.Nat as IndNat open import Induction.Lexicographic open import Category.Applicative open import Category.Monad -- * Universe of (collapsible) datatypes {- In this file, we will *compute* (on the fly) the inductive family representing a given Bove-Capretta predicate. To this end, we need first-class inductive families, ie. inductives we can build from within the type theory. I'll achieve this by defining a *universe* of inductive families in Agda. A usual universe of datatypes would be closed under Σ-type: that's the one code that lets us store information in a datatype. However, because we want to erase our Bove-Capretta witnesses at run-time, we must make sure that their inductive definition has no computational content by forbidding the Σ-code (and its variants). We shall call the datatypes thus described the "collapsible datatypes", based on the idea that they have no computational content. This terminology (and claim) will be formally justified in the last Section. We thus define a set of codes : -} data CDesc (I : Set) : Set₁ where `0 : CDesc I `1 : CDesc I `X : (i : I) → CDesc I _`×_ : (A B : CDesc I) → CDesc I `Π : (S : Set)(T : S → CDesc I) → CDesc I {- Followed by their interpretation, which builds functors from Set/I to Set: -} ⟦_⟧ : {I : Set} → CDesc I → (I → Set) → Set ⟦ `0 ⟧ X = ⊥ ⟦ `1 ⟧ X = ⊤ ⟦ `X i ⟧ X = X i ⟦ A `× B ⟧ X = ⟦ A ⟧ X × ⟦ B ⟧ X ⟦ `Π S T ⟧ X = (s : S) → ⟦ T s ⟧ X {- We obtain the code of (collapsible) descriptions, which describe endofunctors on Set/I: -} record CFunc (I : Set) : Set₁ where constructor mk field func : I → CDesc I {- From which we can define a generic least fixpoint operator : -} data μ {I : Set}(R : CFunc I)(i : I) : Set where con : ⟦ CFunc.func R i ⟧ (μ R) → μ R i {- From there, we can also define induction over these structures, but we won't need it in this file. -} -- * The recursion oracle: {- Now, the game is to provide a domain-specific language for the programmer to write a recursive function and prove, after the fact, that the function is indeed well-defined. -} module RecMonad (A : Set)(B : A → Set) where {- To describe a recursive function of type [(a : A) → B a], we take the free monad of the signature [call : (a : A) → B a] -} data RecMon (X : Set) : Set where callRec : (a : A)(rec : B a → RecMon X) → RecMon X returnRec : (x : X) → RecMon X recMon : RawMonad RecMon recMon = record { return = returnRec ; _>>=_ = _>>=_ } where _>>=_ : ∀{X Y : Set} → RecMon X → (X → RecMon Y) → RecMon Y returnRec x >>= f = f x callRec a rec >>= f = callRec a (λ b → (rec b) >>= f) {- The type recProg captures those functions defined with the recursion oracle : -} recProg : (A : Set)(B : A → Set) → Set recProg A B = (a : A) → RecMonad.RecMon A B (B a) {- Besides the monadic structure of recProg, we can call the oracle with the call⟨_⟩ operation : -} call⟨_⟩ : {A : Set}{B : A → Set} → recProg A B call⟨ a ⟩ = RecMonad.callRec a return where open RawMonad (RecMonad.recMon _ _) {- Intuitively, the call⟨_⟩ operation is our oracle, providing a (B a)-result to any A-query. We thus write our recursive programs by calling the oracle instead of doing a recursive call. -} -- ** Example 1: gcd module Gcd where open RawMonad (RecMonad.recMon (ℕ × ℕ) (λ _ → ℕ)) {- We implement gcd pretty much as usual, using the oracle in the recursive cases : -} gcd : recProg (ℕ × ℕ) (λ _ → ℕ) gcd (0 , n) = return n gcd (m , 0) = return m gcd (suc m , suc n) with m ≤? n ... | yes _ = call⟨ suc m , n ∸ m ⟩ ... | no _ = call⟨ m ∸ n , suc n ⟩ open Gcd -- ** Example: fib module Fib where open RawMonad (RecMonad.recMon ℕ (λ _ → ℕ)) {- We can also chain recursive calls, as per the monadic structure. For example, we can write the naïve Fibonacci function: -} fib : recProg ℕ (λ _ → ℕ) fib zero = return 0 fib (suc zero) = return 1 fib (suc (suc n)) = call⟨ suc n ⟩ >>= λ r₁ → call⟨ n ⟩ >>= λ r₂ → return (r₁ + r₂) open Fib -- * Generic Bove-Capretta predicate generator: {- From a recProg, we can build a Bove-Capretta predicate that, intuitively, is merely the reification (as an inductive family) of the call-graph of the recursive program. -} module BC -- Let: {A : Set} {B : A → Set} (prog : recProg A B) where open RecMonad A B {- As it turns out, this call-graph is always a collapsible predicate: to "prove" this, we simply describe the Bove-Capretta predicate with a collapsible description Dom: -} dom : ∀{a} → RecMon (B a) → CDesc A dom (returnRec z) = `1 dom (callRec a rec) = `X a `× `Π (B a) λ b → dom (rec b) Dom : CFunc A Dom = CFunc.mk λ a → dom (prog a) {- Then, following the Bove-Capretta technique, we can run the (potentially, general-recursive) function "prog" by recursion over its call-graph (and, therefore, not over its argument a): -} mutual run : (a : A) → μ Dom a → B a run a (con domS) = run1 (prog a) (mapRun {p = prog a} domS) mapRun : ∀{a}{p : RecMon (B a)} → ⟦ dom p ⟧ (μ Dom) → ⟦ dom p ⟧ B mapRun {p = returnRec x} tt = tt mapRun {p = callRec a rec} (domA , domRec) = run a domA , λ b → mapRun {p = rec b} (domRec b) run1 : ∀{a} → (p : RecMon (B a)) → ⟦ dom p ⟧ B → B a run1 (returnRec b) tt = b run1 (callRec a rec) (b , domRec) = run1 (rec b) (domRec b) {- Note that we are *not* using the elements of μ Dom s in a computationally-relevant way: they are only here to convince Agda that the definition (trivially) terminates. [Question: could we use Agda's irrelevance modality to make that clear in this file?] In fact, we know for sure that these elements cannot be computationally-relevant: being collapsible, there is nothing in μ Dom to compute with! At run-time, Edwin would just ignore it. -} -- * Example: Gcd -- ** Naive implementation {- Naively, one could implement gcd as follows: gcd : (m n : ℕ) → ℕ gcd 0 n = n gcd m 0 = m gcd (suc m) (suc n) with m ≤? n gcd (suc m) (suc n) | yes p = gcd (suc m) (n ∸ m) gcd (suc m) (suc n) | no ¬p = gcd (m ∸ n) (suc n) But you need the 'Trust-me-I-am-a-doctor' flag to convince Agda that, well, you know what you're doing: {-# OPTIONS --no-termination-check #-} module Test where test1 : gcd 4 5 ≡ 1 test1 = refl test2 : gcd 30 35 ≡ 5 test2 = refl test3 : gcd 70 105 ≡ 35 test3 = refl -} -- ** Using Bove-Capretta {- Disclaimer: For the curious, check Data.Nat.GCD in Nisse's standard library for the "proper" way to implement GCD, purely by induction. Also, have a sip of Conor's 'Djinn, monotonic' for an introduction to the framework at work in Nisse's code. A (perhaps?) less elegant way to implement the GCD function consists in using the above Bove-Capretta construction. The benefit of this approach is that you don't need at least 2 Phds to make sense of it (it took me one, your mileage may vary). Applying our generic machinery to the recursive definition of gcd, we obtain the Bove-Capretta predicate: -} DomGCD : ℕ × ℕ → Set DomGCD (m , n) = μ (BC.Dom gcd) (m , n) {- And, still applying our generic machinery, we get that, for any two input numbers satisfying the Bove-Capretta predicate, we can compute their gcd: -} gcd-bove : (m n : ℕ) → DomGCD (m , n) → ℕ gcd-bove m n xs = BC.run gcd (m , n) xs -- *** GCD is general recursive: {- Now, we can get rid of that pesky DomGCD predicate by proving, after the fact, that our gcd function is indeed terminating. For that, we simply have to prove that DomGCD is inhabited for any input numbers m and n : -} gcd-wf : (m n : ℕ) → DomGCD (m , n) gcd-wf m n = build ([_⊗_] IndNat.<-rec-builder IndNat.<-rec-builder) (λ { (m , n) → DomGCD (m , n) }) (λ { (m , n) rec → con (ih m n rec) }) (m , n) where ih : ∀ x y → (IndNat.<-Rec ⊗ IndNat.<-Rec) DomGCD (x , y) → ⟦ BC.dom gcd (gcd (x , y)) ⟧ DomGCD ih zero y rec = tt ih (suc x) zero rec = tt ih (suc x) (suc y) rec with x ≤? y ih (suc x) (suc y) (rec-x , rec-y) | yes p = (rec-x (y ∸ x) (s≤′s (≤⇒≤′ (n∸m≤n x y)))) , (λ _ → tt) ih (suc x) (suc y) (rec-x , rec-y) | no ¬p = rec-y ((x ∸ y)) ((s≤′s (≤⇒≤′ (n∸m≤n y x)))) (suc y) , (λ _ → tt) {- And we get the desired gcd function: -} gcd' : (m n : ℕ) → ℕ gcd' m n = gcd-bove m n (gcd-wf m n) module TestGcd where test0 : gcd' 0 5 ≡ 5 test0 = refl test0' : gcd' 4 0 ≡ 4 test0' = refl test1 : gcd' 4 5 ≡ 1 test1 = refl test2 : gcd' 30 35 ≡ 5 test2 = refl test3 : gcd' 70 105 ≡ 35 test3 = refl -- * Example: Fibonacci {- The same goes for the Fibonacci function, so I'll be mercilessly brief. -} DomFib : ℕ → Set DomFib m = μ (BC.Dom fib) m fib-wf : (n : ℕ) → DomFib n fib-wf a = cRec (λ n → DomFib n) (λ n r → con (ih {n} r)) a where ih : ∀{n} → IndNat.CRec DomFib n → ⟦ BC.dom fib (fib n) ⟧ DomFib ih {zero} ih = tt ih {suc zero} ih = tt ih {suc (suc n)} (fib-sn , fib-n , xs) = fib-sn , λ n' → fib-n , λ _ → tt fib' : ℕ → ℕ fib' n = BC.run fib n (fib-wf n) module TestFib where fib'0 : fib' 0 ≡ 0 fib'0 = refl fib'1 : fib' 1 ≡ 1 fib'1 = refl fib'2 : fib' 2 ≡ 1 fib'2 = refl fib'3 : fib' 3 ≡ 2 fib'3 = refl fib'4 : fib' 4 ≡ 3 fib'4 = refl fib'5 : fib' 5 ≡ 5 fib'5 = refl -- * Collapse {- This is all very well but we've traded the freedom from termination checking for the burden of carrying Bove-Capretta around: how much of our foot do we have left? Well, in fact, once the dust settles, we should have as many toes as before and that's thanks to the "collapsibility" of the CDesc universe. In "Inductive Families Need Not Store Their Indices", Edwin Brady, Conor McBride, and James McKinna describe a *run-time* optimisation called "collapsing" (Section 6): An inductive family D : I → Set is *collapsible* if for every index i, if a, b : D i, then a ≡ b (extensionally) That is, the index i determines entirely the content of the inductive family. Put otherwise, the inductive family has no computational content, hence the name 'collapsible': morally, it collapses to a single element. Remark: In the lingo of Homotopy Type Theory, a collapsible type D : I → Set corresponds to a family of h-propositions, ie. we have: ∀ i → isProp(D i) That is: ∀ i → ∀ (x y : D i) → x ≡ y -} -- ** Example: ≤ relation (Section 6) data _≤`_ : ℕ → ℕ → Set where le0 : ∀{n} → 0 ≤` n leS : ∀{m n} → m ≤` n → suc m ≤` suc n -- This datatype is collapsible: ≤-collapsible : ∀{m n} → (a b : m ≤` n) → a ≡ b ≤-collapsible {zero} le0 le0 = refl ≤-collapsible {suc m} {zero} () b ≤-collapsible {suc m} {suc n} (leS a) (leS b) rewrite ≤-collapsible a b = refl -- ** CFunc describes collapsible datatypes : {- Assuming extensionality (by working in the Squash applicative ⊢_), we can prove (generically) that fixpoints of CDesc are indeed collapsible. Briefly, here is the Squash applicative: -} infixr 1 ⊢_ data ⊢_ {l : Level}(X : Set l) : Set l where pf : .X → ⊢ X Applicative⊢ : RawApplicative ⊢_ Applicative⊢ = record { pure = pf ; _⊛_ = _⊛_ } where _⊛_ : {A B : Set} → ⊢ (A → B) → ⊢ A → ⊢ B (pf f) ⊛ (pf a) = pf (f a) postulate extensionality : {A : Set}{B : A → Set}{f g : (a : A) → B a} → ((x : A) → ⊢ (f x ≡ g x)) → ⊢ (f ≡ g) -- Using this machinery we can prove that any family R is -- collapsible: CDesc-collapse : ∀{I i}{R} → (xs ys : μ R i) → ⊢ xs ≡ ys CDesc-collapse {I}{R = R} (con xs) (con ys) = cong con <$> help (CFunc.func R _) xs ys where open RawApplicative Applicative⊢ help : (D : CDesc I) → (xs ys : ⟦ D ⟧ (μ R)) → ⊢ xs ≡ ys help `0 () _ help `1 tt tt = pf refl help (`X i) (con xs₁) (con ys₁) = cong con <$> help (CFunc.func R i) xs₁ ys₁ help (D₁ `× D₂) (xs₁ , xs₂) (ys₁ , ys₂) = cong₂ _,_ <$> help D₁ xs₁ ys₁ ⊛ help D₂ xs₂ ys₂ help (`Π S T) f g = extensionality λ s → help (T s) (f s) (g s) {- Edwin's compiler should therefore be able to optimise away our Bove-Capretta predicates away (at run-time only!). -} -- * Conclusion: {- Having implemented gcd with a recursion oracle (and having faith in Edwin's optimiser), we are guaranteed that gcd suffers no run-time cost associated with the construction or consumption of the Bove-Capretta predicate we've generically constructed. Remark: This may be more than a fancy trick. In order to mark the accessibility predicates as 'computationally irrelevant', Coq users define their accessibility predicates in Prop. The system then checks that these definitions are 'singleton types', ie. have a single constructor (hey, that's our notion of 'collapsible', isn't it?). However, to be usable on the Set (computationally-relevant) side, Coq has to support the elimination of these 'singleton types' into Set. The benefit is that, being in Prop, the accessibility predicate is simply not extracted by Coq. The inconvenient is the loss of strong normalisation of the calculus (see Letouzey's PhD, 'L'elimination des singletons', p.61): we have to restrict ourselves to weak reductions, ie. no reduction can happen under a lambda. Using our more structural approach (extracting a class of datatypes that can be automatically ignored), we may be able to have an OTT-style Prop (where only ⊥ : Prop can be eliminated over) while paying no run-time cost for gcd's collapsible argument. That's a strongly normalising calculus for you, at no expense. -}