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

Question

我能够轻易获得密钥列表如下：

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 

与此相关的，我也感到困惑的Value在Data.AVL声明。用(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

它看起来像每个值的树的类型是：

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

提取值然后可以用辅助功能沿toList产生的名单工作的帮助下完成取决于 的关键？

是。这就是为什么你的代码不会检测 - List s是同质的，但不同的Value有不同的索引（即取决于不同的Key s），因此也有不同的类型。

您可以使用不同种类的名单中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 a Tree，它使用您的keys来提取密钥列表并将它们变成Set s，方法是将Value映射到列表上。

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