将排序列表与大小类型合并

假设我们有一个排序列表的数据类型，具有与证明无关的排序见证。我们将使用 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 相信它是完整的可能很棘手。事实上，如果没有任何显式的大小索引，该函数将无法进行终止检查。一种选择是将函数拆分为两个相互递归的定义 https://stackoverflow.com/questions/17910737/termination-check-on-list-merge。这是可行的，但给定义和相关证明增加了一定量的冗余。

但同样，我不确定是否可以明确给出大小索引，以便merge有 Agda 会接受的签名。这些幻灯片 http://www2.tcs.ifi.lmu.de/~abel/appsemTalk.ps.gz%E2%80%8E讨论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 抱怨说.ι != ∞ of type Size、检查身体时xs定义的第一个子句。我并不声称非常了解大小类型，但我的印象是任何大小 ι 都会与 ∞ 统一。也许自这些幻灯片编写以来，大小类型的语义已经发生了变化。

那么，我的场景是针对哪种大小的类型的用例吗？如果是这样，我应该如何使用它们？如果尺寸类型在这里不合适，为什么第一个版本merge上面不是终止检查，因为以下是 https://stackoverflow.com/questions/17910737/termination-check-on-list-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

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

↑inf : ↑ ∞ ≡ ∞
↑inf = refl

好吧，这促使我调查其他规则是什么。我在 Andreas Abel 的关于尺寸类型的幻灯片中找到了其余的内容（可以找到here http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf):

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

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

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

所以，如果你有一个价值观x类型的A你知道A是一个子类型B，你可以治疗x作为类型B以及。这看起来很奇怪，因为遵循大小类型的子类型规则，您应该能够处理类型的值SortedList l u {ι} as SortedList l u.

所以我做了一些挖掘并发现了这个错误报告 http://code.google.com/p/agda/issues/detail?id=701。事实上，问题只是 Agda 无法正确识别大小，并且规则不会触发。我所需要做的就是重写定义SortedList to:

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