SpringerLink - Book Chapter

On the Unification of Substitutions in Type Inference

Book Series

Lecture Notes in Computer Science

Publisher

Springer Berlin / Heidelberg

ISSN

0302-9743 (Print) 1611-3349 (Online)

Volume

Volume 1595/1999

Book

Implementation of Functional Languages

DOI

10.1007/3-540-48515-5

1999

ISBN

978-3-540-66229-7

DOI

10.1007/3-540-48515-5_9

Pages

649-650

Subject Collection

Computer Science

SpringerLink Date

Friday, January 01, 1999

On the Unification of Substitutions in Type Inference

Bruce J. McAdam⁶

(6)	Laboratory for Foundations of Computer Science, The University of Edinburgh, USA

Abstract

The response of compilers to programs with type errors can be unpredictable and confusing. In part this is because the point at which type inference fails may not be the point at which the programmer has made a mistake. This paper explores a way of making type inference algorithms fail at different locations in programs so that clearer error messages may then be produced.

Critical to the operation of type inference algorithms is their use of substitutions. We will see that the way in which substitutions are applied in type inference algorithm W means that errors are detected towards the right-hand side of expressions. This paper introduces a new operation — unification of substitutions — which allows greater control over the use of substitutions so that this bias can be removed.

Bruce J. McAdam
Email: bjm@dcs.ed.ac.uk

On the Unification of Substitutions in Type Inference

Fulltext Preview (Small, Large)