A type system with usage aspects

David Aspinall, Martin Hofmann, Michal Konečný

Research output: Contribution to journalArticle

Abstract

Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a read-only context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konen'y (In TYPES 2002 workshop, Nijmegen, Proceedings, Springer-Verlag, 2003).
Original languageEnglish
Pages (from-to)141-178
Number of pages38
JournalJournal of Functional Programming
Volume18
Issue number2
DOIs
Publication statusPublished - Mar 2008

Fingerprint

Semantics
Static analysis

Bibliographical note

Aspinall, D, Hofmann, M & Konecný, M 2008, 'A type system with usage aspects', Journal of functional programming, vol 18, no. 2, pp. 141-178.
http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=1695688

Cite this

Aspinall, David ; Hofmann, Martin ; Konečný, Michal. / A type system with usage aspects. In: Journal of Functional Programming. 2008 ; Vol. 18, No. 2. pp. 141-178.
@article{576d8d9ad4014532aa993e76de1f20b8,
title = "A type system with usage aspects",
abstract = "Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a read-only context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konen'y (In TYPES 2002 workshop, Nijmegen, Proceedings, Springer-Verlag, 2003).",
author = "David Aspinall and Martin Hofmann and Michal Konečn{\'y}",
note = "Aspinall, D, Hofmann, M & Konecn{\'y}, M 2008, 'A type system with usage aspects', Journal of functional programming, vol 18, no. 2, pp. 141-178. http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=1695688",
year = "2008",
month = "3",
doi = "10.1017/S0956796807006399",
language = "English",
volume = "18",
pages = "141--178",
journal = "Journal of Functional Programming",
issn = "0956-7968",
publisher = "Cambridge University Press",
number = "2",

}

A type system with usage aspects. / Aspinall, David; Hofmann, Martin; Konečný, Michal.

In: Journal of Functional Programming, Vol. 18, No. 2, 03.2008, p. 141-178.

Research output: Contribution to journalArticle

TY - JOUR

T1 - A type system with usage aspects

AU - Aspinall, David

AU - Hofmann, Martin

AU - Konečný, Michal

N1 - Aspinall, D, Hofmann, M & Konecný, M 2008, 'A type system with usage aspects', Journal of functional programming, vol 18, no. 2, pp. 141-178. http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=1695688

PY - 2008/3

Y1 - 2008/3

N2 - Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a read-only context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konen'y (In TYPES 2002 workshop, Nijmegen, Proceedings, Springer-Verlag, 2003).

AB - Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a read-only context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konen'y (In TYPES 2002 workshop, Nijmegen, Proceedings, Springer-Verlag, 2003).

UR - http://www.scopus.com/inward/record.url?scp=38949199387&partnerID=8YFLogxK

U2 - 10.1017/S0956796807006399

DO - 10.1017/S0956796807006399

M3 - Article

AN - SCOPUS:38949199387

VL - 18

SP - 141

EP - 178

JO - Journal of Functional Programming

JF - Journal of Functional Programming

SN - 0956-7968

IS - 2

ER -