Write a Blog >>
GPCE 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
co-located with SPLASH 2019
Mon 21 Oct 2019 11:30 - 11:50 at Ground floor conference room - Language extension Chair(s): Adam Welc

Programming languages with sufficiently expressive type theories provide users with essentially two levels of data ‘bundling’. This applies in particular to dependently-typed languages such as Agda, Coq, and Idris, where one can choose to make certain constituents of a record either parameters or fields. For example, we can speak of graphs /over/ a particular vertex set, or speak of arbitrary graphs wherein the vertex set is a component. These create isomorphic types, but differ with respect to convenience. Traditionally, a library designer would make this choice between parameters and fields; if a user wants a different variant, they are forced to build conversion utilities as well as duplicate functionality. In our earlier example about graph datatypes, if a library only provides a Haskell-like typeclass view of graphs /over/ a vertex set, yet a user wishes to work with the category of graphs, they must now package a vertex set as a component in a record along with a graph over that set.

We design and implement a language feature that allows both the library designer and the user to make the choice of information exposure only when necessary and otherwise leave the distinguishing line between parameters and fields unspecified. Our language feature is currently prototypically implemented as a meta-program that is not only easily incorporated into Agda’s Emacs ecosystem, but is also unobtrusive to Agda users.

Mon 21 Oct (GMT+03:00) Beirut change

11:00 - 12:30: GPCE 2019 - Language extension at Ground floor conference room
Chair(s): Adam WelcUber Technologies
gpce-2019-papers11:00 - 11:30
Shigeru ChibaGraduate School of Information Science and Technology, The University of Tokyo
gpce-2019-papers11:30 - 11:50
Musa Al-hassyMcMaster University, Wolfram KahlMcMaster University, Jacques CaretteMcMaster University
gpce-2019-papers11:50 - 12:10
Lucas KramerUniversity of Minnesota, Eric Van WykUniversity of Minnesota, USA
DOI Pre-print
gpce-2019-papers12:10 - 12:30
Artur AndrzejakHeidelberg University, Kevin Kiefer, Diego CostaHeidelberg University, Oliver WenzHeidelberg University