Data.AVL.map that changes value type

user_477476 0
Viewed 78

The Data.AVL module of the standard library is parametrized by the value type (among other things):

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

which of course means the map function it exports can't change the value type:

map : ({k : Key} → Value k → Value k) → Tree → Tree

Is there a way still to transform values stored in a Tree in a non-endomorphic way?

agda functor dictionary
2 Answers

Currently, this seems to be if not impossible then at least very annoying. The internal tree representation, Indexed.Tree, is parameterised by upper and lower bounds of type Key⁺ Value ..., so one would have to convert between Key⁺ V and Key⁺ W for different value types V, W and convince Agda that the conversion doesn't change anything. (It doesn't, of course, since Value is not used in the definition of Key⁺, but proving this is a hassle.)

The easiest way to solve the problem would therefore be to fix the library, moving the Value parameter down a few scopes. I'm sure the Agda devs would accept a patch to that effect.

user_29482500

I have performed the refactoring I was suggesting in the comment to @JannisLimperg's answer. You can readily access it in the refactor-avl branch of the standard library. Edit: it's been merged and is now part of the stdlib!

Here is the summary of the changes as listed in the changelog:

Overhaul of Data.AVL

  • Splitting out Data.AVL.Key and Data.AVL.Height which should not depend on the type of Value the tree will contain.

  • Putting Indexed into its own core module Data.AVL.Indexed following the example of e.g. Category.Monad.Indexed or Data.Container.Indexed

  • Giving map a polymorphic type: it is now possible to change the type of values contained in a tree when mapping over it.

user_7276670
Related