<div dir="ltr">I'm trying to learn to use Sized Types to solve a simple non-termination issue. After reading a couple papers (MiniAgda, Equational Reasoning about Formal Languages in Coalgebraic Style) and everything I could find online, I was still confused. I've found a solution that works, but I don't know why my first attempt didn't work. Would love to learn the insight I am missing.<div><br></div><div>A small lambda toy with separate neutrals and values:</div><div><br></div><div> <font face="monospace">   data Type : Set where <br>      Nat : Type <br>      _⇒_ : Type → Type → Type <br>    <br>    data Value : List Type → Type → Set<br>    data Neutral : List Type → Type → Set where <br>      var : ∀ {Γ T} → T ∈ Γ → Neutral Γ T<br>      app : ∀ {Γ S T} → Neutral Γ (S ⇒ T) → Value Γ S → Neutral Γ T <br>  <br>    data Value where <br>      coerce : ∀ {Γ T} → Neutral Γ T → Value Γ T <br>  <br>    ⟦_⟧T : Type → Set <br>    ⟦ Nat ⟧T = ℕ <br>    ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T <br>  <br>    ⟦_⟧C : List Type → Set <br>    ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T<br>  <br>    {-# NON_TERMINATING #-}<br>    ⟦_⟧t : ∀ {Γ T} → Value Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T <br>    ⟦ (coerce (var (here px))) ⟧t  (fst , _) rewrite px = fst<br>    ⟦ (coerce (var (there x))) ⟧t  (_ , rest) = ⟦ (coerce (var x)) ⟧t rest<br>    ⟦ (coerce (app f x)) ⟧t  ctx = (⟦ coerce f ⟧t ctx) (⟦ x ⟧t ctx)<br></font></div><div><br></div><div>The final app clause is what causes a problem. A mutually recursive function pair works fine:</div><div><br></div><div><font face="monospace">    ⟦_⟧t-v : ∀ {Γ T} → Value Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T <br>    ⟦_⟧t-n : ∀ {Γ T} → Neutral Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T <br>    ⟦ (coerce n) ⟧t-v env = ⟦ n ⟧t-n env<br>    ⟦ (var (here px)) ⟧t-n  (fst , _) rewrite px = fst<br>    ⟦ (var (there x)) ⟧t-n  (_ , rest) = ⟦ var x ⟧t-n rest<br>    ⟦ (app f x) ⟧t-n  ctx = (⟦ f ⟧t-n ctx) (⟦ x ⟧t-v ctx)  </font><br></div><div><br></div><div>But I want the excuse to learn how to apply Sized Types, so I take a crack at getting rid of NON_TERMINATING by threading a Size index through everything.</div><div><br></div> <font face="monospace"> module SizedExample where <br>    open import Data.Nat <br>    open import Data.List<br>    open import Data.List.Membership.Propositional<br>    open import Data.List.Membership.Propositional.Properties<br>    open import Data.List.Relation.Unary.Any<br>    open import Data.Product<br>    open import Data.Unit<br>    open import Data.Vec<br>    open import Function<br>    open import Relation.Binary.PropositionalEquality<br>    open import Size<br>  <br>    data Type : Set where <br>      Nat : Type <br>      _⇒_ : Type → Type → Type <br>    <br>    data Value : Size → List Type → Type → Set<br>    data Neutral : Size → List Type → Type → Set <br><br>    data Neutral where<br>      var : ∀ {i : Size} {Γ T} → T ∈ Γ → Neutral i Γ T <br>      app : ∀ {szf szx : Size} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szx Γ S → Neutral ((↑ szf) ⊔ˢ szx) Γ T <br>  <br>    data Value where <br>      coerce : ∀ {sz : Size} {Γ T} → Neutral sz Γ T → Value sz Γ T <br>  <br>    ⟦_⟧T : Type → Set <br>    ⟦ Nat ⟧T = ℕ <br>    ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T <br>  <br>    ⟦_⟧C : List Type → Set <br>    ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T<br><br>    ⟦_⟧t : ∀ {sz Γ T} → Value sz Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T <br>    ⟦ (coerce (var (here px))) ⟧t (fst , _) rewrite px = fst<br>    ⟦ (coerce (var (there x))) ⟧t (_ , rest) = ⟦ (coerce (var x)) ⟧t rest<br></font><div><font face="monospace">    ⟦_⟧t .{(↑ szf) ⊔ˢ szx} (coerce (app {szf} {szx} f x)) ctx = ⟦_⟧t {szf} (coerce f) ctx (⟦_⟧t {szx} x ctx)  </font></div><div>  </div><div>The termination checker rejects the last line. But I don't see why. It looks to me like there's enough information there to see szf and szx are each smaller than their max to let those calls go through. I also tried giving extra headroom for szf in case that helped, but that didn't work either.</div><div><br></div><div>A refactor to use Size< on parameters, instead of the max operator on the result, works: </div><div><br></div><div><font face="monospace">module SizedExample2 where <br>    open import Data.Nat <br>    open import Data.List<br>    open import Data.List.Membership.Propositional<br>    open import Data.List.Membership.Propositional.Properties<br>    open import Data.List.Relation.Unary.Any<br>    open import Data.Product<br>    open import Data.Unit<br>    open import Data.Vec<br>    open import Function<br>    open import Relation.Binary.PropositionalEquality<br>    open import Size<br>  <br>    data Type : Set where <br>      Nat : Type <br>      _⇒_ : Type → Type → Type <br>    <br>    data Value : Size → List Type → Type → Set<br>    data Neutral : Size → List Type → Type → Set <br><br>    data Neutral where<br>      var : ∀ {sz Γ T} → T ∈ Γ → Neutral sz Γ T <br>      app : ∀ {sz} {szf szx : Size< sz} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szx Γ S → Neutral sz Γ T <br>  <br>    data Value where <br>      coerce : ∀ {sz Γ T} → Neutral sz Γ T → Value sz Γ T <br>  <br>    ⟦_⟧T : Type → Set <br>    ⟦ Nat ⟧T = ℕ <br>    ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T <br>  <br>    ⟦_⟧C : List Type → Set <br>    ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T<br><br>    ⟦_⟧t : ∀ {sz Γ T} → Value sz Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T <br>    ⟦ (coerce (var (here px))) ⟧t (fst , _) rewrite px = fst<br>    ⟦ (coerce (var (there x))) ⟧t (_ , rest) = ⟦ (coerce (var x)) ⟧t rest<br>    ⟦_⟧t (coerce (app f x)) ctx = ⟦ (coerce f) ⟧t ctx (⟦ x ⟧t ctx)</font><br></div><div><br></div><div><br></div><div>That makes me suspicious this is like a Size version of needing to avoid computed values in the result position of constructors, but I'm not really sure why the version with the max operator didn't work.</div><div><br></div><div>Thanks in advance for any insight.</div><div><br></div><div>-James</div><div><br></div><div><br></div></div>