## Stephen J Bevan <stephenb@harlequin.co.uk>11 Jun 1998 16:12:20 -0400

From comp.compilers

Related articles
| List of all articles for this month |

 From: Stephen J Bevan 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
> I have been looking for an algorithm for this problem, but all
> literature found so far (robinson 1965, milner 1978, cardelli
> mentioned, but never included in the proposed solution.

The following might be useful :-

@inproceedings
{ Kaes:esop:1988
, author= "Stefan Kaes"
, crossref= "esop:1988"
, pages= "131--144"
, refs= 16
, checked= 19940827
, source= "Main Library, University of Manchester"
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
principal type property, thereby allowing the design of efficient type
inference algorithms. We present sound type deduction systems, both
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
, author= "P. Wadler and S. Blott"
, 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"
, 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
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"
, 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
only, that is, where the only overloading is that which exists in an
{\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
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"
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
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
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"
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