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.

Video of the talk: https://youtu.be/yrEwdGbb_Jg

Jamie Gabbay: The design of the Nominal Datatypes package in Haskell / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0