To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Cristal - 03/12/04 - Paris - FR

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

                             S E M I N A I R E
       ___      .                       
      /    ___   __  /_  _   /             /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /    -----    / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                     Salle de conférences du bâtiment 7

                         Vendredi 3 decembre, 10h30

                                 ---------
                                 Barry Jay
                                 ---------

                                UTS, Sydney

                            ===================
                            Unifiable Subtyping
                            ===================


Pattern-matching algorithms can support more algorithms, and more
polymorphism, than previously realised. Typing of such powerful
algorithms requires novel type derivation rules. A key insight is that
different cases in a patternmatch may have different types, provided
that they are all specialisations of a common default type. Two forms
of specialisation have been identified. The first is by type variable
instantiation. It allows one to define map1 : (a->b) -> c a -> c b by
cases whose types instantiate the variable c to different type
combinators. The second is by (unifiable) subtyping which eliminates
many of the difficulties usually associated with subtyping.

For P->S to be a unifiable subtype of Q -> T it suffices

        sigma P = sigma Q  implies sigma S < sigma T

for any type substitution sigma. When this holds it is possible to
combine cases of types P->S and Q->T into a pattern-matching
function. In paticular, it is possible to add new cases to existing
methods in a sub-class. Since function arguments are handled by type
unification instead of subtyping there is no contravariance problem,
and so no need for dynamic typecasts etc.

These ideas, and the pattern calculus as a whole, will be addressed,
using implemented examples to illustrate.