article

Erratic fudgets: a semantic theory for an embedded coordination language

Authors:

Andrew Moran,

David Sands,

Magnus CarlssonAuthors Info & Claims

Science of Computer Programming, Volume 46, Issue 1-2

Pages 99 - 135

https://doi.org/10.1016/S0167-6423(02)00088-6

Published: 01 January 2003 Publication History

Abstract

The powerful abstraction mechanisms of functional programming languages provide the means to develop domain-specific programming languages within the language itself. Typically, this is realised by designing a set of combinators (higher-order reusable programs) for an application area, and by constructing individual applications by combining and coordinating individual combinators. This paper is concerned with a successful example of such an embedded programming language, namely Fudgets, a library of combinators for building graphical user interfaces in the lazy functional language Haskell. The Fudget library has been used to build a number of substantial applications, including a web browser and a proof editor interface to a proof checker for constructive type theory. This paper develops a semantic theory for the non-deterministic stream processors that are at the heart of the Fudget concept. The interaction of two features of stream processors makes the development of such a semantic theory problematic: (i) the sharing of computation provided by the lazy evaluation mechanism of the underlying host language, and (ii) the addition of non-deterministic choice needed to handle the natural concurrency that reactive applications entail We demonstrate that this combination of features in a higher-order functional language can be tamed to provide a tractable semantic theory and induction principles suitable for reasoning about contextual equivalence of Fudgets.

References

[1]

{1} G.A. Agha, I.A. Mason, S.F. Smith, C.L. Talcott, A foundation for actor computation, J. Functional Program. 7 (1997) 1-72.]]

Digital Library

Google Scholar

[2]

{2} F. Arbab, I. Herman, P. Spilling, An overview of MANIFOLD and its implementation, Concurrency: Practice Exper. 5 (1) (1993) 23-70.]]

Digital Library

Google Scholar

[3]

{3} Z.M. Ariola, M. Felleisen, The call-by-need lambda calculus, J. Functional Program. 7 (3) (1997) 265-301.]]

Digital Library

Google Scholar

[4]

{4} Z. Ariola, M. Felleisen, J. Maraist, M. Ordersky, P. Walder, A call-by-need lambda calculus, in: Proc. POPL'95, ACM Press, New York, 1995, pp. 233-246.]]

Crossref

Google Scholar

[5]

{5} A. Arnold, M. Nivat, Metric interpretations of infinite trees and semantics of non-deterministic recursive programs, Theoret. Comput. Sci. 11 (1980) 181-205.]]

Crossref

Google Scholar

[6]

{6} G. Berry, G. Boudol, The chemical abstract machine, Theoret. Comput. Sci. 96 (1) (1992) 217-248.]]

Digital Library

Google Scholar

[7]

{7} G. Boudol, A lambda-calculus for parallel functions, Rapports de Recherche No. 1231, INRIA Sophia-Antipolis, May 1990.]]

Google Scholar

[8]

{8} M. Broy, A theory for nondeterminism, parallelism, communication, and concurrency, Theoret. Comput. Sci. 45 (1) (1986) 1-61.]]

Digital Library

Google Scholar

[9]

{9} M. Carlsson, T. Hallgren, Fudgets-purely functional processes with applications to graphical user interfaces, Ph.D. thesis, Department of Computing Sciences, Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden, March 1998.]]

Google Scholar

[10]

{10} W. Clinger, Nondeterministic call by need is neither lazy nor by name, in: Lisp and Functional Programming, 1982, pp. 226-234.]]

Crossref

Google Scholar

[11]

{11} U. de'Liguoro, A. Piperno, Must preorder in non-deterministic untyped γ-calculus, in: CAAP '92, Lecture Notes in Computer Science, vol. 581, 1992, pp. 203-220.]]

Crossref

Google Scholar

[12]

{12} U. de'Liguoro, A. Piperno, Non-deterministic extensions of untyped γ-calculus, Inform. Comput. 122 (2) (1995) 149-177.]]

Digital Library

Google Scholar

[13]

{13} H. Erdogmus, R. Johnston, M. Ferguson, On the operational semantics of nondeterminism and divergence, Theoret. Comput. Sci. 159 (2) (1996) 271-317.]]

Digital Library

Google Scholar

[14]

{14} W. Ferreira, M. Hennessy, Towards a semantic theory of CML (extended abstract), in: J. Wiedermann, P. Hajek (Eds.), Proc. MFCS'95, Lecture Notes in Computer Science, vol. 969, Springer, Berlin, 1995.]]

Crossref

Google Scholar

[15]

{15} W. Ferreira, M. Hennessy, A. Jeffrey, A theory of weak bisimulation for core CML, in: Proc. ICFP'96, ACM Press, New York, 1996, pp. 201-212.]]

Crossref

Google Scholar

[16]

{16} S. Finne, S.P. Jones, Composing Haggis, in: Proc. 5th Eurographics Workshop on Programming Paradigms in Graphics, 1995.]]

Google Scholar

[17]

{17} E.R. Gansner, J.H. Reppy, eXene, in: Proc. 1991 CMU Workshop on Standard ML, Carnegie Mellon University, 1991.]]

Google Scholar

[18]

{18} A.D. Gordon, A.M. Pitts (Eds.), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, Cambridge University Press, Cambridge, 1998.]]

Digital Library

Google Scholar

[19]

{19} M.C.B. Hennessy, The semantics of call-by-value and call-by-name in a nondeterministic environment, SIAM J. Comput. 9 (1) (1980) 67-84.]]

Crossref

Google Scholar

[20]

{20} M.C.B. Hennessy, E.A. Ashcroft, A mathematical semantics for a nondeterministic typed γ-calculus, Theoret. Comput. Sci. 11 (1980)227-245.]]

Crossref

Google Scholar

[21]

{21} M. Hennessy, E.A. Ashcroft, The semantics of non-determinism, in: Automata, Languages and Programming, 1973.]]

Google Scholar

[22]

{22} T. Hildebrandt, P. Panagaden, G. Winskel, A relational model of non-deterministic dataflow, in: CONCUR '98, Lecture Notes in Computer Science, vol. 1466, Springer, Berlin, 1998.]]

Crossref

Google Scholar

[23]

{23} S.P. Jones, A. Gordon, S. Finne, Concurrent Haskell, in: Proc. POPL'96, ACM Press, New York, 1996, pp. 295-308.]]

Crossref

Google Scholar

[24]

{24} S.P. Jones, W. Partain, A. Santos, Let-floating: moving bindings to give faster programs: in: Proc. ICFP'96, ACM Press, New York, 1996, pp. 1-12.]]

Crossref

Google Scholar

[25]

{25} S.P. Jones, A. Santos, A transformation-based optimiser for Haskell, Sci. Comput. Program. 32 (1-3) (1998) 3-47.]]

Digital Library

Google Scholar

[26]

{26} B. Jonsson, J.N. Kok, Comparing two fully abstract dataflow models, in: E. Odijk, M. Rem, J.-C. Syre (Eds.), Proc. Conf. on Parallel Architectures and Languages Europe, Lecture Notes in Computer Science, vols. 2, 366, Springer, Berlin, 1989, pp. 217-234.]]

Crossref

Google Scholar

[27]

{27} A. Kutzner, M. Schmidt-Schauß, A non-deterministic call-by-need lambda calculus, in: Proc. ICFP'98, ACM Press, New York, 1998, pp. 324-335.]]

Crossref

Google Scholar

[28]

{28} S.B. Lassen, Relational reasoning about functions and nondeterminism, Ph.D. Thesis, Department of Computer Science, University of Aarhus, May 1998.]]

Google Scholar

[29]

{29} S.B. Lassen, A.K. Moran, Unique fixed point induction for McCarthy's Arab, in: Proc. MFCS'99, Lecture Notes in Computer Science, vol. 1672, Springer, Berlin, 1999, pp. 198-208.]]

Crossref

Google Scholar

[30]

{30} J. Launchbury, A natural semantics for lazy evaluation, in: Proc. POPL'93, ACM Press, New York, 1993, pp. 144-154.]]

Crossref

Google Scholar

[31]

{31} I. Mason, C. Talcott, Equivalence in functional languages with effects, J. Functional Program. 1 (3) (1991) 287-327.]]

Crossref

Google Scholar

[32]

{32} R. Milner, Fully abstract models of the typed γ-calculus, Theoret. Comput. Sci. 4 (1977) 1-22.]]

Crossref

Google Scholar

[33]

{33} M.W. Mislove, F.J. Oles, A simple language supporting angelic nondeterminism and parallel composition, in: S. Brookes, M. Main, A. Melton, M. Mislove, D. Schmidt (Eds.), Mathematical Foundations of Programming Semantics, 7th Internat. Conf., PA, USA, March 1991, Proc., Lecture Notes in Computer Science, vol. 598, Springer, Berlin, 1992, pp. 77-101.]]

Crossref

Google Scholar

[34]

{34} A.K. Moran, Call-by-name, call-by-need, and McCarthy's Amb, Ph.D. Thesis, Department of Computing Sciences, Chalmers University of Technology, Gothenburg, Sweden, September 1998.]]

Google Scholar

[35]

{35} A.K. Moran, D. Sands, Improvement in a lazy context: an operational theory for call-by-need (extended version), extended version of {36}; available from the authors (Nov. 1998).]]

Crossref

Google Scholar

[36]

{36} A.K. Moran, D. Sands, Improvement in a lazy context: an operational theory for call-by-need, in: Proc. POPL'99, ACM Press, New York, 1999, pp. 43-56.]]

Crossref

Google Scholar

[37]

{37} F. Nielson, H.R. Nielson, From CML to its process algebra, Theoret. Comput. Sci. 155 (1) (1996) 179-219.]]

Digital Library

Google Scholar

[38]

{38} P. Panangaden, V. Shanbhogue, McCarthy's amb cannot implement fair merge, Technical Report, TR88-913, Cornell University, Computer Science Department, May 1988.]]

Crossref

Google Scholar

[39]

{39} P. Panangaden, E.W. Stark, Computations, residuals, and the power of indeterminancy, in: ICALP '88, Lecture Notes in Computer Science, vol. 317, Springer, Berlin, 1988, pp. 439-454.]]

Crossref

Google Scholar

[40]

{40} D. Park, On the semantics of fair parallelism, in: Abstract Software Specifications, Lecture Notes in Computer Science, vol. 86, Springer, Berlin, 1980, pp. 504-526.]]

Crossref

Google Scholar

[41]

{41} D. Park, The fairness problem and nondeterministic computing networks, Mathematisch Centrum, Amsterdam, 1983, pp. 133-162.]]

Google Scholar

[42]

{42} J. Peterson, K. Hammond, The Haskell Report, Version 1.4, Technical Report, Yale University, 1997.]]

Google Scholar

[43]

{43} G.D. Plotkin, A powerdomain construction, SIAM J. Comput. 5 (3) (1976) 452-487.]]

Crossref

Google Scholar

[44]

{44} A.M. Pitts, Some notes on inductive and co-inductive techniques in the semantics of functional programs, Notes Series BRICS-NS-94-5, BRICS, Department of Computer Science, University of Aarhus, December, 1994.]]

Google Scholar

[45]

{45} J.H. Reppy, CML: a higher-order concurrent language, in: Proc. PLDI'91, SIGPLAN Notices, vol. 26, ACM Press, New York, 1991, pp. 294-305.]]

Crossref

Google Scholar

[46]

{46} D. Sands, A naïve time analysis and its theory of cost equivalence, J. Logic Comput 5 (4) (1995) 495-541.]]

Crossref

Google Scholar

[47]

{47} D. Sands, Improvement theory and its applications, in: Gordon, Pitts (Eds.), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, Cambridge University Press, Cambridge, 1998, pp. 275-306.]]

Digital Library

Google Scholar

[48]

{48} D. Sands, Computing with contexts: a simple approach, in: A.D. Gordan, A.M. Pitts, C.L. Talcott (Eds.), Proc. HOOTS II, Electronic Notes in Theoretical Computer Science, vol. 10, Elsevier Science Publishers, Amsterdam, 1998.]]

Google Scholar

[49]

{49} D. Sangiorgi, The lazy lambda calculus in a concurrency scenario, Inform. Comput 111 (1) (1994) 120-153.]]

Digital Library

Google Scholar

[50]

{50} P. Sestoft, Deriving a lazy abstract machine, J. Functional Program. 7 (3) (1997) 231-264.]]

Digital Library

Google Scholar

[51]

{51} H. Søndergaard, P. Sestoft, Non-determinism in functional languages, The Comput. J. 35 (5) (1992) 514-523.]]

Digital Library

Google Scholar

[52]

{52} M.B. Smyth, Power domains, J. Comput. System Sci. 16 (23-26) (1978) 23-35.]]

Crossref

Google Scholar

[53]

{53} M.B. Smyth, Power domains and predicate transformers: a topological view, in: ICALP'83, Lecture Notes in Computer Science, vol. 154, 1983, pp. 662-676.]]

Crossref

Google Scholar

[54]

{54} C.L. Talcott, Reasoning about functions with effects, in: Gordon, Pitts (Eds.), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, Cambridge University Press, Cambridge, 1998, pp. 347-390.]]

Crossref

Google Scholar

[55]

{55} C. Taylor, Formalising and reasoning about Fudgets, Ph.D. Thesis, School of Computer Science and Information Technology, University of Nottingham, October 1998.]]

Google Scholar

[56]

{56} C. Taylor, A theory for core Fudgets, in: Proc. ICFP'98, ACM Press, New York, 1998, pp. 75-85.]]

Crossref

Google Scholar

Cited By

View all

Sabel DSchmidt-Schauß MMaio L(2022)Contextual Equivalence in a Probabilistic Call-by-Need Lambda-CalculusProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551374(1-15)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551374
Ceresa MJaskelioff M(2022)Effectful improvement theoryScience of Computer Programming10.1016/j.scico.2022.102792217:COnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102792
Schmidt-Schauß MSabel DCheney JVidal G(2016)Unification of program expressions with recursive bindingsProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming10.1145/2967973.2968603(160-173)Online publication date: 5-Sep-2016
https://dl.acm.org/doi/10.1145/2967973.2968603
Show More Cited By

Index Terms

Erratic fudgets: a semantic theory for an embedded coordination language

Recommendations

Erratic Fudgets: A Semantic Theory for an Embedded Coordination Language
COORDINATION '99: Proceedings of the Third International Conference on Coordination Languages and Models

The powerful abstraction mechanisms of functional programming languages provide the means to develop domain-specific programming languages within the language itself. Typically, this is realised by designing a set of combinators (higher-order reusable ...
A theory of core fudgets

The Fudgets system is a toolkit for developing graphical applications in the lazy functional programming language Haskell. In this paper we develop an operational semantics for a subset of this system, inspired by ideas from concurrency theory. A ...
A theory of core fudgets
ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

The Fudgets system is a toolkit for developing graphical applications in the lazy functional programming language Haskell. In this paper we develop an operational semantics for a subset of this system, inspired by ideas from concurrency theory. A ...

Reviews

Reviewer: R. Waldo Roth

This insightful paper deals with the topic of erratic fudgets, which is useful in studying parallelism in functional programming languages. Fudgets, and a calculus for them, are also of value in the study of high-level languages that use stream processes, and help provide a calculus for them as well. Readers should have some background in the various ways that interpreters can implement functional calls, such as call-by-need versus the more traditional call-by-name. The concept of lazy functional evaluation is also important, but defined carefully. The underlying languages used to develop this theory are based on Haskell and concurrent Haskell. After an excellent introduction to the topic and to the theory and uses of fudgets, the authors develop a call-by-need lambda calculus, including an erratic choice operator. The notation and development is strenuous, and may be difficult for those not initiated in the subject, but can be read, if carefully, since the style of the paper is supportive and pedagogical. The theorems developed are cryptic and concisely developed, but adequate for the authors' purposes. A short, helpful fudget example is illustrated in an appendix, but may have been more useful to the reader earlier in the paper. The authors have a clear and instructional writing style, and have included a thorough and rather complete list of 50 citations and references on the topics developed. The material should be useful for those doing research in this specialty, particularly those who have placed heavy emphasis on the developments of Chris Taylor. The authors' suggestions and ideas on applying their work to parallel computing are the highlights of the paper, and should be especially contributory to further research. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Science of Computer Programming

Science of Computer Programming Volume 46, Issue 1-2

Special issue on coordination languages and architectures

January/February 2003

190 pages

ISSN:0167-6423

Issue’s Table of Contents

Publisher

Elsevier North-Holland, Inc.

United States

Publication History

Published: 01 January 2003

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sabel DSchmidt-Schauß MMaio L(2022)Contextual Equivalence in a Probabilistic Call-by-Need Lambda-CalculusProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551374(1-15)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551374
Ceresa MJaskelioff M(2022)Effectful improvement theoryScience of Computer Programming10.1016/j.scico.2022.102792217:COnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102792
Schmidt-Schauß MSabel DCheney JVidal G(2016)Unification of program expressions with recursive bindingsProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming10.1145/2967973.2968603(160-173)Online publication date: 5-Sep-2016
https://dl.acm.org/doi/10.1145/2967973.2968603
Schmidt-Schauí MSabel DMachkasova E(2011)Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrecInformation Processing Letters10.1016/j.ipl.2011.04.011111:14(711-716)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1016/j.ipl.2011.04.011
Schmidt-Schauß M(2007)Correctness of copy in calculi with letrecProceedings of the 18th international conference on Term rewriting and applications10.5555/1779782.1779807(329-343)Online publication date: 26-Jun-2007
https://dl.acm.org/doi/10.5555/1779782.1779807

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations