# [Agda] help with inductive sized types

Andreas Abel andreas.abel at ifi.lmu.de
Wed Aug 25 13:46:32 CEST 2021

```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
>
```