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

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 相信它是完全的可能很棘手。实际上，如果没有任何明确的大小索引，该函数就无法进行终止检查。一种选择是split the function into two mutually recursive definitions。这行得通，但给定义和相关证明增加了一定量的冗余。

但同样，我不确定是否甚至可以明确给出大小索引，以便merge 具有 Agda 将接受的签名。 These slides 明确讨论 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)

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

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

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

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

有趣的是，您的第一个版本实际上是正确的。我提到考虑到Size，Agda 启用了一些额外的规则，其中之一是↑ ∞ ≡ ∞。顺便说一句，您可以通过以下方式确认：

↑inf : ↑ ∞ ≡ ∞
↑inf = refl

嗯，这让我调查了其他规则是什么。我在 Andreas Abel 的尺寸类型幻灯片中找到了其余部分（可以找到 here）：

• ↑ ∞ ≡ ∞
• i ≤ ↑ i ≤ ∞
• T {i} <: T {↑ i} <: T {∞}

<: 关系是子类型关系，您可能从面向对象的语言中知道它。还有一个与这种关系相关的规则，subsumption 规则：

Γ ⊢ x : A   Γ ⊢ A <: B
────────────────────── (sub)
      Γ ⊢ x : B

因此，如果您有一个A 类型的值x，并且您知道A 是B 的子类型，那么您也可以将x 视为B 类型。这看起来很奇怪，因为遵循大小类型的子类型化规则，您应该能够将类型为 SortedList l u {ι} 的值视为 SortedList l u。

所以我做了一点挖掘，发现了这个bug report。事实上，问题只是 Agda 没有正确识别大小并且规则没有触发。我需要做的就是将SortedList的定义重写为：

data SortedList (l u : A) : {ι : Size} → Set (? ⊔ ℓ) where
  -- ...

就是这样！

---

作为附录，这是我用于测试的代码：

data ℕ : {ι : _} → Set where         -- does not work
-- data ℕ : {ι : Size} → Set where   -- works
  zero : ∀ {ι} →         ℕ {↑ ι}
  suc  : ∀ {ι} → ℕ {ι} → ℕ {↑ ι}

test : ∀ {ι} → ℕ {ι} → ℕ
test n = n