Derivatives of data structures in Agda

Question

I am currently implementing derivatives of regular data structures, in Agda, as presented in the One-Hole Context paper by Conor McBride [5].

In implementing it straight out of the OHC paper, which has also been done by Löh & Magalhães [3,4], we are left with the ⟦_⟧ function highlighted in red, as Agda can't tell if the μ and I cases will terminate together. Löh & Magalhães made a comment of this in their repository.

Other papers have also included a similar implementation or definitions in their papers [7,8] but do not have a repo (at least I haven't been able to find it) [1,2,6], or they follow a different approach [9] in which μ is defined separately from Reg, ⟦_⟧, and derive (or dissection in their case), with no environment, and the operations are performed on a stack.

Using the {-# TERMINATING #-} or {-# NON_TERMINATING #-} flags is undesirable. Particularly, anything using ⟦_⟧ will not normalize, and thus I can't use this function to prove anything.

The implementation below is a slight modification to the OHC implementation. It removes weakening and substitution as part of the structural definition of Reg. Which, at first, makes ⟦_⟧ happy! But I find a similar problem when implementing derive -- Agda's termination checker is not happy with the μ case.

I haven't been successful at convincing Agda that derive terminates. I was wondering if anyone had successfully implemented derive with the signature derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n

The code below only shows some of the important pieces. I have included a gist with the rest of the definitions, which includes definitions of substitution and weakening and the derive that fails to terminate.

 -- Regular universe, multivariate.
 -- n defines the number of variables
 data Reg : ℕ → Set₁ where
   0′    : {n : ℕ} → Reg n
   1′    : {n : ℕ} → Reg n
   I     : {n : ℕ} → Fin n → Reg n 
   _⨁_  : {n : ℕ} → (l r : Reg n) → Reg n
   _⨂_  : {n : ℕ} → (l r : Reg n) → Reg n
   μ′    : {n : ℕ} → Reg (suc n)   → Reg n

 infixl 30 _⨁_
 infixl 40 _⨂_

 data Env : ℕ → Set₁ where
   []  : Env 0
   _,_ : {n : ℕ} → Reg n → Env n → Env (suc n)

 mutual
   ⟦_⟧ : {n : ℕ} → Reg n → Env n → Set
   ⟦ 0′ ⟧  _ = ⊥
   ⟦ 1′ ⟧  _ = ⊤
   ⟦ I zero  ⟧   (X , Xs) = ⟦ X ⟧  Xs   
   ⟦ I (suc n) ⟧ (X , Xs) = ⟦ I n ⟧ Xs  
   ⟦ L ⨁ R ⟧ Xs = ⟦ L ⟧ Xs ⊎ ⟦ R ⟧ Xs
   ⟦ L ⨂ R ⟧ Xs = ⟦ L ⟧ Xs × ⟦ R ⟧ Xs
   ⟦  μ′ F  ⟧ Xs =  μ F Xs

   data μ {n : ℕ} (F : Reg (suc n)) (Xs : Env n) : Set where
     ⟨_⟩ : ⟦ F ⟧ (μ′ F , Xs) → μ F Xs

 infixl 50 _[_]
 infixl 50 ^_

 _[_]  : {n : ℕ} → Reg (suc n) → Reg n → Reg n
 ^_    : {n : ℕ} → Reg n → Reg (suc n)

 derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n
 derive = {!!}

Complete code: https://pastebin.com/awr9Bc0R

[1] Abbott, M., Altenkirch, T., Ghani, N., and McBride, C. (2003). Derivatives of con- tainers. In International Conference on Typed Lambda Calculi and Applications, pages 16–30. Springer.

[2] Abbott, M., Altenkirch, T., McBride, C., and Ghani, N. (2005). δ for data: Differ- entiating data structures. Fundamenta Informaticae, 65(1-2):1–28.

[3] Löh, A. & Magalhães JP (2011). Generic Programming with Indexed Functors. In Proceedings of the seventh ACM SIGPLAN Workshop on Generic Programming (WGP'11).

[4] Magalhães JP. & Löh, A. (2012) A Formal Comparison of Approaches to Datatype-Generic Programming. In Proceedings Fourth Workshop on Mathematically Structured Functional Programming (MSFP '12).

[5] McBride, C. (2001). The derivative of a regular type is its type of one-hole contexts. Unpublished manuscript, pages 74–88.

[6] McBride, C. (2008). Clowns to the left of me, jokers to the right (pearl): dissecting data structures. In ACM SIGPLAN Notices, volume 43, pages 287–295. ACM.

[7] Morris, P., Altenkirch, T., & McBride, C. (2004, December). Exploring the regular tree types. In International Workshop on Types for Proofs and Programs (pp. 252-267). Springer, Berlin, Heidelberg.

[8] Sefl, V. (2019). Performance analysis of zippers. arXiv preprint arXiv:1908.10926.

[9] Tome Cortinas, C. and Swierstra, W. (2018). From algebra to abstract machine: a verified generic construction. In Proceedings of the 3rd ACM SIGPLAN Interna- tional Workshop on Type-Driven Development, pages 78–90. ACM.

Answer 1

The definition of derive terminates, you just adapted the code from the repo incorrectly. If derive is only called on F in the μ′ F case, that's clearly structural. In the code sample you tried to recurse on ^ (F [ μ′ F ]) instead.

derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n
derive i 0′ = 0′
derive i 1′ = 0′
derive i (I j) with i ≟ j
derive i (I j) | yes refl = 1′
...            | no _     = 0′
derive i (L ⨁ R) = derive i L ⨁ derive i R
derive i (L ⨂ R) = (derive i L ⨂ R) ⨁ (L ⨂ derive i R)
derive i (μ′ F) = μ′ (    (^ (derive (suc i) F [ μ′ F ]))
                       ⨁ (^ (derive zero F [ μ′ F ])) ⨂ I zero)

I also suggest to adjust Reg as follows, since n as index is unnecessary, and Set₁ as well.

data Reg (n : ℕ) : Set where
  0′    : Reg n
  1′    : Reg n
  I     : Fin n → Reg n
  _⨁_  : (l r : Reg n) → Reg n
  _⨂_  : (l r : Reg n) → Reg n
  μ′    : Reg (suc n)  → Reg n