Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 15:40 - 16:00 at Aurora Borealis - Generic Programming and Synthesis Chair(s): Edwin Brady

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.

Sun 18 Aug

tyde-2019-papers
15:20 - 16:40: TyDe 2019 - Generic Programming and Synthesis at Aurora Borealis
Chair(s): Edwin BradyUniversity of St. Andrews, UK
tyde-2019-papers15:20 - 15:40
Talk
Cas van der RestUtrecht University, Wouter SwierstraUtrecht University, Netherlands, Manuel ChakravartyTweag I/O & IOHK
Pre-print
tyde-2019-papers15:40 - 16:00
Talk
Guillaume AllaisUniversity of Strathclyde
Link to publication
tyde-2019-papers16:00 - 16:20
Talk
Bruce CollieUniversity of Edinburgh, Michael O'BoyleUniversity of Edinburgh
Pre-print
tyde-2019-papers16:20 - 16:40
Talk
Peter-Michael OseraGrinnell College
Link to publication