A fresh look at commutativity : free algebraic structures via fresh lists

Kupke, Clemens and Nordvall Forsberg, Fredrik and Watters, Sean (2023) A fresh look at commutativity : free algebraic structures via fresh lists. In: The 21st Asian Symposium on Programming Languages and Systems, 2023-11-26 - 2023-11-29.

[thumbnail of Kupke-etal-ASPLS-2023-A-fresh-look-at-commutativity]
Preview
 Text. Filename: Kupke_etal_ASPLS_2023_A_fresh_look_at_commutativity.pdf
Accepted Author Manuscript
License: Strathprints license 1.0
Download (799kB)| Preview

Abstract

We show how types of finite sets and multisets can be constructed in ordinary dependent type theory, without the need for quotient types or working with setoids, and prove that these constructions realise finite sets and multisets as free idempotent commutative monoids and free commutative monoids, respectively. Both constructions arise as generalisations of C. Coquand’s data type of fresh lists, and we show how many other free structures also can be realised by other instantiations. All of our results have been formalised in Agda.

CORE (COnnecting REpositories)