[Agda] help with inductive sized types

[Andreas Abel]

The upper-bound operator for sizes is very experimental and should not 
be used.  Its implementation is very incomplete.

It works if you give both arguments of `app` the same upper bound `szf`:


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

   module SizedExample where
     open import Data.Nat.Base
     open import Data.List.Base
     open import Data.List.Membership.Propositional
     open import Data.List.Relation.Unary.Any using (here; there)
     open import Data.Product using (_×_; _,_)
     open import Data.Unit
     open import Function.Base
     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 : Size} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szf 
Γ S → Neutral (↑ szf) Γ 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 = foldr _×_ ⊤ ∘ 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)} (coerce (app {szf} f x)) ctx = ⟦_⟧t {szf} (coerce 
f) ctx (⟦_⟧t {szf} x ctx)


On 2021-08-25 04:30, Jonathan Chan wrote:
> The only problem I can spot is that szx is /not/ strictly smaller 
> thanmax(szf + 1, szx), so the size of the type of app has to be either ↑ 
> (szf ⊔ˢ szx) or ↑ szf ⊔ˢ ↑ szx. But even then, with the app case of ⟦_⟧t 
> having either of these sizes, it still doesn't pass the termination 
> check, so I'm not sure what's going there, because I'm pretty confident 
> that szf and szx are both strictly smaller than ↑ (szf ⊔ˢ szx) and ↑ szf 
> ⊔ˢ ↑ szx.
> 
> It could just be that this isn't something that the size checker can 
> verify. If you pick the first version — that is,
> 
> 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
> 
> Then you could "raise" the size of the recursive arguments of ⟦_⟧t from 
> szf and szx both to (szf ⊔ˢ szx), so that the app branch is
> 
> ⟦_⟧t .{↑ (szf ⊔ˢ szx)} (coerce (app {szf} {szx} f x)) ctx = ⟦_⟧t {szf ⊔ˢ 
> szx} (coerce f) ctx (⟦_⟧t {szf ⊔ˢ szx} x ctx)
> 
> I don't remember if Agda has sized subtyping (I mean, probably, given 
> that this passes termination checking), but for instance (coerce f) has 
> type (Value szf Γ T), which would need to be a subtype of (Value (szf ⊔ˢ 
> szx) Γ T), which follows from (szf ≤ szf ⊔ˢ szx), and finally (szf ⊔ˢ 
> szx ≤ ↑ (szf ⊔ˢ szx)) for termination checking.
> 
> The original version without the trick just needs (szf ≤ ↑ (szf ⊔ˢ szx)) 
> and (szx ≤ ↑ (szf ⊔ˢ szx)) though, which holds by transitivity. Is Agda 
> unable to check transitive subsizing relations like that?
> 
> On Mon, 23 Aug 2021 at 21:07, James Smith <james.smith.69781 at gmail.com 
> <mailto:james.smith.69781 at gmail.com>> wrote:
>  >
>  > 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
>  >
>  >
>  > _______________________________________________
>  > Agda mailing list
>  > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>  > https://lists.chalmers.se/mailman/listinfo/agda 
> <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>