Termination-checking substitution via (monadic) join and fmap

Question

I'm using sized types, and have a substitution function for typed terms which termination-checks if I give a definition directly, but not if I factor it via (monadic) join and fmap.

{-# OPTIONS --sized-types #-}

module Subst where

   open import Size

To show the problem, it's enough to have unit and sums. I have data types of Trie and Term, and I use tries with a codomain of Term inside Term, as part of the elimination form for sums.

   data Type : Set where
      𝟏 : Type
      _+_ : Type → Type → Type

   postulate Cxt : Set → Set

   -- Every value in the trie is typed in a context obtained by extending Γ.
   data Trie (A : Cxt Type → Set) : {ι : Size} → Type → Cxt Type → Set where
      〈〉 : ∀ {ι Γ} → A Γ → Trie A {↑ ι} 𝟏 Γ
     〔_,_〕 : ∀ {ι τ₁ τ₂ Γ} → 
              Trie A {ι} τ₁ Γ → Trie A {ι} τ₂ Γ → Trie A {↑ ι} (τ₁ + τ₂) Γ

   -- The elimination form for + types is a trie whose values are terms.
   data Term (A : Cxt Type → Type → Set) : {ι : Size} → 
             Cxt Type → Type → Set where
      var : ∀ {ι Γ τ} → A Γ τ → Term A {↑ ι} Γ τ
      inl : ∀ {ι Γ τ₁ τ₂} → Term A {ι} Γ τ₁ → Term A {↑ ι} Γ (τ₁ + τ₂)
      match_as_ : ∀ {ι Γ τ τ′} → Term A {ι} Γ τ → 
                  Trie (λ Γ → Term A {ι} Γ τ′) {ι} τ Γ  → Term A {↑ ι} Γ τ′

Now, if I define substitution into terms directly (mutually with substitution into tries with codomain Term), then the definition termination-checks, even without size indices.

   -- Define substitution directly.
   _*_ : ∀ {A Γ Γ′ τ} → (∀ {τ} → A Γ τ → Term A Γ′ τ) → Term A Γ τ → Term A Γ′ τ
   _*ᵀ_ : ∀ {A Γ Γ′ τ τ′} → (∀ {τ} → A Γ τ → Term A Γ′ τ) →
          Trie (λ Γ → Term A Γ τ) τ′ Γ → Trie (λ Γ → Term A Γ τ) τ′ Γ′

   θ * var x = θ x
   θ * inl e = inl (θ * e)
   θ * (match e as κ) = match (θ * e) as (θ *ᵀ κ)

   θ *ᵀ 〈〉 x = 〈〉 (θ * x)
   θ *ᵀ 〔 κ₁ , κ₂ 〕 = 〔 θ *ᵀ κ₁ , θ *ᵀ κ₂ 〕

However, Trie and Term are functors, so it's natural to want to define substitution in terms of <$> (fmap) and join, where the latter collapses a term of terms into a term. Note that <$> and its counterpart for tries is size-preserving, and indeed we need to use size indices which reflect this for Agda to be satisfied that it terminates.

   -- Size-preserving fmap.
   _<$>ᵀ_ : ∀ {ι 𝒂 τ Γ Γ′} {A B : Cxt Type → Set 𝒂} → 
            (A Γ → B Γ′) → Trie A {ι} τ Γ → Trie B {ι} τ Γ′
   f <$>ᵀ (〈〉 x) = 〈〉 (f x)
   f <$>ᵀ 〔 σ₁ , σ₂ 〕 = 〔 f <$>ᵀ σ₁ , f <$>ᵀ σ₂ 〕

   _<$>_ : ∀ {ι A B Γ Γ′ τ} → 
           (∀ {τ} → A Γ τ → B Γ′ τ) → Term A {ι} Γ τ → Term B {ι} Γ′ τ
   f <$> var x = var (f x)
   f <$> inl e = inl (f <$> e)
   f <$> match e as κ = match f <$> e as ((λ e → f <$> e) <$>ᵀ κ)

   -- Monadic multiplication.
   join : ∀ {A Γ τ} → Term (Term A) Γ τ → Term A Γ τ
   join (var e) = e
   join (inl e) = inl (join e)
   join (match e as κ) = match join e as (join <$>ᵀ κ)

   -- Now substitution is easily defined in terms of join and fmap.
   _*′_ : ∀ {A Γ Γ′ τ} → (∀ {τ} → A Γ τ → Term A Γ′ τ) → Term A Γ τ → Term A Γ′ τ
   θ *′ e = join (θ <$> e)

Unfortunately join does not termination-check, and I'm not sure it's possible to use size indices to convince Agda that it does. Intuitively, it's clear enough that if you have a tree with a maximum depth of ι, and you replace its leaves with trees with a maximum depth of ι', you obtain a tree with a maximum depth of (ι + ι'). But I don't think this is the kind of thing you can establish with sized types or whether it would even help if you could. Note that without the mutual recursion into tries via join <$>ᵀ, the function termination-checks fine.

Is there a way to have this mutually recursive version of join termination-check, or am I stuck with writing substitution explicitly?

Answer 1

Give join the following type:

join : ∀ {ι A Γ τ} → Term (Term A) {ι} Γ τ → Term A Γ τ

(from gallais' comment above).