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 réunion du bâtiment 11 VENDREDI 10 juin, 10h30 ---------------- Jacques Garrigue ---------------- Université de Nagoya ========================================== Adding GADTs to OCaml: the direct approach ========================================== Generalized Algebraic Datatypes, or GADTs, extend algebraic datatypes by allowing an explicit relation between type parameters and case analysis. They have useful applications, among others for encoding invariants of data structures, or providing tag-less data representations. We have implemented them in OCaml, by directly modifying the type inference engine. We discuss the technical choices involved, and the properties expected to hold. In particular, we have worked on two aspects of inference: principality, which holds only by requiring some derivations to be minimal, and exhaustiveness of pattern-matching, which requires a new notion of incompatibility. (Joint work with Jacques Le Normand.)