[Agda] DTO, STO, AVL.Tree

[Serge D. Mechveliani]

People,
I have a couple of beginner qustions on Standard Library:
* on the propositional equality,
* on DecidableTotalOrder vs StrictTotalOrder.

Propositional equality (\equiv)
-------------------------------

The Haskell Standard library  has for equality _only_ "algebraic" one:
(==) of the  class Eq.
Its instance needs to be implemented by a programmer for each appropriate 
user data type. And this approach works fine. 
For example, the GHC library has the type constructor  Dat.Map.Map  
for a finite map, which is represented by a _balanced binary search tree_
(BBT).
A key type needs to have an instance of  Eq (with ==) and  Ord 
(with `compare', (<)) -- the former being a superclass for the latter.
And all the usual operations with BBT are implemented nicely.
And this does not need any more special equality than a generic (==).

Now, what I see in the Agda lib:

1. The `class'  Setoid,  with its fields  Carrier  and  \~~.
   I think,  \~~  needs to be used as the algebraic equality, 
   similarly as  (==) used in Haskell.
   
The classes for equality and ordering, and so on, are formulated in a 
fully mathematically adequate way (which is not possible in Haskell).

2. There is a data type for the  propositional equality  \equiv,  
   with a single constructor   refl : x \equiv x 
This is something very different from  \~~.
It has some relevance to the function  refl x x = true,  which is not
possible in Haskell. I think, this is natural to be used in constructing 
equality proofs.

3. Unlike GHC,  Data.AVL.Tree  requires  \equiv  rather than  Setoid.\~~  
   Why?
   \~~ is more generic, it can be implemented by the user;
   Map.Map of GHC relies on an analogue of \~~, and it is all right.

4. DecidableTotalOrder  (DTO)  vs  StrictTotalOrder (STO).

Standard library declares DTO and STO, IsDTO and IsSTO. 
Has it something to reflected a connection between these two?

4.1. Thus, consider DTO, with its _<=_,  and define 
                                       x < y = (x <= y , \neg (x \~~ y))
-- is less-or-equal and not equal.
Is it true that this  _<_  satisfies IsSTO ?

4.2. For STO with its _<_, define  
                               x <= y = (x < y) disjointUnion (x \~~ y)
-- is less or equal.
Is it true that this _<=_ satisfies  IsDTO ?

If 4.1 and 4.2 are true, then it is probably natural to add _<_ to DTO
(IsDTO), and to remove STO, IsSTO from Standard library
-- ?
A similar question is for the relation between  TotalOrdering  and
Strict?Ordering.

4.3. In particular, I have a strange problem with using DTO + STO
     in _sorting a list_.

First, I have the function  orderList  which relies on  DTO, with its
\~~ and _<=_.  It also provides a proof for the result orderedness by 
_<=_.  
Then, I need to add a proof for that 
                            multiset xs  \~~  multiset (orderList xs).
And I use  AVL.Tree  to represent  Multiset :  
a finite map from  (Carrier dto)  to  Multiplicity = Bin.

But  AVL  requires the propositional equality \equiv  and  _<_ of IsSTO.
So, I probably need to 
a) specialize from  \~~  to  \equiv,  from  (IsDTO \~~    _<=_)
                                      to    (IsDTO \equiv _<=_),
b) define  _<_  as   x < y = (x <= y , \neg (x \~~ y)),

c) build the instance of  (IsSTO \equiv _<_)  from  (IsDTO \equiv _<=_).
   I do now know, so far, how easy this may occur.
   What does Standard library have to support this construction?

What may be a nice design with agreeing these DTO and STO things in 
this example?

I am not sure, but have an impression that 
1) STO needs to be removed and to merge to DTO, with _<_ defined via
   _<=_  and  \neg (x \~~ y),
2) AVL needs to generalize from \equiv to \~~.

Am I missing something?
Thank you in advance for your comments.

------
Sergei