Browse Prior Art Database

Types as Intervals

IP.com Disclosure Number: IPCOM000128272D
Original Publication Date: 1984-Dec-31
Included in the Prior Art Database: 2005-Sep-15

Publishing Venue

Software Patent Institute

Related People

Robert Cartwrightt: AUTHOR [+3]

Abstract

To accommodate polymorphic data types and operations, several computer scientists-most notably MacQueen, Plotkin, and Sethi-have proposed formalizing types as ideals. Although this approach is intuitively appealing, the resulting type system is both complex and restrictive because the type constructor that creates function types is not monotonic, and hence not computable. As a result, types cannot be treated as data values, precluding the formalization of type constructors and polymorphic program modules (where types are values) as higher order computable functions. Moreover, recursive definitions of new types do not necessarily have solutions.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 5% of the total text.

Page 1 of 45

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Types as Intervals

Robert Cartwrightt

Rice COMP TR84-5

Department of Computer Science Rice University P.O. Box 1892 Houston, TX 77251-1892

(713) 527-8101

,This research was oerformed while the author was a visiting professor at Carnegie-Mellon University and has been Dar-tiaily supported by DARPA Order No. 3597, monitored by the Air Force Avionics Laboratory under Contract F33615-8-K-, 539. Types as Intervals

Robert Cartwrightt

Computer Science Department Rice University Houston, TX 77251

Abstract

To accommodate polymorphic data types and operations, several computer scientists-most notably MacQueen, Plotkin, and Sethi-have proposed formalizing types as ideals. Although this approach is intuitively appealing, the resulting type system is both complex and restrictive because the type constructor that creates function types is not monotonic, and hence not computable. As a result, types cannot be treated as data values, precluding the formalization of type constructors and polymorphic program modules (where types are values) as higher order computable functions. Moreover, recursive definitions of new types do not necessarily have solutions.

This paper proposes a new formulation of types-called intervals-that subsumes the theory of types as ideals, yet avoids the pathologies caused by non-monotonic type constructors. In particu-lar, the set of interval types contains the set of ideal types as a proper subset and all of the primi-tive type operations on intervals are extensions of the corresponding operations on ideals. Nevertheless, all of the primitive interval type constructors including the function type constructor and type quantifiers are computable operations. Consequently, types are higher order data values that can be freely manipulated within programs.

The key idea underlying the formulation of types as intervals is that negative information should be included in the description of a type. Negative information identifies the finite elements that do not belong to a type, just as conventional, positive information identifies the elements that do. Unless the negative information in a type description is the exact complement of the positive information, the description is partial in the sense that it approximates many different types--an interval of ideals between the positive information and the complement of the negative information. Although programmers typically deal with total (maximal) types, partial types appear to be an essential feature of a comprehensive polymorphic type system that accommodates types as data, just as partial functions are essential in any universal programming language.

Rice University Page 1 Dec 31, 1984

Page 2 of 45

Types as Intervals

1. Introduction

One of the major unresolved questions in programming language design is how to define the notion of data type. This paper focuses on type systems for abstract programming languages (e.g., S...