[Agda] collections/containers/finite sets

[Ramana Kumar]

Dear Nils (and list)

I appreciate the effort you put into README.AVL, and I hope to use it some day.
At present, though, I'm still struggling with simpler things.
Perhaps a very concrete example will help me get an answer.

Suppose I have started a module like this:

module Hol.Type where

open import Data.String using (String)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec;_∷_;[_];[])

record TypeOperator : Set where
  field name  : String
        arity : ℕ

data Type : Set where
  TyVar : String -> Type
  TyApp : (op : TypeOperator) -> Vec Type (TypeOperator.arity op) -> Type

Now suppose I want to make AVL Sets of these Types.
That should require me to come up with a strict total order on them, right?
But I would imagine that such a relation can be computed completely
automatically using existing relations on String and Vec.
What's the best (i.e. shortest, or most elegant) way to continue this
module so it eventually includes a value whose type is an AVL set of
Types?
If the order relation can't be computed automatically, I'd still like
pointers on the syntax for specifying it manually.
(Eventually I plan to make AVL sets of further user-defined records
that include the record above, but I think this is a simpler example
that will still be useful.)

On Fri, Nov 11, 2011 at 6:53 PM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-11-11 11:49, Ramana Kumar wrote:
>>
>> Are there any example files available on how to use Data.AVL.Sets?
>> I'm getting this kind of error
>> Set !=<
>> (.Relation.Binary.IsStrictTotalOrder
>>  .Relation.Binary.Core.Dummy._≡_ _79)
>> of type Set₁
>> when checking that the expression Formula has type
>> .Relation.Binary.IsStrictTotalOrder .Relation.Binary.Core.Dummy._≡_
>> _79
>> which presumably means I need to show I have a strict total order on
>> the type of elements of the sets.
>> I don't know how to do that concretely in Agda... (theoretically it
>> should be easy for my type though)
>
> I just added some examples showing how the AVL tree module can be used:
>
>  http://www.cse.chalmers.se/~nad/listings/lib/README.AVL.html
>
> Note that these examples use the current development version of the
> library, in which the AVL tree interface has changed.
>
> --
> /NAD
>
>