[Agda] parametrised data structures

[James Cranch]

Dear all,

I thought I'd have a go at writing some data structures for Agda. I've been 
focusing on maps ("dicts" or "associative arrays" if you prefer).

The attached code gives an example of what I was planning.

A "MapClass" is supposed to be all the vital structure of an implementation 
of maps with a certain set K of keys. So it specifies a type of maps (which 
depend on a value type, K -> Set) and some structure involving that.

One attraction of this kind of approach is that one could hope to compose 
MapClasses. For example, given a MapClass N, one could hope to define a 
MapClass of prefix trees where the nodes are stored as maps according to N.

However, I have been having problems getting this to work. The attached 
code violates positivity.

It is possible that a coinductive approach would solve that, but (firstly) 
I have no idea how and (secondly) I'm a bit worried because I actually want 
all prefix trees to genuinely be finite.

Does anyone have any ideas for circumventing this?

Best wishes,

James
\/\/\


-- 
------------------------------------------------------------
James Cranch                     http://jdc41.user.srcf.net/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Example.agda
Type: application/octet-stream
Size: 1997 bytes
Desc: Example.agda
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120126/e0af92f9/Example-0001.obj