What's in a Bag?: An “Application Proving Interface” for Finite Bags and its Implementation
Alexander Dinges, Ralf Thomas Walter Hinze · 2023
Bags are ubiquitous in program verification. They are the means of choice when we want to express that a collection of elements is a rearrangement of another collection. We are working towards an “application proving interface” (API) for finite bags that is perspicuous, rich, and easy to use. We propose an implementation of the Bag API in the dependently typed language Agda that has minimal meta-theoretic requirements and that we believe is suitable for both instructional and practical applications. Bags form a free commutative monoid. The implementation boils down to the free structure: bag expressions built from the empty bag , singleton bags, and the union of bags Math 1 , quotiented by the laws of commutative monoids.