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.