[Agda] finite map
mechvel at botik.ru
Thu Dec 19 14:46:53 CET 2013
On Thu, 2013-12-19 at 14:13 +0100, Nils Anders Danielsson wrote:
> On 2013-12-17 09:53, Sergei Meshveliani wrote:
> > I consider implementing AssociationList,
> > like AssocList in the Haskell library, only with some proofs.
> > Has the Agda standard library such?
> Perhaps you can use Data.List.Any.any.
1) AssocList is a list of pairs (key , value), with keys compared by
_≈_. But I think that there is also needed the condition of that the
keys do not repeat. This makes it a certain record. And then,
insert k v assocList
needs to include a proof for the condition.
Then, I am going to use this to define Multiset.
Generally, it is probably natural to have such AssocList in Standard
library -- because AVL.Tree is only for syntactic equality.
2) Suppose that AVL.Tree is generalized to Key being of
StrictTotalOrder _≈_ _<_ (rather than _≡_).
This requires certain difficult proofs.
And suppose that these proofs are `postulate'-d.
Probably, it will be useful even in this version
For example, one can define Multiset as Tree A ℕ, and it is also
O(n*(log n)) is lookup/insert.
More information about the Agda