English
 
Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Extensional equality preservation and verified generic programming

Botta, N., Brede, N., Jansson, P., Richter, T. (2021): Extensional equality preservation and verified generic programming. - Journal of Functional Programming, 31, e24.
https://doi.org/10.1017/S0956796821000204

Item is

Files

show Files
hide Files
:
25925oa.pdf (Publisher version), 512KB
Name:
25925oa.pdf
Description:
-
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
Copyright Date:
-
Copyright Info:
-

Locators

show
hide
Description:
-

Creators

show
hide
 Creators:
Botta, Nicola1, Author              
Brede, Nuria1, Author              
Jansson, Patrik2, Author
Richter, Tim2, Author
Affiliations:
1Potsdam Institute for Climate Impact Research, ou_persistent13              
2External Organizations, ou_persistent22              

Content

show
hide
Free keywords: Dependent Type Theory; Verified generic programming; Extensional Equality
 Abstract: In verified generic programming, one cannot exploit the structure of concrete data types but has to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads are at the core of many applications of functional programming. This raises the question of what useful ADTs for verified functors and monads could look like. The functorial map of many important monads preserves extensional equality. For instance, if f , g : A → B are extensionally equal, that is, ∀x ∈ A, f x = g x, then map f : List A → List B and map g are also extensionally equal. This suggests that preservation of extensional equality could be a useful principle in verified generic programming. We explore this possibility with a minimalist approach: we deal with (the lack of) extensional equality in Martin-Löf’s intensional type theories without extending the theories or using full-fledged setoids. Perhaps surprisingly, this minimal approach turns out to be extremely useful. It allows one to derive simple generic proofs of monadic laws but also verified, generic results in dynamical systems and control theory. In turn, these results avoid tedious code duplication and ad- hoc proofs. Thus, our work is a contribution towards pragmatic, verified generic programming.

Details

show
hide
Language(s): eng - English
 Dates: 2021-08-012021-10-212021
 Publication Status: Finally published
 Pages: 24
 Publishing info: -
 Table of Contents: -
 Rev. Type: Peer
 Identifiers: PIKDOMAIN: RD4 - Complexity Science
Organisational keyword: RD4 - Complexity Science
MDB-ID: yes - 3218
Model / method: Decision Theory
Model / method: Open Source Software
Model / method: Research Software Engineering (RSE)
DOI: 10.1017/S0956796821000204
OATYPE: Hybrid - Cambridge University Press
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Journal of Functional Programming
Source Genre: Journal, SCI, Scopus
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 31 Sequence Number: e24 Start / End Page: - Identifier: ISSN: 0956-7968
Other: 1469-7653
Publisher: Cambridge University Press
CoNE: https://publications.pik-potsdam.de/cone/journals/resource/journal-functional-programming