Re: Type-checking with polymorphism & overloading

<hat@se-46.wpa.wtb.tue.nl> writes:
> I am working on building a type-checking system for a language which
> has both polymorphism and overloading, and compile-time type checking.
> I have been looking for an algorithm for this problem, but all
> literature found so far (robinson 1965, milner 1978, cardelli
> 1986(1987?)) assumes polymorphism only. Overloading is sometimes
> mentioned, but never included in the proposed solution.


The following might be useful :-


@inproceedings
{ Kaes:esop:1988
, author= "Stefan Kaes"
, title= "Parametric overloading in polymorphic programming languages"
, crossref= "esop:1988"
, pages= "131--144"
, refs= 16
, checked= 19940827
, source= "Main Library, University of Manchester"
, abstract= "The introduction of unrestricted overloading in languages
with type systems based on implicit parametric polymorphism generally
destroys the principal type property: namely that the type of every
expression can uniformly be represented by a single type expression
over some set of type variables. As a consequence, type inference in
the presence of unrestricted overloading can become a NP-complete
problem. In ths paper we define the concept of parametric overloading
as a restricted form of overloading which is easily combined with
parametric polymorphism. Parametric overloading preserves the
principal type property, thereby allowing the design of efficient type
inference algorithms. We present sound type deduction systems, both
for predefiend and programmer defined overloading. Finally we state
that parametric overloading can be resolved either statically, at
compile time, or dynamically, during program execution."
, reffrom= Nipkow:Snelting:fplca:1991
, reffrom= Volpano:Smith:fplca:1991
, reffrom= Morrison:Dearle:Connor:Brown:acm:toplas:1991
, reffrom= Snelting:acta:1991
, reffrom= Chen:Hudak:Odersky:acm:lfp:1992
, reffrom= Duggan:Sourelis:acm:icfp:1996
}


@inproceedings
{ esop:1988
, editor= "H. Ganzinger"
, title= "Proceedings of the European Symposium on Programming"
, booktitle= "Proceedings of the European Symposium on Programming"
, publisher= "Springer Verlag"
, series= lncs
, volume= 300
, year= 1988
}




@inproceedings
{ Wadler:Blott:acm:popl:1989
, author= "P. Wadler and S. Blott"
, title= "How to make ad hoc polymorphism less ad hoc"
, pages= "60--76"
, crossref= "acm:popl:1989"
, reffrom= Nipkow:Snelting:fplca:1991
, reffrom= Volpano:Smith:fplca:1991
, reffrom= Leroy:Mauny:fplca:1991
, reffrom= Morrison:Dearle:Connor:Brown:acm:toplas:1991
, reffrom= Snelting:acta:1991
, reffrom= Chen:Hudak:Odersky:acm:lfp:1992
, reffrom= Gastagna:Ghelli:Longo:acm:lfp:1992
, reffrom= Appel:cwc:1992
, reffrom= Berry:jfp:1993
, reffrom= Jones:afp:1995
, reffrom= Thiemann:spe:1997
}




@proceedings
{ acm:popl:1989
, title= "Conference Record of the 16th Annual ACM Symposium
on Principles of Programming Languages"
, booktitle= "Conference Record of the 16th Annual ACM Symposium
on Principles of Programming Languages"
, organization= "ACM"
, publisher= "ACM"
, month= jan
, year= 1989
}




@inproceedings
{ Nipkow:Snelting:fplca:1991
, author= "Tobias Nipkow and Gregor Snelting"
, email= "Tobias.Nipkow@cl.cam.ac.uk and snelting@pi.informatik.th-darmstadt.de"
, title= "Type Classes and Overloading Resolution via Order-Sorted Unification"
, crossref= "fplca:1991"
, pages= "1--14"
, refs= 16
, checked= 19940809
, source= "Main Library, University of Manchester"
, abstract= "We present a type inference algorithm for a Haskell-like
language based on order-sorted unification. The language features
polymorphism, overloading, type classes and multiple inheritance.
Classes and instance declarations give rise to an order-sorted algebra
of types. Type inference essentially reduces to the Hindly/Milner
algorithm where unification takes place in this order-sorted algebra
of types. The theory of order-sorted unification provides simple
sufficient conditions which ensure the existence of principal types.
The semantics of the language is given by a translation into ordinary
$\lambda$-calculus. We prove the correctness of our type inference
algorithm with respect to this semantics."
, reffrom= Chen:Hudak:Odersky:acm:lfp:1992
}






@inproceedings
{ Volpano:Smith:fplca:1991
, author= "Dennis M. Volpano and Geoffrey S. Smith"
, title= "On the Complexity of ML Typability with Overloading"
, crossref= "fplca:1991"
, pages= "15--28"
, refs= 12
, checked= 19940809
, source= "Main Library, University of Manchester"
, abstract= "We example [typo on my part - sjb] the complexity of type
checking in an ML-style type system that permits functions to be
overloaded with different types. In particular, we consider the
extension of the ML type system proposed by Wadler and Blott in the
appendix of~\cite{Wadler:Blott:acm:popl:1989}, with global overloading
only, that is, where the only overloading is that which exists in an
initial type assumption set; no local overloading via {\em over} and
{\em inst} expressions is allowed. It is shown that under a correct
notion of well-typed terms, the problem of determining whether a term
is well typed with respect to an assumption set in this system is
undecidable. We then investigate limiting recursion in assumption
sets, the source of the undecidability. Barring mutual recursion is
considered, but this proves too weak, for the problem remains
undecidable. Then we consider a limited form of recursion called {\em
parametric recursion}. We show that although the problem becomes
decidable under parametric recursion, it appears harder than
conventional ML typability, which is complete for
DEXPTIME~\cite{Mairson:acm:popl:1990}."
, reffrom= Chen:Hudak:Odersky:acm:lfp:1992
}




@proceedings
{ fplca:1991
, editor= "John Hughes"
, title= "Functional Programming Languages and Computer Architecture"
, booktitle= "Functional Programming Languages and Computer Architecture"
, publisher= "Springer Verlag"
, month= jun
, year= 1991
, note= "LNCS 523."
}




@article
{ Morrison:Dearle:Connor:Brown:acm:toplas:1991
, author= "R. Morrison and A. Dearle and R. C. H. Connor and A. L. Brown"
, title= "An Ad Hoc Approach to the Implementation of Polymorphism"
, journal= acm:toplas
, volume= 13
, number= 3
, pages= "342--371"
, month= jul
, year= 1991
, cr= "9208-0590"
, refs= 42
, checked= 19951225
, source= "Main Library, University of Manchester"
, abstract= "Polymorphic abstraction provides the ability to write
programs that are independent of the form of the data over which they
operate. There are a number of different categories of polymorphic
expression -- ad hoc and universal, which includes parametric and
inclusion -- all of which have many advantages in terms of code reuse
and software economics. It has proved difficult to provide efficient
implementations of polymorphism. Here, we address this problem and
describe a new technique that can implement all forms of polymorphism,
use a conventional machine architecture, and support nonuniform data
representations. Furthermore, the method ensures that any extra cost
of implementation applies to polymorphic forms only, and allows such
polymorphic forms to persist over program invocations."
}




@inproceedings
{ Chen:Hudak:Odersky:acm:lfp:1992
, author= "Kung Chen and Paul Hudak and Martin Odersky"
, title= "Parametric Type Classes (Extended Abstract)"
, crossref= "acm:lfp:1992"
, pages= "170--181"
, refs= 19
, checked= 19950126
, source= "Computer Science Library, University of Manchester"
, abstract= "We propose a generalization to Haskell's type classes
where a class can have type parameters besides the placeholder
variable. We show that this generalization is essential to represent
container classes with overloaded data constructor and selector
operations. We also show that the resulting type system has principal
types and present unification and type reconstruction algorithms."
}




@inproceedings
{ Gastagna:Ghelli:Longo:acm:lfp:1992
, author= "Guiseppe Castagna and Giorgio Ghelli and Guiseppe Longo"
, title= "A Calculus for Overloaded Functions with Subtyping (extended abstract)"
, crossref= "acm:lfp:1992"
, pages= "182--192"
, refs= 23
, checked= 19950128
, source= "Computer Science Library, University of Manchester"
, abstract= "We present a simple extension of typed $\lambda$-calculus
where functions can be {\em overloaded} by ading different ``pieces of
code''. In short, the code of an overloaded function is formed by
several branches of code; the branch to execute is chosen, when the
function is applied, according to a particular selection rule which
depends on the type of the argument. The crucial feature of the
present approach is that a subtyping relation is defined among types,
such that the type of a term generally decreases during computation,
and this fact induces a distinction between the ``compile-time'' type
and the ``run-time'' type of a term. We study the case of overloaded
functions where the branch selection depends on the run-time type of
the argument, so that overloading cannot be eliminated by a static
analysis of code, but is an essential feature to be dealt with during
computation. We obtain in this way a type-dependent calculus, which
differs from the various $\lambda$-calculi where types do not play,
essentially, any r{\^o}le during computation. We prove Confluence and
Strong Normalization for this calculus as well as a generalized
Subject-Reduction theorem (but proofs are ommited in this abstract).


The definition of this calculus is driven by the understandingn of
object-oriented features and the connections between our calculus and
object-orientedness are extensively stressed. We show that this
calculus provides a foundation for typed object-oriented languages
which solves some of the problems of the standard record-based
approach. It also provides a type discipline for a relevant fragment
of the ``core framework'' (see~\cite{Keene:1989}) of CLOS."
}




@inproceedings
{ Kaes:acm:lfp:1992
, author= "Stefan Kaes"
, email= "kaes@pi.informatik.th-darmstadt.de"
, title= "Type Inference in the Presence of Overloading, Subtyping
and Recursive Types"
, crossref= "acm:lfp:1992"
, pages= "193--204"
, refs= 24
, checked= 19950126
, source= "Computer Science Library, University of Manchester"
, abstract= "We present a unified approach to type inference in the
presence of overloading and coercions based on the concept of {\em
constrained types}. We define a generic inference system, show that
subtyping and overloading can be treated as a special instance of this
system and develop a simple algorithm to compute principal types. We
prove the decidability of type inference for the class of {\em
decomposable predicates} and develop a canonical representation for
principal types based on {\em most accurate simplifications} of
constraint sets. Finally, we investigate the extension of our
techniques to {\em recursive types}."
, reffrom= Wright:Cartwright:acm:lfp:1994
}




@proceedings
{ acm:lfp:1992
, title= "1992 ACM Conferenc on Lisp and Functional Programming"
, booktitle= "1992 ACM Conferenc on Lisp and Functional Programming"
, organization= "ACM"
, publisher= "ACM"
, month= aug
, year= 1992
}




@phdthesis
{ Jones:phd:1992
, author= "Mark Philip Jones"
, title= "Qualified Types: Theory and Practice"
, school= "Oxford University"
, month= jul
, year= 1992
, pages= 176
, checked= 19940320
, supervisor= "Robert Bird and Bernard Sufrin"
, source= "Computer Science Library, University of Manchester"
, note= "Also available as Programming Research Group technical
report 106"
, abstract= "This thesis describes a type system that combines
ML-style polymorphism with a general approach to overloading. The
centeral idea is to use qualified types that include predicates and
restrict the set of types at which an object can be used to particular
instances of a polymorphic type. Different applications of qualified
types can be obtained by changing the underlying system of predicates.
We illustate this with examples including type classes, explicit
subtyping and extensible records.


Much of the thesis deals with a simple, implicitly typed, functional
language. Extending the Damas/Milner approach to type inference, we
define an ordering between the constrainted type schemes used in our
system and show that the set of all possible typings for a give germ
has a greatest element with respect to this ordering. Furthermore,
this principal type scheme can be calculated using a type inference
algorithm.


Using an abstract notion of evidence, we show how the meaning of a
program in this system can be described by translating it into a
language that includes constructions for manipulating evidence values.
Since any term may have many distinct translations it is necessary to
give coherence conditions which guarantee that the meaning of a term
is well defined. This thesis intrduces a new technique for
establishing results of this kind, using a semantic interpretation of
the ordering relation on type schemes.


We also address more practical issues concerning the use of qualified
types, both for the general system and for specific applications.
This includes a promising new representation of extensible records,
based on the use of evidence. In addition, we describe the
implementation of type classes in Haskell and Gofer, an experimental
system developed by the author."
}




@inproceedings
{ Jones:fplca:1993
, author= "Mark P. Jones"
, title= "A system of constructor classes: overloading and implicit
higher-order polymorphism"
, crossref= "fplca:1993"
, pages= "1--10"
, reffrom= Jones:Duponcheel:yale:1004:1993
, reffrom= Jones:afp:1995
, reffrom= Duggan:Sourelis:acm:icfp:1996
}




@proceedings
{ fplca:1993
, title= "Functional Programming Languages and Computer Architecture"
, booktitle= "Functional Programming Languages and Computer Architecture"
, month= jun
, year= 1993
}
--

Return to the comp.compilers page.
Search the comp.compilers archives again.