Technical Report (TR98-02) Cover Page

Department of Information Science, Faculty of Science, University of Tokyo
Title:
Quasi-Linear Types
Authors:
Naoki Kobayashi
Key words and phrases:
linear type, memory management, use inference
Abstract:
Linear types (types of values that can be used just once) have been drawing a great deal of attention because they are useful for memory management, in-place update of data structures, etc.: an obvious advantage is that a value of a linear type can be immediately deallocated after being used. However, the linear types have not been applied so widely in practice, probably because linear values (values of linear types) in the traditional sense do not so often appear in actual programs. In order to increase the applicability of linear types, we relax the condition of linearity by extending the types with information on an evaluation order and simple dataflow information. The extended type system, called a quasi-linear type system, is formalized and its correctness is proved. We have implemented a prototype type inference system for the core-ML that can automatically find out which value is linear in the relaxed sense. Promising results were obtained from preliminary experiments with the prototype system.
Report date:
September, 1998
Written language:
English
Total number of pages:
40
Number of references:
21
Any other identifying information of this report:
A revised version of this paper will be available here .
Distribution statement:
First issue 35 copies.
Supplementary notes: