Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Lundi 10 février, 10h30 ----------------------- Pierre-Évariste Dagand ----------------------- INRIA ======================================== Ornaments: a calculus of data structures ======================================== With Conor McBride, I have studied inductive families in (dependent) type theory and the structural ties between them. Indeed, in a simply-typed language such as ML, a datatype is nothing but a "data-structure". The choice of a particular datatype (say, binary trees) versus another (say, lists) is mostly governed by performance considerations. In type theory, inductive families add a new dimension to datatypes: an inductive family is the combination of a data-structure (e.g., the binarily-branching structure of a tree) and a data-logic (e.g., to be of a certain height). Thanks to inductive families, we can define the datatype of vectors (lists of a given length), or balanced binary trees, etc. However, the choice of a particular data-logic is motivated by logical considerations: it lets the programmers enforce their invariants. This leads to an uncontrolled multiplication of similar yet incompatible datatypes: the same data-structure ends up being duplicated to account for its many logic-specific uses. In this talk, I will give a first-principles introduction to ornaments. To this end, I shall model indexed datatypes in the language of many-sorted signatures, in which data-structures and data-logics can be independently studied. I will then introduce a few constructions on ornaments, building up an actual "calculus of data-structures". From an operational standpoint, we shall build a toolbox for deriving datatypes from others.