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