Refinement types for the digital information age

Digitalization is, at least to some extent, the art of exchanging information electronically that formally was exchanged on paper. For exchanging structured electronic information, we have syntactic vehicles such as XML or JSON. Within a problem domain, pinning down the set of meaningful documents (the schema) is done with the aid of machine-readable languages that express properties and invariants, for example XSD and Schematron.
For the de-serialization boundary problem, that is, from document to in-memory representation, we have parsers. But what about the other direction? How can we make sure that data generated by our program meets all specifications? The property languages are meant to give rise to validators. But what if, instead, we used them to design a data type that has all properties and invariants baked in? Make illegal states unrepresentable, is the motto.

We demonstrate how, starting out from a naive translation of a schema,
one can construct a refinement type from a set of properties. We do this with the help of generic programming and explain how Stone duality can play an integral part of the process.

Olaf Klinke

Olaf Klinke is a mathematician and functional programming enthusiast. His post-academic career includes teaching episodes as well as building software in Haskell to drive the renewable energy revolution. Lately, revolutions in Germany are very orderly and bureaucratic. Therefore Olaf has been putting much thought into how to leverage mathematics and type systems to file taxes, send invoices and how to perform self-documenting computation.