Generic level polymorphic N-ary functions

Guillaume Allais

doi:10.1145/3331554.3342604

Generic level polymorphic N-ary functions

Guillaume Allais

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

50 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 language	English
Title of host publication	TyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019
Editors	David Darais, Jeremy Gibbons
Place of Publication	New York
Pages	14-26
Number of pages	13
DOIs	https://doi.org/10.1145/3331554.3342604
Publication status	Published - 18 Aug 2019
Event	4th ACM SIGPLAN International Workshop on Type-Driven Development - Berlin, Germany Duration: 18 Aug 2019 → 18 Aug 2019 https://icfp19.sigplan.org/home/tyde-2019

Workshop

Workshop	4th ACM SIGPLAN International Workshop on Type-Driven Development
Abbreviated title	TyDe'19
Country/Territory	Germany
City	Berlin
Period	18/08/19 → 18/08/19
Internet address	https://icfp19.sigplan.org/home/tyde-2019

Keywords

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

Access to Document

10.1145/3331554.3342604

Allais-ACM-SIGPLAN-2019-Generic-level-polymorphic-N-aryAccepted author manuscript, 587 KB

Cite this

@inproceedings{6ea7bf44fc6446c5a920d86e4e63cdb2,

title = "Generic level polymorphic N-ary functions",

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.",

keywords = "dependently typed functional type, Agda formalization, arity-generic programming, universe polymorphism",

author = "Guillaume Allais",

year = "2019",

month = aug,

day = "18",

doi = "10.1145/3331554.3342604",

language = "English",

isbn = "9781450368155",

pages = "14--26",

editor = "David Darais and Jeremy Gibbons",

booktitle = "TyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019",

note = "4th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe'19 ; Conference date: 18-08-2019 Through 18-08-2019",

url = "https://icfp19.sigplan.org/home/tyde-2019",

}

TY - GEN

T1 - Generic level polymorphic N-ary functions

AU - Allais, Guillaume

PY - 2019/8/18

Y1 - 2019/8/18

N2 - 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.

AB - 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.

KW - dependently typed functional type

KW - Agda formalization

KW - arity-generic programming

KW - universe polymorphism

UR - https://github.com/gallais/nary

UR - http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=87160&copyownerid=145423

U2 - 10.1145/3331554.3342604

DO - 10.1145/3331554.3342604

M3 - Conference contribution book

SN - 9781450368155

SP - 14

EP - 26

BT - TyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019

A2 - Darais, David

A2 - Gibbons, Jeremy

CY - New York

T2 - 4th ACM SIGPLAN International Workshop on Type-Driven Development

Y2 - 18 August 2019 through 18 August 2019

ER -

Generic level polymorphic N-ary functions

Abstract

Workshop

Keywords

Access to Document

Other files and links

Fingerprint

Homotopy Type Theory: Programming and Verification

Cite this

Generic level polymorphic N-ary functions

Abstract

Workshop

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Homotopy Type Theory: Programming and Verification

Cite this