Deutsch
 
Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Extensional equality preservation and verified generic programming

Urheber*innen
/persons/resource/nicola.botta

Botta,  Nicola
Potsdam Institute for Climate Impact Research;

/persons/resource/Nuria.Brede

Brede,  Nuria
Potsdam Institute for Climate Impact Research;

Jansson,  Patrik
External Organizations;

Richter,  Tim
External Organizations;

Externe Ressourcen
Volltexte (frei zugänglich)

25925oa.pdf
(Verlagsversion), 512KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


Zitierlink: https://publications.pik-potsdam.de/pubman/item/item_25925
Zusammenfassung
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.