technical report available: "kinded parametric overloading"

technical report available: "kinded parametric overloading"

[Dominic Duggan]

Readers of this mailing list may be interested in the following
technical report, which has been submitted to a journal.  
Although not the main point of the paper, we thought some people
might be amused by the following application, which we understand
was the subject of some discussion on this mailing list some time back.

-----------------------------------------------------------------------

Consider = defined for integers, strings, chars and sets.
Under our type system = is overloaded with the type:

    K{=} >= {int, string, char, K{=} set}
    =  :  'a * 'a -> bool

Suppose specialized instances of = are defined for sets of integers
and sets of chars. This is possible in our type system (without 
ambiguity), giving the type of = as:

    K{=} >= {int, string, char, int set, char set, 
             (K{=} set) \ {int set, char set}}
    =  :  'a * 'a -> bool

After some normalization, this becomes:

    K{=} >= {int, string, char, int set, char set, 
             (K{=} \ {int,char}) set}
    =  :  'a * 'a -> bool

The paper discusses a mechanism for ``closing up'' such a type.
Using this mechanism, = can be given the ``closed type'':

    =  :  'a * 'a -> bool
    where 'a : k
          k  = {int, string, char, int set, char set, k' set}
          k' = {string, int set, char set, k' set}

-----------------------------------------------------------------------

Details of the paper follow:

@TechReport{overload:DO94:kinds,
  author =       "Dominic Duggan and John Ophel",
  title =        "Kinded Parametric Overloading",
  institution =  "University of Waterloo, Department of Computer Science",
  year =         1994,
  number =       {CS-94-35},
  month =        "September",
  note =         {Supersedes CS-94-15 and CS-94-16, March 1994, and CS-93-32,
                  August 1993} 
}

Abstract:

The combination of overloading and parametric polymorphism has received some
attention in the functional programming community.  The main approach has been
that of Haskell type classes.  An approach to the type-checking and semantics
of parametric overloading is presented, based on using structured types to
constrain type variables.  {\em Open kinds} constrain type variables by sets of
operations and are useful for the incremental development of reusable
procedures (in a similar manner to Haskell classes), while {\em closed kinds}
constrain type variables by sets of types (essentially providing a type-safe
form of dynamic typing).  The type system includes a rule for ``closing up'' an
open kind to a closed kind.  Applications of these faciities include local
overloading, the combination of parametric overloading with a Standard ML-like
module system, and an optimization which replaces call-site closure
construction with dynamic dispatching based on explicit type tags.  A set
difference operation for kinds allows the unambiguous typing of overlapping
overload instances.  The system of kinds is provided in some detail.  A type
system and type inference algorithm are sketched.  An operational semantics is
provided and used to verify semantic soundness.  This operational semantics is
also used to verify the correctness of the removal of call-site closure
construction.

-------------------------------------------------------------------------------

The paper may be retrieved at either of the following addresses:

        http://nuada.uwaterloo.ca/dduggan/papers.html#kinds-paper
        ftp://nuada.uwaterloo.ca/pub/papers/kinded-parametric-overloading.ps.gz

Regards,
  Dominic Duggan (dduggan@uwaterloo.ca)
  John Ophel (johno@lucinda.lat.oz.au)