如何从 Data.AVL.Tree 中获取值列表？

Question

我很容易就能得到一个 Keys 列表，如下：

open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_)

module AVL-Tree-Functions
  { k v ℓ } { Key : Set k }
  ( Value : Key → Set v )
  { _<_ : Rel Key ℓ }
  ( isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_ )
  where

  open import Data.AVL Value isStrictTotalOrder public

  open import Data.List.Base
  open import Function
  open import Data.Product

  keys : Tree → List Key
  keys = Data.List.Base.map proj₁ ∘ toList

但我不清楚如何指定返回值列表的函数类型。这是我的第一次尝试：

  -- this fails to typecheck
  values : Tree → List Value
  values = Data.List.Base.map proj₂ ∘ toList

与此相关，我也对 Data.AVL 中 Value 的声明感到困惑。使用( Value : Key → Set v )，看起来树中每个值的类型都依赖于键？或类似的东西。然后我发现 proj₂ 会返回 Set v 类型的东西，所以我尝试了这个：

  -- this also fails to typecheck
  values : Tree → List (Set v)
  values = Data.List.Base.map proj₂ ∘ toList

但这也不起作用（它失败并出现不同的错误）。请展示如何从 Data.AVL.Tree 获取值列表（或解释为什么不可能）。奖励：解释为什么我的两次尝试都失败了。

附：这是使用 2.4.2.3 版的 Agda 和 agda-stdlib。

Answer 1

看起来树中每个值的类型取决于 钥匙？

是的。这就是为什么您的代码不进行类型检查的原因 - Lists 是同质的，但不同的 Values 具有不同的索引（即取决于不同的 Keys），因此类型也不同。

您可以像 gallais 的回答那样使用异构列表，但在您的情况下，索引列表可能就足够了：

open import Level

data IList {ι α} {I : Set ι} (A : I -> Set α) : Set (ι ⊔ α) where
  []ᵢ  : IList A
  _∷ᵢ_ : ∀ {i} -> A i -> IList A -> IList A

projs₂ : ∀ {α β} {A : Set α} {B : A -> Set β} -> List (Σ A B) -> IList B
projs₂  []            = []ᵢ
projs₂ ((x , y) ∷ ps) = y ∷ᵢ projs₂ ps

或者你可以结合这些技术：

data IHList {ι α} {I : Set ι} (A : I -> Set α) : List I -> Set (ι ⊔ α) where
  []ᵢ  : IHList A []
  _∷ᵢ_ : ∀ {i is} -> A i -> IHList A is -> IHList A (i ∷ is)

projs₂ : ∀ {α β} {A : Set α} {B : A -> Set β}
       -> (xs : List (Σ A B)) -> IHList B (Data.List.Base.map proj₁ xs)
projs₂  []            = []ᵢ
projs₂ ((x , y) ∷ ps) = y ∷ᵢ projs₂ ps

Answer 2

Value : Key → Set v 的意思是值的类型可能取决于它所关联的键。这意味着 AVL 树可能包含布尔值、Nats 等，只要它们存储的键反映了这一事实。有点像记录可以存储不同类型的值（类型由字段名称决定）。

现在，它们是不同的方法：您可以将整个树的内容提取到键/值对列表中（因为列表的元素都是相同的，您需要在这里构建一个对，以便所有具有相同的类型Σ Key Value)。这就是toList 所做的。

另一种方法是使用通常称为HList（H 代表异构）的方法，它在列表中在类型级别存储每个元素应该具有的类型.出于大小原因，我在这里通过对元素集的归纳来定义它，但这一点都不重要（如果你将它定义为数据类型，它会活得更高一级）：

open import Level
open import Data.Unit

HList : {ℓ : Level} (XS : List (Set ℓ)) → Set ℓ
HList []       = Lift ⊤
HList (X ∷ XS) = X × HList XS

现在，您可以给出值的HList 的类型。给定 t 和 Tree，它使用您的 keys 提取键列表，并通过在列表上映射 Value 将它们转换为 Sets。

values : (t : Tree) → HList (List.map Value (keys t))

然后可以借助沿toList 生成的列表工作的辅助函数来完成值的提取：

values t = go (toList t) where

  go : (kvs : List (Σ Key Value)) → HList (List.map Value $ List.map proj₁ kvs)
  go []         = lift tt
  go (kv ∷ kvs) = proj₂ kv , go kvs