Instantiating Data.AVL module with different element types

Question

The Agda documentation gives some example of how to use the Data.AVL module:

http://darcsden.com/abel/AgdaPrelude/browse/README/AVL.agda

In the examples, the module is instantiated once at import-time with arguments specifying the type of values stored in the trees, as well as an order for the key type.

How does one use AVL trees at different value types (e.g. both trees of strings and trees of numbers) in the same client module?

Answer 1

You can open the Data.AVL module and use the functions directly. This is quite inconvenient because anytime you use such function, you have to give it all the module parameters, which means you'd end up with code looking like:

open import Data.AVL
open import Data.Nat
open import Data.Nat.Properties
open import Data.String
  using (String)
open import Relation.Binary

test-tree : Tree (λ _ → String)
  (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)
test-tree = empty (λ _ → String)
  (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)

---

Let's not go there. Instead, we'll exploit the fact that Agda can create and apply modules (even inside another module). Here's one (totally artificial, sorry) example:

module M (A B : Set) where
  f : A → B → A
  f x _ = x

We can create new module just by applying M:

module M′ = M ℕ

If we ask what is the type of M′.f (using C-c C-d, for example), we get (B : Set) → ℕ → B → ℕ. If you compare that with M.f : (A : Set) (B : Set) → A → B → A, you can see that ℕ was indeed substituted for A.

Also, by applying it fully:

module M″ = M ℕ String
-- or equivalently
module M″ = M′  String

we get the expected M″.f : ℕ → String → ℕ.

---

So, how do we apply it to AVL? At this point, you probably see what's going to happen next:

module AVL[ℕ,String] = Data.AVL (λ _ → String)
  (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)

module AVL[ℕ,ℕ] = Data.AVL (λ _ → ℕ)
  (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)

All stuff from AVL[ℕ,String] operates on trees where the key is ℕ and the value is String. And here's how you can use it:

tree₁ : AVL[ℕ,String].Tree
tree₁ = insert 42 "hello" empty
  where
  open AVL[ℕ,String]

tree₂ : AVL[ℕ,ℕ].Tree
tree₂ = insert 1 2 empty
  where
  open AVL[ℕ,ℕ]

Notice that I locally open the AVL[ℕ,String] and AVL[ℕ,ℕ] modules so that I don't have to write, for example, AVL[ℕ,String].insert. Without the intermediate module, it would look like:

tree₁ : _
tree₁ = insert 4 "hello" empty
  where
  open Data.AVL (λ _ → String)
    (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)

Which is still far better than using the functions directly.

---

We can go even further and use instance arguments:

open import Data.Vec

module AVL-Instance
  {k} {Key : Set k}
  {v} {Value : Key → Set v}
  {ℓ} {_<_ : Rel Key ℓ}
  {{isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_}}
  = Data.AVL Value isStrictTotalOrder

ℕ-IsStrictTotalOrder : _
ℕ-IsStrictTotalOrder =
  StrictTotalOrder.isStrictTotalOrder strictTotalOrder

open AVL-Instance
  hiding (Tree)

open module AVL-Type {k v} (Key : Set k) (Value : Key → Set v)
  = AVL-Instance {Key = Key} {Value = Value}
  using (Tree)

tree₁ : Tree ℕ λ _ → String
tree₁ = insert 4 "hello" empty

tree₂ : Tree ℕ (Vec ℕ)
tree₂ = insert 2 (0 ∷ 1 ∷ []) empty

This seems to work quite well, but my feeling is that this will be very fragile beyond simple examples.

To explain where my intuition is coming from, consider:

open import Data.Vec
  hiding (lookup)
open import Data.Maybe

tree₃ : Maybe (Vec ℕ 2)
tree₃ = lookup 2 (insert 2 (0 ∷ 1 ∷ []) empty)

What is the type of empty? It can very well be Tree ℕ (Vec ℕ), Tree ℕ λ _ → Vec ℕ 2 or something crazy like Tree ℕ λ n → Vec ℕ (2 * n + 12). Instead of guessing, Agda will simply reject this definition and ask you to fill in more information:

tree₃ : Maybe (Vec ℕ 2)
tree₃ = lookup 2 (insert 2 (0 ∷ 1 ∷ []) (empty {Value = Vec ℕ}))

You've been warned. :)