[Agda] collections/containers/finite sets

[Ramana Kumar]

On Mon, Nov 14, 2011 at 12:28 PM, Nils Anders Danielsson
<nad at chalmers.se> wrote:
> On 2011-11-14 13:03, Ramana Kumar wrote:
>>
>> 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 you want to combine two strict total orders into one you can use
>
>  Relation.Binary.Product.StrictLex._×-strictTotalOrder_,
>
> and for lists you can use
>
>  Relation.Binary.List.StrictLex.<-strictTotalOrder.
>
> The library does not define a strict total order for strings, but you
> can define one by converting the strings to lists of natural numbers.

Do you mean like this?

open import Relation.Binary using (Rel)
open import Relation.Binary.List.StrictLex using (Lex-<)
open import Data.Char using ()
open import Relation.Binary.Core using (_≡_)

str< : Rel String _
str< s₁ s₂ = Lex-< _≡_ (λ c₁ c₂ → Data.Char.toNat c₁ < Data.Char.toNat
c₂) (Data.String.toList s₁) (Data.String.toList s₂)

Is there a slicker way to do it?
In particular, are there notions of inverse image or relation
composition in the standard library somewhere?
Is it bad to use _≡_ for the equality? I tried to get Data.Char._==_,
but it's not a relation and I didn't know how to turn it into one.
And there must be more I can do with syntax and renaming (I'm still
pretty unsure about how modules work).

>
> --
> /NAD
>
>