Séminaire Cambium, Inria Paris
                               Salle Paul Erdös
                           Mardi 2 décembre, 10h30

                               Alistair O'Brien
                           University of Cambridge

         Omnidirectional type inference for ML: principality any way

At the heart of the Damas-Hindley-Milner (ML) type system lies the ability to
guess types. For instance, in `fun x -> e`, the parameter type for `x` is
guessed and subsequently constrained by the body of `e`. The elegance of the
ML discipline is that such guesses are never arbitrary: there always exists a
"most general" or principal type---ensuring that every well-typed expression
has a unique principal type, a property known as principality. This guarantees
both predictability and efficiency of inference: local typing decisions are
globally optimal without resorting to backtracking. Principality, however, is
fragile: many extensions of ML---GADTs, higher-rank polymorphism, and static
overloading---break it by introducing fragile constructs that resist principal
inference. Existing approaches recover principality through directional
inference algorithms, which propagate known type information in a fixed (or
static) order (e.g. as in bidirectional typing) to disambiguate such
constructs. However, the rigidity of a static inference order often causes
otherwise well-typed programs to be rejected.

In this talk, I will present omnidirectional type inference, an approach where
type information flows in a dynamic order. Typing constraints may be solved in
any order, suspending when progress requires known type information and
resuming once it becomes available (typically via unification). This approach
comes naturally for simply typed systems, but becomes challenging in the
presence of ML-style local let-generalization. In existing ML inference
algorithms, typing a let-binding `let x = e1 in e2` follows a static order:
first type `e1`, then generalize its type, and finally type the body `e2`
under the extended environment. To break this static ordering, we introduce
incremental instantiation, allowing partially solved type schemes containing
suspended constraints to be instantiated, with a mechanism to incrementally
update instances as the scheme is refined. Omnidirectionality provides a
general framework for restoring principality in the presence of fragile
features. We demonstrate its versatility on two fundamentally different
features of OCaml: (1) static overloading of record labels and datatype
constructors and (2) semi-explicit first-class polymorphism. In both cases, we
obtain a principal type inference algorithm that is more expressive than
OCaml's current typechecker.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.