[Agda] collections/containers/finite sets

[Ramana Kumar]

On Thu, Nov 10, 2011 at 10:22 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> On 10.11.11 4:59 PM, Ramana Kumar wrote:
>>
>> Is there an Agda library defining a type of finite set-like
>> collections of elements of any type?
>
> If you are not worried about complexity, you can use
>
>  List A
>
> as finite collection of elements of type A.  Otherwise, if you want an
> efficient implementation, you can have a look the the AVL trees of the
> standard library or Julien Oster's red-black trees.

Ah I didn't realize that AVL trees were in the standard library,
because they're not linked to from the README (I found them just now
by first clicking "Everything" from the README, then scanning down for
AVL). Thanks.

AVL trees will probably suit me, but I'm curious whether it makes
sense to write some Agda code to just the interface for finite sets
without specifying exactly how they're implemented. Is that possible?
I think in Coq you could achieve that (with MSets) by writing your
code as the body of a functor parameterised by something matching the
MSetsInterface.

>
> https://bitbucket.org/anyfoo/agda-std-trees/src
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>