Jamie Gabbay: The design of the Nominal Datatypes package in Haskell

Time: Thursday, 29 April 2021, 9:30 Edinburgh time (UTC+1)

Abstract:

We’ll tour my Nominal techniques Haskell package, which provides easy access to types and type classes with nominal-style binding.

Why do you need this?  Because it lets you program and reason on name-like data (e.g. variable symbols, pointers, links), and binding (e.g. name-binding, hiding, locality) at the type-class level.  You instantiate to concrete datatype instances only when you want to; and the package takes care of the rest.

This means:

  • no more need for your functions to carry around “binding environments”, or “variable lookup functions”, or “binding contexts” (unless you want to), and no more need to engineer explicit renaming maps, or to correctly maintain separation invariants and thread them through your code;
  • pointers to substructures can be just pointers to substructures, and you can deference when you want to and practice information-hiding when you don’t — all efficiently, and without worrying (too much) about how it’s implemented;
  • common code patterns can be, and are, factored out as useful typeclasses;
  • it’s easier to notice and express algebraic code rewrites, including as properties for property-based tests;
  • tests and test-generators themselves are less dependent underlying representation and so can be easier to read, write, and maintain.

Furthermore, implementing nominal techniques is a stress-test both of

  • the language — can it do what we need it to do? if so, is the resulting code readable? does it add value overall? — and of
  • the maths — adapting mathematics to an executable environment can and does throw up ideas, due to an ambient notion of state and execution flow.  In the case of Haskell, this shows up as new monads and some cool new type classes.

This has wider implications.  Programmers care about clean code, and this gives us a success metric which can be detected in areas that are not obviously related to binding, if their internal representations would benefit from access to binding type classes.  Usually, this happens if it allows us to represent data at a higher level of abstraction and without committing to a concrete representation.  Examples include a reference blockchain implementation, programming on graphs, and constructing new kinds of automata.

I will walk through the package and, time permitting, discuss its broader implications and future work.

Live seminar links:

css.php

Report this page

To report inappropriate content on this page, please use the form below. Upon receiving your report, we will be in touch as per the Take Down Policy of the service.

Please note that personal data collected through this form is used and stored for the purposes of processing this report and communication with you.

If you are unable to report a concern about content via this form please contact the Service Owner.

Please enter an email address you wish to be contacted on. Please describe the unacceptable content in sufficient detail to allow us to locate it, and why you consider it to be unacceptable.
By submitting this report, you accept that it is accurate and that fraudulent or nuisance complaints may result in action by the University.

  Cancel