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