foo.agda

module Test498 where

open import Agda.Builtin.Equality
open import Agda.Builtin.String
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open Agda.Primitive renaming (Set to Type)

_×_ : ∀ {l l'} → Type l → Type l' → Type _
A × B = Σ A λ _ → B

record Lift {l} l' (A : Type l) : Type (l ⊔ l') where
  constructor lift
  field lower : A

open Lift

data Box (A : Type) : Type where
  box : (x : A) -> Box A
  wrap : (y : Box A) -> Box A

data Boxed : Type where
  nobox : Boxed
  bbox : (b : Box Boxed) -> Boxed

postulate
  e : Boxed ≡ Boxed

module _ {l l'} (P : Boxed → Type l) (Q : Box Boxed → Type l') where
  Below1 : Boxed → Type (l ⊔ l')
  Below2 : Box Boxed → Type (l ⊔ l')

  Below1 nobox    = Lift _ ⊤
  Below1 (bbox b) = Q b × Below2 b

  Below2 (box x)  = P x × Below1 x
  Below2 (wrap x) = Q x × Below2 x

  Elim : P nobox → (∀ b → Q b → P (bbox b)) → (∀ x → P x → Q (box x)) → (∀ x → Q x → Q (wrap x)) → ((∀ x → P x) × (∀ x → Q x))
  Elim pno pbb qbx qwr = go1 , go2 where
    go1 : ∀ x → P x
    go2 : ∀ x → Q x

    go1 nobox    = pno
    go1 (bbox b) = pbb b (go2 b)

    go2 (box x)  = qbx x (go1 x)
    go2 (wrap x) = qwr x (go2 x)

Fix
  : ∀ {l l'} (P : Boxed → Type l) (Q : Box Boxed → Type l')
  → (∀ x → Below1 P Q x → P x) → (∀ x → Below2 P Q x → Q x)
  → ((∀ x → P x) × (∀ x → Q x))
Fix P Q m1 m2 =
  let
    (fix1 , fix2) = Elim (λ b → P b × Below1 P Q b) (λ b → Q b × Below2 P Q b)
      (m1 nobox (lift tt) , lift tt)
      (λ b z → m1 (bbox b) z , z)
      (λ x z → m2 (box x) z , z)
      (λ x z → m2 (wrap x) z , z)
  in (λ a → fix1 a .fst) , λ a → fix2 a .fst

data Label : Type where
  lloop  : Boxed     → Label
  lweird : Box Boxed → Label

record Labelled {l} (s : Label) (A : Type l) : Type l where
  constructor return
  field call : A

open Labelled

J : ∀ {l l'} {A : Type l} {x : A} (P : (y : A) → x ≡ y → Type l') → P x refl → ∀ {y} p → P y p
J P pr refl = pr

loop-weird
  : ((x : Boxed)     → Labelled (lloop x) Boxed)
  × ((x : Box Boxed) → Labelled (lweird x) Boxed)
loop-weird = Fix (λ _ → _) (λ _ → _)
  -- cases for loop
  (λ { nobox    mtree        → return nobox
     ; (bbox b) (weirdb , _) → return (bbox (box (weirdb .call)))
     })

  -- cases for weird
  (λ { (box x)  (loopx  , mtree) → return (loopx .call)
     ; (wrap x) mtree →
        let
          rec-here : Box Boxed → Type
          rec-here = Below2 (λ z → Labelled (lloop z) Boxed) (λ z → Labelled (lweird z) Boxed)
        in return do
          -- inline side2
          J (λ A _ → (arg : Box A) (rec : rec-here (wrap {! arg  !})) → Boxed)
            --                     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
            -- this argument represents something like "the capabilities
            -- for making a recursive call at the current point"
            -- outside the J, projecting (mtree .fst) would correspond
            -- to defining
            --    weird (wrap x) = weird x
            --
            -- passing *the entire memo-tree* implements the idea that
            -- intermediate calls in a cycle like
            --   f x → g x → h x
            -- can *preserve* the size of the arguments as long as the
            -- overall cycle is still decreasing
            --
            -- we *want* to make a recursive call
            --   weird (wrap y) → side2 e y → weird y (== weird (subst Id e y), problem!).
            -- but what justifies preserving the memo tree for this recursive program?
            --    we can't fill in ?0 := arg in the motive above because arg : Box A ≠ Box Boxed.
            -- i believe the insight here is that we can only think of
            -- the structurally-smaller relation as a proxy for
            -- projecting from a memo tree *if the parameters do not
            -- change*. the shape of the memo tree depends on the
            -- parameters.
            --
            -- what if we pass only the recursive call? well, if we set
            -- the labels aside¹, passing the recursive call instead of
            -- the memo tree would sort-of be equivalent to defining
            --    side2 _ y := weird y
            -- which is fine.

            -- ¹ mtree .fst : Labelled (lweird x) Boxed, but we want a Labelled (lweird arg) Boxed, which also fails.
            -- are the labels fundamental to this approach?
            -- Conor introduced them because she uses it to infer what
            -- component of the memotree corresponds to each call.
            -- that's sort of what i'm doing, too, but i added them so i
            -- don't get confused.
            (λ x c → c .fst .call)
            e x mtree
     })

mutual
  weird : (x : Box Boxed) -> Boxed
  loop : Boxed -> Boxed

  side2 : ∀ {A} (e' : A ≡ Boxed) (x : Box A) -> Boxed

  weird (box x) = loop x
  weird (wrap y) = side2 e y
  loop nobox = nobox
  loop (bbox n) = bbox (box (weird n))

  side2 refl x = weird x