# [Agda] DTO, STO, AVL.Tree

Serge D. Mechveliani mechvel at botik.ru
Fri Oct 19 21:49:34 CEST 2012

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


More information about the Agda mailing list