Hi On 20 May 2009, at 07:08, Eugene Kirpichov wrote:
Thanks for the thorough response.
I've found Barras&Bernardo's work (at least, slides) about ICC*, I'll have a look at it. Could you provide with names of works by Altenkirch/Morris/Oury/you? The unordered pair example was especially interesting, since I am somewhat concerned with which operations do not break parametricity for *unordered sets* (as opposed to lists) - turns out, not too many.
Unordered sets or bags? Both are interesting, but hiding multiplicity makes sets tricky. Anyway, the news on publications is not so good. There's a paper "Observational Equality, Now!" by Altenkirch, McB, Swierstra which describes more or less how we handle observational equalities in general, but the specific instantiation of that pattern to quotients is more recent. An older paper "Constructing Polymorphic Programs with Quotient Types" by Abbott, Altenkirch, McB, Ghani extends container theory to things which are fuzzy about position (bags, cycles, etc), so may have some relevance. One formulation of quotients in Epigram 2, by the aforementioned Altenkirch, Morris, McB, Oury, are sadly documented only by the source code of the implementation, which you can find here http://www.e-pig.org/darcs/epigram/src/Quotient.lhs if you're curious. We knocked that up in about half an hour one afternoon shortly before the money ran out. The basic idea is terribly simple. A quotient is an abstract type X/f wrapping a carrier set X which has a notion of normal form given by f : X -> Y, for some Y. (e.g. f might be even, and Y Bool, giving arithmetic modulo 2). Equality on X/f is just equality at Y of whatever f gives on the packed C values. You can almost unpack X/f freely, gaining access to the element of the carrier, applying any (possibly dependent) function g you like to it -- just as long as you can prove that forall x x'. f x == f x' -> g x == g x' Any such g on X readily lifts to X/f. This to design and redesign an interface of quotient-respecting functions and then work compositionally. Amusingly, under certain circumstances, the idea of quotient by an equivalence fits this picture: given R : X -> X -> Prop, just take Y, above, to be X -> Prop (a predicate describing an equivalence class; predicates are equal by mutual inclusion). That allows you permutative quotients which don't admit a more concrete normal form, like general unordered pairs. Of course, if you do have an order on the data, you can just take f to be sort! Sorry for lack of writings, for which this status dump is poor compensation. Things aren't very applied yet, but the machinery for restricting observation in exchange for guarantees is on its way. We'll see what the summer brings. All the best Conor