Это следует за другим вопросом, заданным несколько месяцев назад. Проблема связана с проверкой завершения в Agda с использованием размерных типов.
Вот преамбула:
{-# OPTIONS --sized-types #-}
module Term where
open import Data.Empty
open import Function
open import Relation.Binary.PropositionalEquality
open import Size
data Type : Set where
???? : Type
_+_ _⇾_ : Type → Type → Type
Cxt : Set₁
Cxt = Type → Set
-- Adapted from "Names for free: polymorphic views of names and binders",
-- by Bernardy and Pouillard.
data _∷ʳ_ (Γ : Cxt) (V : Cxt) (A : Type) : Set where
here : V A → (Γ ∷ʳ V) A
there : Γ A → (Γ ∷ʳ V) A
-- A renaming from Γ to Γ′.
_⇢_ : Cxt → Cxt → Set
Γ ⇢ Γ′ = ∀ {A} → Γ A → Γ′ A
infixr 19 _⇢_
-- Extend a renaming under a binder.
extend₁ : ∀ {Γ Γ′} → Γ ⇢ Γ′ → ∀ {A} → Γ ∷ʳ (_≡_ A) ⇢ Γ′ ∷ʳ (_≡_ A)
extend₁ f (here x) = here x
extend₁ f (there x) = there (f x)
data Trie (Γs : Cxt → Cxt) (C : Type) : {ι : Size} → Type → Set where
postulate
_ᵀ<$>_ : ∀ {Γs Γs′ : Cxt → Cxt} →
(∀ {C Γ} → (Γs Γ C → Γs′ Γ C)) →
∀ {ι C} → (λ A → Trie Γs A {ι} C) ⇢ (λ A → Trie Γs′ A {ι} C)
Контексты представлены полиморфно с использованием индексов де Брейна. Детали попыток не важны, поэтому я оставил тип пустым и просто постулирую ᵀ<$>
, операцию, подобную fmap, для попыток.
Я бы хотел провести следующую проверку завершения. Приведенные здесь индексы размера - это моя грубая первая попытка, но программа проверки завершения все еще отклоняет код.
data Term (Γ : Type → Set) : {ι : Size} → Type → Set where
var : ∀ {ι A} → Γ A → Term Γ {↑ ι} A
match_as_ : ∀ {ι A A′} → Term Γ {ι} A →
Trie (λ Γ′ → Term (Γ ∷ʳ Γ′) {ι}) A′ A → Term Γ {↑ ι} A′
fun : ∀ {ι A B} → Term (Γ ∷ʳ (_≡_ A)) {ι} B → Term Γ {↑ ι} (A ⇾ B)
_<$>_ : ∀ {ι} {Γ Γ′ : Type → Set} → Γ ⇢ Γ′ → Term Γ {ι} ⇢ Term Γ′ {ι}
_*_ : ∀ {ι Γ Γ′} → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι}) → Term Γ {ι} ⇢ Term Γ′ {ι}
extend : ∀ {ι Γ Γ′ A} → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι}) →
(Γ ∷ʳ A) ⇢ Term (Γ′ ∷ʳ A) {↑ ι}
-- Functoriality.
f <$> var x = var (f x)
f <$> match e as m = match f <$> e as (_*_ (extend (var ∘ f)) ᵀ<$> m)
f <$> fun e = fun (extend₁ f <$> e)
-- Monadic bind, a.k.a. substitution.
θ * var x = θ x
θ * (match e as m) = match θ * e as (_*_ (extend θ) ᵀ<$> m)
θ * fun e = fun (extend θ * e)
-- Extend a substitution under a binder.
extend θ (here x) = var (here x)
extend θ (there x) = there <$> θ x
Как мне исправить свои индексы? Я также был бы признателен за помощь в понимании проблемы. Например, я предполагаю, что имея
∀ {ι} → Γ ⇢ Term Γ′ {↑ ι}
поскольку тип подстановки может быть проблематичным из-за ↑, но мне кажется, это нужно, чтобы позволить var ∘ f
быть подходящим аргументом для extend
. (Также любопытно, почему это не приводит к несогласованным ограничениям, а скорее к коду, который не работает с обычным средством проверки завершения Agda.)