Generic level polymorphic N-ary functions

Research output: Contribution to conferencePaper

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.

Workshop

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

Fingerprint

Substitution reactions
Mathematical operators

Keywords

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

Cite this

Allais, G. (Accepted/In press). Generic level polymorphic N-ary functions. Paper presented at 4th ACM SIGPLAN International Workshop on Type-Driven Development, Berlin, Germany.
Allais, Guillaume. / Generic level polymorphic N-ary functions. Paper presented at 4th ACM SIGPLAN International Workshop on Type-Driven Development, Berlin, Germany.13 p.
@conference{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 = "6",
day = "9",
language = "English",
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",

}

Allais, G 2019, 'Generic level polymorphic N-ary functions' Paper presented at 4th ACM SIGPLAN International Workshop on Type-Driven Development, Berlin, Germany, 18/08/19 - 18/08/19, .

Generic level polymorphic N-ary functions. / Allais, Guillaume.

2019. Paper presented at 4th ACM SIGPLAN International Workshop on Type-Driven Development, Berlin, Germany.

Research output: Contribution to conferencePaper

TY - CONF

T1 - Generic level polymorphic N-ary functions

AU - Allais, Guillaume

PY - 2019/6/9

Y1 - 2019/6/9

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

M3 - Paper

ER -

Allais G. Generic level polymorphic N-ary functions. 2019. Paper presented at 4th ACM SIGPLAN International Workshop on Type-Driven Development, Berlin, Germany.