[Agda] help with inductive sized types

[James Smith]

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.

A small lambda toy with separate neutrals and values:

    data Type : Set where
      Nat : Type
      _⇒_ : Type → Type → Type

    data Value : List Type → Type → Set
    data Neutral : List Type → Type → Set where
      var : ∀ {Γ T} → T ∈ Γ → Neutral Γ T
      app : ∀ {Γ S T} → Neutral Γ (S ⇒ T) → Value Γ S → Neutral Γ T

    data Value where
      coerce : ∀ {Γ T} → Neutral Γ T → Value Γ T

    ⟦_⟧T : Type → Set
    ⟦ Nat ⟧T = ℕ
    ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T

    ⟦_⟧C : List Type → Set
    ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T

    {-# NON_TERMINATING #-}
    ⟦_⟧t : ∀ {Γ T} → Value Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T
    ⟦ (coerce (var (here px))) ⟧t  (fst , _) rewrite px = fst
    ⟦ (coerce (var (there x))) ⟧t  (_ , rest) = ⟦ (coerce (var x)) ⟧t rest
    ⟦ (coerce (app f x)) ⟧t  ctx = (⟦ coerce f ⟧t ctx) (⟦ x ⟧t ctx)

The final app clause is what causes a problem. A mutually recursive
function pair works fine:

    ⟦_⟧t-v : ∀ {Γ T} → Value Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T
    ⟦_⟧t-n : ∀ {Γ T} → Neutral Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T
    ⟦ (coerce n) ⟧t-v env = ⟦ n ⟧t-n env
    ⟦ (var (here px)) ⟧t-n  (fst , _) rewrite px = fst
    ⟦ (var (there x)) ⟧t-n  (_ , rest) = ⟦ var x ⟧t-n rest
    ⟦ (app f x) ⟧t-n  ctx = (⟦ f ⟧t-n ctx) (⟦ x ⟧t-v ctx)

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.

  module SizedExample where
    open import Data.Nat
    open import Data.List
    open import Data.List.Membership.Propositional
    open import Data.List.Membership.Propositional.Properties
    open import Data.List.Relation.Unary.Any
    open import Data.Product
    open import Data.Unit
    open import Data.Vec
    open import Function
    open import Relation.Binary.PropositionalEquality
    open import Size

    data Type : Set where
      Nat : Type
      _⇒_ : Type → Type → Type

    data Value : Size → List Type → Type → Set
    data Neutral : Size → List Type → Type → Set

    data Neutral where
      var : ∀ {i : Size} {Γ T} → T ∈ Γ → Neutral i Γ T
      app : ∀ {szf szx : Size} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szx
Γ S → Neutral ((↑ szf) ⊔ˢ szx) Γ T

    data Value where
      coerce : ∀ {sz : Size} {Γ T} → Neutral sz Γ T → Value sz Γ T

    ⟦_⟧T : Type → Set
    ⟦ Nat ⟧T = ℕ
    ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T

    ⟦_⟧C : List Type → Set
    ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T

    ⟦_⟧t : ∀ {sz Γ T} → Value sz Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T
    ⟦ (coerce (var (here px))) ⟧t (fst , _) rewrite px = fst
    ⟦ (coerce (var (there x))) ⟧t (_ , rest) = ⟦ (coerce (var x)) ⟧t rest
    ⟦_⟧t .{(↑ szf) ⊔ˢ szx} (coerce (app {szf} {szx} f x)) ctx = ⟦_⟧t {szf}
(coerce f) ctx (⟦_⟧t {szx} x ctx)

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.

A refactor to use Size< on parameters, instead of the max operator on the
result, works:

module SizedExample2 where
    open import Data.Nat
    open import Data.List
    open import Data.List.Membership.Propositional
    open import Data.List.Membership.Propositional.Properties
    open import Data.List.Relation.Unary.Any
    open import Data.Product
    open import Data.Unit
    open import Data.Vec
    open import Function
    open import Relation.Binary.PropositionalEquality
    open import Size

    data Type : Set where
      Nat : Type
      _⇒_ : Type → Type → Type

    data Value : Size → List Type → Type → Set
    data Neutral : Size → List Type → Type → Set

    data Neutral where
      var : ∀ {sz Γ T} → T ∈ Γ → Neutral sz Γ T
      app : ∀ {sz} {szf szx : Size< sz} {Γ S T} → Neutral szf Γ (S ⇒ T) →
Value szx Γ S → Neutral sz Γ T

    data Value where
      coerce : ∀ {sz Γ T} → Neutral sz Γ T → Value sz Γ T

    ⟦_⟧T : Type → Set
    ⟦ Nat ⟧T = ℕ
    ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T

    ⟦_⟧C : List Type → Set
    ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T

    ⟦_⟧t : ∀ {sz Γ T} → Value sz Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T
    ⟦ (coerce (var (here px))) ⟧t (fst , _) rewrite px = fst
    ⟦ (coerce (var (there x))) ⟧t (_ , rest) = ⟦ (coerce (var x)) ⟧t rest
    ⟦_⟧t (coerce (app f x)) ctx = ⟦ (coerce f) ⟧t ctx (⟦ x ⟧t ctx)


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.

Thanks in advance for any insight.

-James
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210823/05bcbbba/attachment.html>