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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:20 - 16:40
Generic Programming and SynthesisTyDe at Aurora Borealis
Chair(s): Edwin BradyUniversity of St. Andrews, UK
15:20
20m
Talk
Generic Enumerators
TyDe
Cas van der RestUtrecht University, Wouter SwierstraUtrecht University, Netherlands, Manuel ChakravartyTweag I/O & IOHK
Pre-print
15:40
20m
Talk
Generic Level Polymorphic N-ary Functions
TyDe
Guillaume AllaisUniversity of Strathclyde
Link to publication
16:00
20m
Talk
Augmenting Type Signatures for Program Synthesis
TyDe
Bruce CollieUniversity of Edinburgh, Michael F. P. O'BoyleUniversity of Edinburgh
Pre-print
16:20
20m
Talk
Constraint-based Type-directed Program Synthesis
TyDe
Peter-Michael OseraGrinnell College
Link to publication