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

Displayed time zone: Beirut change

11:00 - 12:30
Language extensionGPCE 2019 at Ground floor conference room
Chair(s): Adam Welc Uber Technologies
11:00
30m
Talk
Foreign language interfaces by code migration
GPCE 2019
Shigeru Chiba Graduate School of Information Science and Technology, The University of Tokyo
11:30
20m
Talk
A Language Feature to Unbundle Data at Will (Short Paper)
GPCE 2019
Musa Al-hassy McMaster University, Wolfram Kahl McMaster University, Jacques Carette McMaster University
11:50
20m
Talk
Parallel Nondeterministic Programming as a Language Extension to C (Short Paper)
GPCE 2019
Lucas Kramer University of Minnesota, Eric Van Wyk University of Minnesota, USA
DOI Pre-print
12:10
20m
Talk
Agile Construction of Data Science DSLs (Tool Demo)
GPCE 2019
Artur Andrzejak Heidelberg University, Kevin Kiefer , Diego Costa Heidelberg University, Oliver Wenz Heidelberg University