11 Jun 1998 16:12:20 -0400

Related articles |
---|

Type-checking with polymorphism & overloading hat@se-46.wpa.wtb.tue.nl (1998-06-09) |

Re: Type-checking with polymorphism & overloading tkb@access.mountain.net (1998-06-11) |

Re: Type-checking with polymorphism & overloading stephenb@harlequin.co.uk (Stephen J Bevan) (1998-06-11) |

Re: Type-checking with polymorphism & overloading ast@halcyon.com (1998-06-11) |

Re: Type-checking with polymorphism & overloading jsm@it.dtu.dk (Jørgen Steensgaard) (1998-06-11) |

Re: Type-checking with polymorphism & overloading ceebds@cee.hw.ac.uk (Ben Speight) (1998-06-11) |

Re: Type-checking with polymorphism & overloading fjh@cs.mu.OZ.AU (1998-06-18) |

Re: Type-checking with polymorphism & overloading hat@se-46.wpa.wtb.tue.nl (1998-06-24) |

From: | Stephen J Bevan <stephenb@harlequin.co.uk> |

Newsgroups: | comp.compilers |

Date: | 11 Jun 1998 16:12:20 -0400 |

Organization: | Harlequin Ltd., Manchester, UK. |

References: | 98-06-041 |

Keywords: | types, bibliography, polymorphism |

<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

*}*

--

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.