如何獲取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