[Agda] help with inductive sized types

[Jonathan Chan]

The only problem I can spot is that szx is *not* strictly smaller than
max(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>
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
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210824/8e304577/attachment.html>