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.

-}