[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