Functor instance for Data.AVL

Question

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.

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 = {!!}

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.

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.

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

Answer 1

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

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 ]

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∼ ∼- = ∼-

The type of fmap then looks like this:

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

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

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 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

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)

---

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

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

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

---

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.

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