[Agda] help with inductive sized types

James Smith james.smith.69781 at gmail.com
Tue Aug 24 06:07:24 CEST 2021

```I'm trying to learn to use Sized Types to solve a simple non-termination
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210823/05bcbbba/attachment.html>
```