Observers for Linear Types Export

@inproceedings{citeulike:5652205, abstract = {Linear types provide the framework for a safe embedding of mutable state in functional languages by enforcing the principle that variables of linear type must be used exactly once. A potential disadvantage of this approach is that it places read accesses to suchvariables under the same restriction as write accesses, and thus prevents reads to proceed in parallel. We present here an extension of linear types which augments the usual distinction between linear and non-linear bya third state, observers of linear variables. Since, unlike linear variables, observers can be duplicated, multiple concurrent reads are made possible. On the other hand, observers must be short-lived enough to never overlap with mutations. The resulting type system is in many aspects similar to the one of ML: It is polymorphic, has principal types, and admits a type reconstruction algorithm. 1 Introduction We are investigating a type system that addresses the update problem in functional languages: How...}, author = {Odersky, Martin}, booktitle = {ESOP '92: 4th European Symposium on Programming, Rennes, France, Proceedings}, citeulike-article-id = {5652205}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.245}, keywords = {pl, substructural, types}, pages = {390--407}, posted-at = {2009-08-26 21:12:20}, priority = {0}, title = {Observers for Linear Types}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.245}, volume = {582}, year = {1992} }

TY - CONF ID - citeulike:5652205 L3 - citeulike-article-id:5652205 N2 - Linear types provide the framework for a safe embedding of mutable state in functional languages by enforcing the principle that variables of linear type must be used exactly once. A potential disadvantage of this approach is that it places read accesses to suchvariables under the same restriction as write accesses, and thus prevents reads to proceed in parallel. We present here an extension of linear types which augments the usual distinction between linear and non-linear bya third state, observers of linear variables. Since, unlike linear variables, observers can be duplicated, multiple concurrent reads are made possible. On the other hand, observers must be short-lived enough to never overlap with mutations. The resulting type system is in many aspects similar to the one of ML: It is polymorphic, has principal types, and admits a type reconstruction algorithm. 1 Introduction We are investigating a type system that addresses the update problem in functional languages: How... EP - 407 TI - Observers for Linear Types VL - 582 T2 - ESOP ’92: 4th European Symposium on Programming, Rennes, France, Proceedings SP - 390 KW - pl KW - substructural KW - types AU - Odersky, Martin PY - 1992/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.245 ER -