From mboxrd@z Thu Jan 1 00:00:00 1970 Received: by pauillac.inria.fr; Fri, 7 Oct 94 20:51:39 +0100 Received: from concorde.inria.fr by pauillac.inria.fr; Thu, 6 Oct 94 18:24:49 +0100 Received: from margaux.inria.fr (margaux.inria.fr [128.93.8.2]) by concorde.inria.fr (8.6.9/8.6.9) with ESMTP id SAA27588 for ; Thu, 6 Oct 1994 18:24:48 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by margaux.inria.fr (8.6.8/8.6.6) with ESMTP id SAA26579 for ; Thu, 6 Oct 1994 18:24:45 +0100 Received: from nuada.uwaterloo.ca (root@nuada.uwaterloo.ca [129.97.78.59]) by concorde.inria.fr (8.6.9/8.6.9) with SMTP id SAA27584 for ; Thu, 6 Oct 1994 18:24:44 +0100 Received: by nuada.uwaterloo.ca id <158883>; Thu, 6 Oct 1994 13:24:39 -0400 From: Dominic Duggan To: caml-list@margaux.inria.fr Subject: technical report available: "kinded parametric overloading" Cc: dduggan@nuada.uwaterloo.ca, johno@latcs1.lat.oz.au Message-Id: <94Oct6.132439edt.158883@nuada.uwaterloo.ca> Date: Thu, 6 Oct 1994 13:24:33 -0400 Sender: weis@pauillac.inria.fr 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)