Designing Abstract Data Types

[Taneb]

We've had trouble in the past (e.g. here and here) defining abstract data types. We should come up with a strategy we can use to define interfaces without taking months of discussion.

[Taneb]

As I see it, there's two difficulties apparent in Agda that aren't present in something like ML:

1. we care about the properties of the operations as well as the operations themselves
2. we need to be able to express things like "taking all the elements out of a queue one at a time will eventually terminate", because Agda is a total programming language