[Agda] collections/containers/finite sets

[Andreas Abel]

On 11/10/11 11:31 PM, Ramana Kumar wrote:
> 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.

You can define a record type with the operations you need for your 
finite sets---this corresponds to what you usually do with a module.

This would roughly look like

record FSet (A : Set)(oA : IsStrictTotalOrder A) : Set1 where
   constructor fSet
   field
     T : Set  -- the representation of the finite set
     empty  : T                -- the operations on T
     member : A -> T -> Bool
     insert : A -> T -> T
     delete : A -> T -> T
     ...

Then you can work with an abstraction, e.g. like this

module WorkingWithIntSetAbstractly (IntSet : FSet Int ...) where

   open IntSet

   myIntSet : T
   myIntSet = empty

   myIntSet1 : T
   myIntSet1 = insert 5 myIntSet

   ....

(I did not type this code into Agda, there might be errors...)

In the std-lib there are many examples of such abstract developments, 
look e.g. at Algebra.Structures.  (However, I acknowledge that these 
examples are complicated...)

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/