[Haskell-cafe] Free theorems for dependent types?

[Conor McBride]

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