Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E

                   ______                __    _               
                  / ____/___ _____ ___  / /_  (_)_  ______ ___ 
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ 

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                                   EN LIGNE

                           Lundi 9 novembre, 10h30

                               ----------------
                               Thierry Martinez
                               ----------------

                                 Inria Paris

                     ===================================
                     Type-safe type reflection for OCaml
                     ===================================

I will present the refl package (https://github.com/thierry-martinez/refl),
which provides type-safe type reflection for OCaml. This package uses
generalized algebraic datatypes (GADTs) and extensible variant types to encode
types and type declarations into values, covering most of the OCaml type
system, including GADTs.  The encoding of the type declarations into type
witnesses allows printers, serializers, visitors, to be defined as regular
functions parameterized by the type witnesses.  The encoding is uniform so as
to ensure separate compilation: type declarations and definitions of functions
that operate on corresponding type witnesses can span distinct modules and
be compiled separately.  Moreover, the encoding offers strong type safety
guarantees: the signature of functions can require that the type witnesses
satisfy some properties regarding parameter variance, type system features or
attributes.  On the other hand, the correctness and the completeness of these
functions is proved by type checking: values of the corresponding type are
constructed and destructed without any run-time check.