Book chapter
Quotients by Idempotent Functions in Cedille
Trends in Functional Programming, pp.1-20
Lecture Notes in Computer Science, Springer International Publishing
05/11/2020
DOI: 10.1007/978-3-030-47147-7_1
Abstract
We present a simple characterization of definable quotient types as being induced by idempotent functions, and an encoding of this in Cedille (a dependently typed programming language) in which both equational constraints and the packaging that associates these with elements of the carrier type are irrelevant, facilitating equational reasoning in proofs. We provide several concrete examples of definable quotients using this encoding and give combinators for function lifting (with one variant having zero run-time cost).
Details
- Title: Subtitle
- Quotients by Idempotent Functions in Cedille
- Creators
- Andrew Marmaduke - University of IowaChristopher Jenkins - University of IowaAaron Stump - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Trends in Functional Programming, pp.1-20
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-47147-7_1
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 05/11/2020
- Academic Unit
- Computer Science
- Record Identifier
- 9984259493602771
Metrics
15 Record Views