终止检查的函子和单子实例

Question

这是几个月前another question 的后续。该问题与 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)

上下文是represented polymorphically using de Bruijn indices。 Try 的细节并不重要，因此我将类型留空，并简单地假设 ᵀ<$>，这是一个类似 fmap 的 try 操作。

我想做的是进行以下终止检查。这里给出的大小指数是我粗略的第一次尝试，但终止检查器仍然拒绝代码。

   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 终止检查器失败的代码。）

Answer 1

如果您将extend₁ 推广到extend′，您可以在不参考替换的情况下定义功能性，并且所有终止检查都很好：

extend′ : ∀ {Γ Γ′} → Γ ⇢ Γ′ → ∀ {Δ} → Γ ∷ʳ Δ ⇢ Γ′ ∷ʳ Δ
extend′ f (here  x) = here  x
extend′ f (there x) = there (f x)

_<$>_  : ∀ {ι} {Γ Γ′ : Type → Set}
         → Γ ⇢ Γ′
         → Term Γ {ι} ⇢ Term Γ′ {ι}

_*_    : ∀ {ι Γ Γ′}
         → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι})
         → Term Γ {ι} ⇢ Term Γ′ {ι}

extend : ∀ {ι Γ Γ′ A}
         → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι})
         → (Γ ∷ʳ A) ⇢ Term (Γ′ ∷ʳ A) {↑ ι}

-- Functoriality.
f <$> var x = var (f x)
f <$> fun e = fun (extend′ f <$> e)
f <$> match e as m =  match f <$> e as (_<$>_ (extend′ f) ᵀ<$> m)

-- Monadic bind, a.k.a. substitution.
θ * var x = θ x
θ * fun e = fun (extend θ * e)
θ * (match e as m) = match θ * e as (_*_ (extend θ) ᵀ<$> m)

-- Extend a substitution under a binder.
extend θ (here  x) = var (here x)
extend θ (there x) = there <$> θ x