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

Question

我很容易得到一个Key列表，如下：

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

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

  -- 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 中获取值列表（或解释为什么不可能）。奖励：解释为什么我的两次尝试都失败了。

P.s。这是使用 Agda 的 2.4.2.3 版本和 agda-stdlib。

Answer 1

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

Answer 2

it looks like the type of each Value in the tree is dependent on the key?

是的。这就是为什么您的代码不进行类型检查的原因 — List 是同类的，但不同的 Value 具有不同的索引（即取决于不同的 Key），因此类型也不同。

您可以像 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

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

How to obtain a list of values from a Data.AVL.Tree?

agda

dependent-type