[Agda] help with inductive sized types
James Smith
james.smith.69781 at gmail.com
Fri Aug 27 17:23:53 CEST 2021
Thank you all! This has been instructive.
On Wed, Aug 25, 2021 at 4:46 AM Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:
> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210827/4241f776/attachment.html>
More information about the Agda
mailing list