<div dir="ltr">Thank you all! This has been instructive. </div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Aug 25, 2021 at 4:46 AM Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The upper-bound operator for sizes is very experimental and should not <br>
be used.  Its implementation is very incomplete.<br>
<br>
It works if you give both arguments of `app` the same upper bound `szf`:<br>
<br>
<br>
   {-# OPTIONS --sized-types #-}<br>
<br>
   module SizedExample where<br>
     open import Data.Nat.Base<br>
     open import Data.List.Base<br>
     open import Data.List.Membership.Propositional<br>
     open import Data.List.Relation.Unary.Any using (here; there)<br>
     open import Data.Product using (_×_; _,_)<br>
     open import Data.Unit<br>
     open import Function.Base<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 : Size} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szf <br>
Γ S → Neutral (↑ szf) Γ 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 = foldr _×_ ⊤ ∘ 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 .{(↑ szf)} (coerce (app {szf} f x)) ctx = ⟦_⟧t {szf} (coerce <br>
f) ctx (⟦_⟧t {szf} x ctx)<br>
<br>
<br>
On 2021-08-25 04:30, Jonathan Chan wrote:<br>
> The only problem I can spot is that szx is /not/ strictly smaller <br>
> thanmax(szf + 1, szx), so the size of the type of app has to be either ↑ <br>
> (szf ⊔ˢ szx) or ↑ szf ⊔ˢ ↑ szx. But even then, with the app case of ⟦_⟧t <br>
> having either of these sizes, it still doesn't pass the termination <br>
> check, so I'm not sure what's going there, because I'm pretty confident <br>
> that szf and szx are both strictly smaller than ↑ (szf ⊔ˢ szx) and ↑ szf <br>
> ⊔ˢ ↑ szx.<br>
> <br>
> It could just be that this isn't something that the size checker can <br>
> verify. If you pick the first version — that is,<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 <br>
> Γ S → Neutral (↑ (szf ⊔ˢ szx)) Γ T<br>
> <br>
> Then you could "raise" the size of the recursive arguments of ⟦_⟧t from <br>
> szf and szx both to (szf ⊔ˢ szx), so that the app branch is<br>
> <br>
> ⟦_⟧t .{↑ (szf ⊔ˢ szx)} (coerce (app {szf} {szx} f x)) ctx = ⟦_⟧t {szf ⊔ˢ <br>
> szx} (coerce f) ctx (⟦_⟧t {szf ⊔ˢ szx} x ctx)<br>
> <br>
> I don't remember if Agda has sized subtyping (I mean, probably, given <br>
> that this passes termination checking), but for instance (coerce f) has <br>
> type (Value szf Γ T), which would need to be a subtype of (Value (szf ⊔ˢ <br>
> szx) Γ T), which follows from (szf ≤ szf ⊔ˢ szx), and finally (szf ⊔ˢ <br>
> szx ≤ ↑ (szf ⊔ˢ szx)) for termination checking.<br>
> <br>
> The original version without the trick just needs (szf ≤ ↑ (szf ⊔ˢ szx)) <br>
> and (szx ≤ ↑ (szf ⊔ˢ szx)) though, which holds by transitivity. Is Agda <br>
> unable to check transitive subsizing relations like that?<br>
> <br>
> On Mon, 23 Aug 2021 at 21:07, James Smith <<a href="mailto:james.smith.69781@gmail.com" target="_blank">james.smith.69781@gmail.com</a> <br>
> <mailto:<a href="mailto:james.smith.69781@gmail.com" target="_blank">james.smith.69781@gmail.com</a>>> wrote:<br>
>  ><br>
>  > I'm trying to learn to use Sized Types to solve a simple <br>
> non-termination issue. After reading a couple papers (MiniAgda, <br>
> Equational Reasoning about Formal Languages in Coalgebraic Style) and <br>
> everything I could find online, I was still confused. I've found a <br>
> solution that works, but I don't know why my first attempt didn't work. <br>
> Would love to learn the insight I am missing.<br>
>  ><br>
>  > A small lambda toy with separate neutrals and values:<br>
>  ><br>
>  >     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 <br>
> rest<br>
>  >     ⟦ (coerce (app f x)) ⟧t  ctx = (⟦ coerce f ⟧t ctx) (⟦ x ⟧t ctx)<br>
>  ><br>
>  > The final app clause is what causes a problem. A mutually recursive <br>
> function pair works fine:<br>
>  ><br>
>  >     ⟦_⟧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)<br>
>  ><br>
>  > But I want the excuse to learn how to apply Sized Types, so I take a <br>
> crack at getting rid of NON_TERMINATING by threading a Size index <br>
> through everything.<br>
>  ><br>
>  >   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) → <br>
> 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>
>  >     ⟦_⟧t .{(↑ szf) ⊔ˢ szx} (coerce (app {szf} {szx} f x)) ctx = ⟦_⟧t <br>
> {szf} (coerce f) ctx (⟦_⟧t {szx} x ctx)<br>
>  ><br>
>  > The termination checker rejects the last line. But I don't see why. <br>
> It looks to me like there's enough information there to see szf and szx <br>
> are each smaller than their max to let those calls go through. I also <br>
> tried giving extra headroom for szf in case that helped, but that didn't <br>
> work either.<br>
>  ><br>
>  > A refactor to use Size< on parameters, instead of the max operator on <br>
> the result, works:<br>
>  ><br>
>  > 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 ⇒ <br>
> 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)<br>
>  ><br>
>  ><br>
>  > That makes me suspicious this is like a Size version of needing to <br>
> avoid computed values in the result position of constructors, but I'm <br>
> not really sure why the version with the max operator didn't work.<br>
>  ><br>
>  > Thanks in advance for any insight.<br>
>  ><br>
>  > -James<br>
>  ><br>
>  ><br>
>  > _______________________________________________<br>
>  > Agda mailing list<br>
>  > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
>  > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a> <br>
> <<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>><br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
</blockquote></div>