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

Clemens Kupke; Fredrik Nordvall Forsberg; Sean Watters

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

Clemens Kupke, Fredrik Nordvall Forsberg, Sean Watters

Research output: Contribution to conference › Paper › peer-review

33 Downloads (Pure)

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.

Original language	English
Pages	1-20
Number of pages	20
Publication status	E-pub ahead of print - 29 Nov 2023
Event	The 21st Asian Symposium on Programming Languages and Systems - Taipei, Taiwan Duration: 26 Nov 2023 → 29 Nov 2023 Conference number: 21 https://conf.researchr.org/home/aplas-2023

Conference

Conference	The 21st Asian Symposium on Programming Languages and Systems
Abbreviated title	APLAS
Country/Territory	Taiwan
City	Taipei
Period	26/11/23 → 29/11/23
Internet address	https://conf.researchr.org/home/aplas-2023

Keywords

free algebraic structures
fresh lists
dependent type theory

Access to Document

Kupke-etal-ASPLS-2023-A-fresh-look-at-commutativityAccepted author manuscript, 781 KBLicence: Strath_1

Cite this

@conference{151dfc48b4e94919926edd0aa6057644,

title = "A fresh look at commutativity: free algebraic structures via fresh lists",

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{\textquoteright}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.",

keywords = "free algebraic structures, fresh lists, dependent type theory",

author = "Clemens Kupke and {Nordvall Forsberg}, Fredrik and Sean Watters",

year = "2023",

month = nov,

day = "29",

language = "English",

pages = "1--20",

note = "The 21st Asian Symposium on Programming Languages and Systems, APLAS ; Conference date: 26-11-2023 Through 29-11-2023",

url = "https://conf.researchr.org/home/aplas-2023",

}

TY - CONF

T1 - A fresh look at commutativity

T2 - The 21st Asian Symposium on Programming Languages and Systems

AU - Kupke, Clemens

AU - Nordvall Forsberg, Fredrik

AU - Watters, Sean

N1 - Conference code: 21

PY - 2023/11/29

Y1 - 2023/11/29

N2 - 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.

AB - 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.

KW - free algebraic structures

KW - fresh lists

KW - dependent type theory

M3 - Paper

SP - 1

EP - 20

Y2 - 26 November 2023 through 29 November 2023

ER -

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

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this