Séminaires des équipes de recherche
First Class Datatypes and their Ornaments
- Date : 12/01/2012
- Lieu : Inria - Rocquencourt - Salle de conférences du bâtiment 11
- Intervenant(s) : Conor McBride - University of Strathclyde
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.