agda - 如何从 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 )，看起来树中每个 Value 的类型都依赖于键？或类似的东西。然后我发现 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

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