如何从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

相关地,我也对ValueData.AVL中的声明感到困惑.有( Value : Key ? Set v ),看起来树中每个Value的类型取决于键？或类似的东西.然后我认为proj 2会返回类型的东西Set v,所以我尝试了这个:

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

但这也不起作用(它失败并出现不同的错误).请说明如何从Data.AVL.Tree获取值列表(或解释为什么不可能).奖金:解释为什么我的两次尝试都失败了.

Ps这是使用Agda的版本2.4.2.3和agda-stdlib.

Answer 1

看起来树中每个Value的类型都取决于键？

是.这就是为什么你的代码没有类型检查 - 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