Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Fri 28 Aug 2020 13:00 - 13:30 at OCaml - Experience Chair(s): Greta Yorsh

Coda is a new cryptocurrency that uses zk-SNARKs to dramatically reduce the size of data needed by nodes running its protocol. Nodes communicate in a format automatically derived from type definitions in OCaml source files. As the Coda software evolves, these formats for sent data may change. We wish to allow nodes running older versions of the software to communicate with newer versions. To achieve that, we identify stable types that must not change over time, so that their serializations also do not change.

To enforce the stability of types, we use three OCaml extension point (“ppx”) implementations. One ppx is a linter that enforces usage patterns of stable types. For example, the linter enforces that all serialized types are marked as versioned, and that serialized types cannot be generated by functor applications. Another ppx marks types as versioned. The typechecker assures that such types are made up only of other versioned types, even when they’re defined in other files. Errors flagged by the linter and version ppx are made visible in editors running the Merlin tool for OCaml.

The last ppx allows marking a module of stable types and generating boilerplate definitions, including annotations to indicate that the contained types are serializable and versioned. Serialized data contains an automatically-generated version byte that identifies a particular version, which we can deserialize and transform to the latest version.

Coda developers are aware that stable types should not be modified, but mistakes can happen. We can run the version ppx in a special way to print out representations of versioned types. A script in the Coda continuous integration setup uses that facility to compare versioned types in Github pull requests, and flags inadvertent changes.

By combining these techniques, we propose a simple and flexible strategy for future-compatible communication in OCaml.

Fri 28 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

11:30 - 13:30: ExperienceOCaml at OCaml
Chair(s): Greta YorshJane Street

Sharing experience about using OCaml in various scenarios.

11:30 - 12:00
OCaml Under The Hood: SmartPy
12:00 - 12:30
A Declarative Syntax Definition for OCaml
Luis Eduardo de Souza AmorimDelft University of Technology, Netherlands, Eelco VisserDelft University of Technology
12:30 - 13:00
LexiFi Runtime Types
Patrik KellerUniversity of Innsbruck, Marc LassonLexiFi
13:00 - 13:30
Types in amber
Paul StecklerO(1) Labs, Matthew RyanO(1) Labs