Agda's standard library Data.AVL.Sets containing Data.String as values

Question

I am trying to figure out how to use Agda's standard library implementation of finite sets based on AVL trees in the Data.AVL.Sets module. I was able to do so successfully using ℕ as the values with the following code.

import Data.AVL.Sets
open import Data.Nat.Properties as ℕ
open import Relation.Binary using (module StrictTotalOrder)
open Data.AVL.Sets (StrictTotalOrder.isStrictTotalOrder ℕ.strictTotalOrder)

test = singleton 5

Now I want to achieve the same thing but with Data.String as the values. There doesn't seem to be a corresponding Data.String.Properties module, but Data.String exports strictTotalOrder : StrictTotalOrder _ _ _ which I thought looked appropriate.

However, just strictly replacing the modules according to this assumption fails.

import Data.AVL.Sets
open import Data.String as String
open import Relation.Binary using (module StrictTotalOrder)
open Data.AVL.Sets (StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder)

Produces the error

.Relation.Binary.List.Pointwise.Rel 
  (StrictTotalOrder._≈_ .Data.Char.strictTotalOrder) (toList x) (toList x₁)
!= x .Relation.Binary.Core.Dummy.≡ x₁ of type Set

when checking that the expression
StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder
has type
Relation.Binary.IsStrictTotalOrder .Relation.Binary.Core.Dummy._≡_
__<__3

which I find difficult to unpack in detail since I have no idea what the Core.Dummy stuff is. It seems that there is some problem with the pointwise definition of the total order for Strings, but I can't figure it out.

Answer 1

If you look at Data.AVL.Sets, you can see that it is parameterised by a strict total order associated to the equivalence relation _≡_ (defined in Relation.Binary.PropositionalEquality):

module Data.AVL.Sets
  {k ℓ} {Key : Set k} {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

Now we can have a look at how the strict total order on Strings is defined. We first convert the Strings to List Chars and then compare them based on the strict lexicographic ordering for lists:

strictTotalOrder =
  On.strictTotalOrder
    (StrictLex.<-strictTotalOrder Char.strictTotalOrder)
    toList

If we dig into the code for StrictLex.<-strictTotalOrder, we can see that the equivalence relation associated to our List of Chars is built using the pointwise lifting Pointwise.isEquivalence of whatever the equivalence relation for Chars is.

But Pointwise.isEquivalence is defined in term of this datatype:

data Rel {a b ℓ} {A : Set a} {B : Set b}
         (_∼_ : REL A B ℓ) : List A → List B → Set (a ⊔ b ⊔ ℓ) where
  []  : Rel _∼_ [] []
  _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Rel _∼_ xs ys) →
        Rel _∼_ (x ∷ xs) (y ∷ ys)

So when Agda expects a strict total order associated to _≡_, we instead provided it with a strict total order associated to Rel _ on toList which has no chance of unifying.

How do we move on from here? Well, you could define your own strict total order on strings. Alternatively, you can try to turn the current one into one where _≡_ is the equivalence used. This is what I am going to do in the rest of this post.

So, I want to reuse an IsStrictTotalOrder R O with a different equivalence relation R′. The trick is to notice that if can transport values from R a b to R′ a b then, I should be fine! So I introduce a notion of RawIso A B which states that we can always transport values from A to B and vice-versa:

record RawIso {ℓ : Level} (A B : Set ℓ) : Set ℓ where
  field
    push : A → B
    pull : B → A
open RawIso public

Then we can prove that RawIsos preserve a lot of properties:

RawIso-IsEquivalence :
  {ℓ ℓ′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  IsEquivalence R → IsEquivalence R′
RawIso-IsEquivalence = ...

RawIso-Trichotomous :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  Trichotomous R O → Trichotomous R′ O
RawIso-Trichotomous = ...

RawIso-Respects₂ :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  O Respects₂ R → O Respects₂ R′
RawIso-Respects₂ = ...

All these lemmas can be combined to prove that given a strict total order, we can build a new one via a RawIso:

RawIso-IsStrictTotalOrder :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  IsStrictTotalOrder R O → IsStrictTotalOrder R′ O    
RawIso-IsStrictTotalOrder = ...

Now that we know we can transport strict total orders along these RawIsos, we simply need to prove that the equivalence relation used by the strict total order defined in Data.String is in RawIso with propositional equality. It's (almost) simply a matter of unfolding the definitions. The only problem is that equality on characters is defined by first converting them to natural numbers and then using propositional equality. But the toNat function used has no stated property (compare e.g. to toList and fromList which are stated to be inverses)! I threw in this hack and I think it should be fine but if someone has a better solution, I'd love to know it!

toNat-injective : {c d : Char} → toNat c ≡ toNat d → c ≡ d
toNat-injective {c} pr with toNat c
toNat-injective refl | ._ = trustMe -- probably unsafe
  where open import Relation.Binary.PropositionalEquality.TrustMe

Anyway, now that you have this you can unfold the definitions and prove:

rawIso : {a b : String} →
         RawIso ((Ptwise.Rel (_≡_ on toNat) on toList) a b) (a ≡ b)
rawIso {a} {b} = record { push = `push ; pull = `pull } where

  `push : {a b : String} → (Ptwise.Rel (_≡_ on toNat) on toList) a b → a ≡ b
  `push {a} {b} pr =
    begin
      a                   ≡⟨ sym (fromList∘toList a) ⟩
      fromList (toList a) ≡⟨ cong fromList (aux pr) ⟩
      fromList (toList b) ≡⟨ fromList∘toList b ⟩
      b
    ∎ where

     aux : {xs ys : List Char} → Ptwise.Rel (_≡_ on toNat) xs ys → xs ≡ ys
     aux = Ptwise.rec (λ {xs} {ys} _ → xs ≡ ys)
           (cong₂ _∷_ ∘ toNat-injective) refl

  `pull : {a b : String} → a ≡ b → (Ptwise.Rel (_≡_ on toNat) on toList) a b
  `pull refl = Ptwise.refl refl

Which allows you to

stringSTO : IsStrictTotalOrder _ _
stringSTO = StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder

open Data.AVL.Sets (RawIso-IsStrictTotalOrder rawIso stringSTO)

Phew!

I have uploaded a raw gist so that you can easily access the code, see the imports, etc.