Get rid of bag postulates

[yfcai]

Sebastian Schoener suggested proving bag postulates via some form of Church-encoding. If we Church-encode the universal property of free abelian groups, then sum and foldBag should become formalizable as well, and the code base would have no postulate other than extensionality.

[Blaisorblade]

But unless anybody knows some very clever encoding, free abelian groups are not an algebraic datatype, so it's not obvious how to Church-encode them. Church-encoding are equivalent to datatypes after all.

then sum and foldBag should become formalizable as well,

Formalizing those was not a problem IIRC.

Our problem was IIRC formalizing abelian-bag, that is, that bags satisfy abelian group axioms. That's only true if your implementation:

• either canonicalizes bag after each operation, so you can use structural equality. You had started designing such an implementation, but we decided the investment wasn't worth it.
• or is quotiented by the right equivalence — unfortunately, standard Agda & Coq don't have quotient types.

However, some quotients can be defined. Finite multisets are one such case; in this paper, Altenkirch & friends suggest defining a canonicalization procedure which returns another data structure — namely, canonicalize the elements into a sorted list (which is easy). At the time, you tried defining a search tree which was directly canonical, and that seemed much harder.

[Blaisorblade]

Church-encode the universal property of free abelian groups

Not sure what that means, but it seems that's maybe just a fold (which doesn't seem to help).

The universal property says that the fold is an isomorphism, but that's only provable given parametricity, and there are non-parametric models which violate parametricity and where (I understand) the fold is not an isomorphism — to quote Wadler, Church encodings are only weakly initial without parametricity — and initiality is equivalent to the universal property.

[yfcai]

Church-encode the universal property of free abelian groups

The universal property of free abelian groups is foldBag. I'm thinking about defining the bag type as the type of foldBag minus the bag parameter, something along the lines of the following code block. It's possible we'd need more properties tagged to the bag type to establish the homomorphism postulates.

Bag : Set → Set
Bag E = ∀ (A : AbelianGroup) → (f : E → A.Carrier) → A.Carrier

-- folding the empty bag results in the identity elem
empty : ∀ (E : Set) → Bag E
empty = λ A f → A.ε

-- folding a singleton bag is calling f on the single element
singleton : ∀ {E : Set} → E → Bag E
singleton x = λ A f → f x

union : ∀ {E : Set} → Bag E → Bag E → Bag E
union xs ys = λ A f → let open A in xs A f · ys A f

negate : ∀ {E : Set} → Bag E → Bag E
negate xs = λ A f → let open A in (xs A f) ⁻¹

bagGroup : ∀ (E : Set) → AbelianGroup (Bag E)
bagGroup = ?

flatMap : ∀ {D E : Set} → (f : D → Bag E) → Bag D → Bag E
flatMap {D} {E} f bag = bag (bagGroup E) f

[Blaisorblade]

Hm, I see. You could prove, say, that union xs ys ≡ union ys xs using extensionality, and proving that results of applying both sides to the same arguments are the same, by appealing to the properties of the target abelian group. That's already something, and maybe homomorphism postulates would also be provable.

The universal property of free abelian groups is foldBag.

Indeed, that's the eliminator half of the universal property — this only gives existence, not unicity.

Anyway, we have more urgent stuff for now.

[Toxaris]

Inlining Bag in the type of bagGroup would result in ... AbelianGroup (AbelianGroup -> ...) ... which I fear is not supported by Agda. More generally, Church encoding is not supported by Agda.

[Blaisorblade]

AbelianGroup (AbelianGroup -> ...) ... which I fear is not supported by Agda.

More generally, Church encoding is not supported by Agda.

Here's a reference confirming that, with further references in the comments: http://cstheory.stackexchange.com/a/30924/989

However, that's confusing. A Church encoding is there, but I see two problems:

• Because of impredicativity, it's not clear that you can produce a bag from a bag (as a consequence of what you say) — but maybe universe polymorphism could help somewhat?
• Induction fails — but do we look for inductions? Reason why it fails: in non-parametric models, so we can't prove it unless we internalize parametricity. The non-parametric elements are also those making the "unicity" part of the universal property fail.

That post also hints at some fixes I don't get (including axiom K + function extensionality + changes to the encoding); maybe the papers linked in the comments might help.

[Blaisorblade]

Because of impredicativity, it's not clear that you can produce a bag from a bag (as a consequence of what you say) — but maybe universe polymorphism could help somewhat?

Where by "somewhat" I meant "you can fold over a number at level N to get a number at level N - 1". And indeed, this is a much simpler problem with predicativity, discussed e.g. here: https://lists.chalmers.se/pipermail/agda/2013/005511.html

[yfcai]

More generally, Church encoding is not supported by Agda. "That's just a sacrifice that Agda makes (unless someone adds impredicativity)."

Unfortunate.