Generic level polymorphic N-ary functions

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

5 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationTyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019
EditorsDavid Darais, Jeremy Gibbons
Place of PublicationNew York
Pages14-26
Number of pages13
DOIs
Publication statusPublished - 18 Aug 2019
Event4th ACM SIGPLAN International Workshop on Type-Driven Development - Berlin, Germany
Duration: 18 Aug 201918 Aug 2019
https://icfp19.sigplan.org/home/tyde-2019

Workshop

Workshop4th ACM SIGPLAN International Workshop on Type-Driven Development
Abbreviated titleTyDe'19
CountryGermany
CityBerlin
Period18/08/1918/08/19
Internet address

Keywords

  • dependently typed functional type
  • Agda formalization
  • arity-generic programming
  • universe polymorphism

Fingerprint Dive into the research topics of 'Generic level polymorphic N-ary functions'. Together they form a unique fingerprint.

  • Projects

  • Cite this

    Allais, G. (2019). Generic level polymorphic N-ary functions. In D. Darais, & J. Gibbons (Eds.), TyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019 (pp. 14-26). New York. https://doi.org/10.1145/3331554.3342604