merge - 合并具有大小类型的排序列表

Question

假设我们有一个排序列表的数据类型，带有与证明无关的排序见证。我们将使用 Agda 的实验性大小类型特性，这样我们就有希望在数据类型上获得一些递归函数来通过 Agda 的终止检查器。

{-# OPTIONS --sized-types #-}

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P

module ListMerge
   { ℓ}
   (A : Set )
   {_<_ : Rel A ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

   open import Level
   open import Size

   data SortedList (l u : A) : {ι : _} → Set ( ⊔ ℓ) where
      [] : {ι : _} → .(l < u) → SortedList l u {↑ ι}
      _∷[_]_ : {ι : _} (x : A) → .(l < x) → (xs : SortedList x u {ι}) → 
               SortedList l u {↑ ι}

现在，一个想要在这样的数据结构上定义的经典函数是merge，它接受两个排序列表，并输出一个排序列表，其中包含输入列表的元素。

   open IsStrictTotalOrder isStrictTotalOrder

   merge : ∀ {l u} → SortedList l u → SortedList l u → SortedList l u
   merge xs ([] _) = xs
   merge ([] _) ys = ys
   merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
   ... | tri< _ _ _ = x ∷[ l<x ] (merge xs (y ∷[ _ ] ys))
   merge (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ = 
      x ∷[ l<x ] (merge xs ys)
   ... | tri> _ _ _ = y ∷[ l<y ] (merge (x ∷[ _ ] xs) ys)

这个函数看起来很无害，但要让 Agda 相信它是完全的可能很棘手。实际上，如果没有任何明确的大小索引，该函数就无法进行终止检查。一种选择是将函数拆分为两个相互递归的定义。这可行，但给定义和相关证明增加了一定量的冗余。

但同样，我不确定是否甚至可以明确给出大小索引，以便merge具有 Agda 接受的签名。这些幻灯片mergesort明确讨论；那里给出的签名表明以下应该有效：

   merge′ : ∀ {l u} → {ι : _} → SortedList l u {ι} → 
                      {ι′ : _} → SortedList l u {ι′} → SortedList l u
   merge′ xs ([] _) = xs
   merge′ ([] _) ys = ys
   merge′ (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
   ... | tri< _ _ _ = x ∷[ l<x ] (merge′ xs (y ∷[ _ ] ys))
   merge′ (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ = 
      x ∷[ l<x ] (merge′ xs ys)
   ... | tri> _ _ _ = y ∷[ l<y ] (merge' (x ∷[ _ ] xs) ys)

在这里，我们正在做的是允许输入具有任意（和不同）大小，并指定输出的大小为 ∞。

.ι != ∞ of type Size不幸的是，有了这个签名，Agda在检查xs定义的第一个子句的正文时抱怨说。我并没有声称非常了解大小类型，但我的印象是任何大小 ι 都会与 ∞ 统一。自从编写这些幻灯片以来，可能大小类型的语义已经发生了变化。

那么，我的场景是否是预期大小类型的用例？如果是这样，我应该如何使用它们？如果大小类型在这里不合适，为什么merge上面的第一个版本不终止检查，因为以下是：

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _     = y ∷ merge (x ∷ xs) ys 
merge xs ys = xs ++ ys

Answer 1