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 Salle de conférences du bâtiment 11 JEUDI 12 janvier, 10h30 ------------- Conor McBride ------------- University of Strathclyde ========================================= First Class Datatypes and their Ornaments ========================================= As Epigram 2 continues its slow crawl into existence, it is acquiring a treatment of datatypes with first class descriptions (inhabiting a datatype with a description). This treatment offers us some new opportunities to compute the structure of data: we can compute the structure of indexed datatypes from their index values; we can characterise what it is to construct one datatype as a "fancy version" of an old one. By making the structure of datatypes a matter of systematic definition rather than artful declaration, we acquire a variety of useful, if mundane, programs and theorems for free. I'll argue for a direction of travel in which data are not seen as inherently and inferably typed, but rather checkable at a multitude of types. Hopefully, the multitude is not a mob, but a regiment.