Séminaire des équipes de recherche
Refactoring ML programs using ornaments
- Date : 27/03/2017
- Lieu : 2 rue Simone Iff (ou: 41 rue du Charolais) - Salle Lions 1, bâtiment C - 10h30
- Intervenant(s) : Thomas Williams (Inria Paris)
Ornaments are a way to describe changes in datatype definitions that preserve their recursive structure, reorganizing, adding, or dropping some pieces of data. The relation between two types given by an ornament can be used to define a lifting relation between functions operating on a bare definition and functions operating on the ornamented structures. Thus, ornaments provide a way to specify the desired behaviour of a program refactored to work on an ornamented datatype.
In this talk, I will explain how ornaments can be used to partially (and sometimes totally) lift a function. I will present a prototype implementation of lifting along ornaments for a subset of OCaml and describe some use cases. I will explain how the lifting is carried out, and how we can prove the correctness of the process.