Generic level polymorphic N-ary functions
Allais, Guillaume; Darais, David and Gibbons, Jeremy, eds. (2019) Generic level polymorphic N-ary functions. In: TyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019. ACM, New York, NY, DEU, pp. 14-26. ISBN 9781450368155
Preview |
Text (Allais-ACM-SIGPLAN-2019-Generic-level-polymorphic-N-ary)
Allais_ACM_SIGPLAN_2019_Generic_level_polymorphic_N_ary.pdf Accepted Author Manuscript Download (601kB)| Preview |
Abstract
Agda's standard library struggles in various places with n-ary functions and relations. It introduces congruence and substitution operators for functions of arities one and two, and provides users with convenient combinators for manipulating indexed families of arity exactly one. After a careful analysis of the kinds of problems the unifier can easily solve, we design a unifier-friendly representation of n-ary functions. This allows us to write generic programs acting on n-ary functions which automatically reconstruct the representation of their inputs' types by unification. In particular, we can define fully level polymorphic n-ary versions of congruence, substitution and the combinators for indexed families, all requiring minimal user input.
ORCID iDs
Allais, Guillaume
ORCID: https://orcid.org/0000-0002-4091-657X;
Darais, David and Gibbons, JeremyItem type: Book Section ID code: 68800 Dates: DateEvent18 August 2019Published9 June 2019AcceptedKeywords: dependently typed functional type, Agda formalization, arity-generic programming, universe polymorphism, Electronic computers. Computer science, Computer Science(all) Subjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 10 Jul 2019 15:47 Last modified: 18 Mar 2021 03:48 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/68800
CORE (COnnecting REpositories)
CORE (COnnecting REpositories)