Data.AVL的函子实例 [英] Functor instance for Data.AVL

问题描述

我想为Data.AVL.Indexed.Tree定义一个仿函数实例.这似乎很棘手，因为存储树的上下边界的索引的类型Key⁺取决于"树中值的类型(或类型族).

I would like to define a functor instance for Data.AVL.Indexed.Tree. This seems to be tricky because of the way the type Key⁺ of the indices storing the upper and lower bounds of the tree "depend on" the type (or family of types) of the values in the tree.

我想做的是在下面实现fmap:

What I want to do is implement fmap below:

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Temp
   {k ℓ}
   {Key : Set k}
   {_<_ : Rel Key ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

open import Function

module AVL (Value : Set)
   where open import Data.AVL (const Value) isStrictTotalOrder public

open AVL

fmap : {A B : Set} → (A → B) → ∀ {l u h} → 
       Indexed.Tree A l u h → Indexed.Tree B {!!} {!!} {!!}
fmap f = {!!}

目前，我忽略了依赖类型的树，而是假设值具有常量类型.这个想法是创建AVL模块的局部变体，仅在类型Value上进行参数化，并在不同的类型上实例化该类型，以提供fmap的签名.

For now I'm ignoring dependently-typed trees, and instead assuming the values have a constant type. The idea is to create a local variant of the AVL module, parameterised only on a type Value, and instantiate that at different types in order to give the signature of fmap.

问题是我似乎无法以l和u的界限进行量化，无法将 same 界限传递给两个不同的实例Indexed.Tree.我想我明白为什么是这样:有两种不同的Key⁺类型，一种是Indexed.Tree A，一种是Indexed.Tree B.但我希望这些类型相同.

The problem is that I then don't seem to be able to quantify over the bounds l and u in such a way that I can pass the same bounds to two different instances of Indexed.Tree. I think I see why this is: there are two different Key⁺ types, one for Indexed.Tree A and one for Indexed.Tree B. But I want these types to be the same.

我在这里遗漏了一些明显的东西吗?还是Data.AVL只是没有以允许我定义fmap的方式参数化?

Am I missing something obvious here, or is Data.AVL just not parameterised in way that allows me to define fmap?

推荐答案

在这里您不会遗漏任何明显的内容.即使Key⁺忽略了Value参数，Agda仍然将它们视为不同的类型.但是，您可以很容易地编写转换函数.我将打开一些模块以使名称可以使用:

You're not missing anything obvious here. Even though Key⁺ ignores the Value parameter, Agda still treats them as a different types. However, you can write the conversion functions quite easily. I'll open some modules to keep the names bearable:

open Extended-key
open Height-invariants

open import Data.Nat

移动Key⁺非常容易，因为基础Key是相同的:

Moving the Key⁺ is very easy, since the underlying Keys are the same:

to : ∀ {A B} → Key⁺ A → Key⁺ B
to ⊥⁺    = ⊥⁺
to ⊤⁺    = ⊤⁺
to [ k ] = [ k ]

移动_<⁺_关系也是可行的，您只需要在两个Key⁺上进行模式匹配，以便将类型简化为(基本上)同一性:

Moving the _<⁺_ relation is also doable, you just need to pattern match on both Key⁺s so that the type is reduced to (basically) identity:

to< : ∀ {A B} l u → _<⁺_ A l u → _<⁺_ B (to l) (to u)
to< ⊥⁺   ⊥⁺     p = p
to< ⊥⁺   ⊤⁺     p = p
to< ⊥⁺   [ _ ]  p = p
to< ⊤⁺    _     p = p
to< [ _ ] ⊥⁺    p = p
to< [ _ ] ⊤⁺    p = p
to< [ _ ] [ _ ] p = p

现在，这似乎可以解决问题，但是当您尝试将其记录下来时，您很快就会发现您还需要一种运送天平的方法.同样，没什么特别的:

Now, it might seem that this should do the trick, but when you try to write it down, you'll soon find out you need a way to transport the balance as well. Again, nothing extraordinary:

to∼ : ∀ {A B h₁ h₂} → _∼_ A h₁ h₂ → _∼_ B h₁ h₂
to∼ ∼+ = ∼+
to∼ ∼0 = ∼0
to∼ ∼- = ∼-

fmap的类型如下:

fmap : ∀ {A B} (f : ∀ {x} → A x → B x) {l u h} →
       Indexed.Tree A l u h → Indexed.Tree B (to l) (to u) h

这不是一个真实的" fmap，但是考虑到您需要使用不同的Key⁺，这与我们所能达到的尽可能接近.

It's not a "true" fmap, but considering you need to have different Key⁺s, this is as close as we can get.

leaf情况要求使用to<，但在其他情况下则微不足道:

leaf case requires usage of to<, but is otherwise trivial:

fmap f {lb} {ub} (Indexed.leaf l<u) = Indexed.leaf (to< lb ub l<u)

node案例是使事情变得有趣的地方.显而易见的解决方案:

node case is where things get interesting. The obvious solution:

fmap f (Indexed.node (k , v) l r bal) =
  Indexed.node (k , f v) (fmap f l) (fmap f r) (to∼ bal)

不进行类型检查.让我们找出原因.以下是上述表达式的类型和目标类型:

does not typecheck. Let's figure out why. Here are the types of the expression above and the goal type:

-- Have:
Indexed.Tree .B (to .l) (to .u) (suc (max .B (to∼ bal)))

-- Goal:
Indexed.Tree .B (to .l) (to .u) (suc (max .A bal))

所以我们需要一个额外的证明:

So we need one extra proof:

max≡ : ∀ {A B} {h₁ h₂} (bal : _∼_ A h₁ h₂) →
  max A bal ≡ max B (to∼ bal)
max≡ ∼+ = refl
max≡ ∼0 = refl
max≡ ∼- = refl

最后，我们可以通过max≡ bal重写目标类型并获得所需的实现:

And finally, we can rewrite the goal type via max≡ bal and get the desired implementation:

fmap f (Indexed.node (k , v) l r bal) rewrite max≡ bal =
  Indexed.node (k , f v) (fmap f l) (fmap f r) (to∼ bal)

---

我还使用了树的更多依赖变体.通过将AVL模块定义为:

---

I'm also using the more dependent variant of the tree. This is done by defining AVL module as:

import Data.AVL
module AVL (Value : Key → Set)
  = Data.AVL Value isStrictTotalOrder

然后只需要求映射函数遵守Key值:

And then simply requiring the mapping function to respect the Key value:

mapping-function : {A B : Key → Set} {x : Key} → A x → B x

---

还有另一种选择:重写Data.AVL模块，以使Extended-key和Height-invariants不被Value参数化.尽管这需要更改标准库，但我认为这是更好的解决方案.在Data.AVL之外，Extended-key和Heigh-invariants肯定是有用的-实际上，我有一个Data.BTree正是使用它.

---

There's another option: rewrite the Data.AVL module such that Extended-key and Height-invariants are not parametrised by Value. While this requires a change in the standard library, I think it's the better solution. Extended-key and Heigh-invariants could certainly be useful outside of Data.AVL - in fact, I have a Data.BTree that uses exactly that.

如果您决定采用这种方式，请考虑将它们分成新的模块(例如Data.ExtendedKey)并提交补丁/拉动请求.

If you decide to go this way, consider separating them into new modules (such as Data.ExtendedKey) and submitting a patch/pull request.

这篇关于Data.AVL的函子实例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！