Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

Effect Systems Revisited—Control-Flow Algebra and Semantics

verfasst von : Alan Mycroft, Dominic Orchard, Tomas Petricek

Erschienen in: Semantics, Logics, and Calculi

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Effect systems were originally conceived as an inference-based program analysis to capture program behaviour—as a set of (representations of) effects. Two orthogonal developments have since happened. First, motivated by static analysis, effects were generalised to values in an algebra, to better model control flow (e.g. for may/must analyses and concurrency). Second, motivated by semantic questions, the syntactic notion of set- (or semilattice-) based effect system was linked to the semantic notion of monads and more recently to graded monads which give a more precise semantic account of effects.
We give a lightweight tutorial explanation of the concepts involved in these two threads and then unify them via the notion of an effect-directed semantics for a control-flow algebra of effects. For the case of effectful programming with sequencing, alternation and parallelism—illustrated with music—we identify a form of graded joinads as the appropriate structure for unifying effect analysis and semantics.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Nächstes Kapitel Last Mile’s Resources
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
To slightly shorten the example, the melody of the last phrase repeats that of the first. Musicians are invited to use the correct notes: F2;F2;E2;C2;D2;C2.
 
2
This easily maps to the \(\lambda \)-calculus-with-constants formulation used in later sections by replacing the https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-27810-0_1/395252_1_En_1_IEq2_HTML.gif statement with https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-27810-0_1/395252_1_En_1_IEq3_HTML.gif and a tail-recursive call, and by treating \(e;e'\) as shorthand for https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-27810-0_1/395252_1_En_1_IEq5_HTML.gif for some fresh variable x.
 
3
Mathematically, \(\mathsf {T}\) is an endofunctor, but languages such as Haskell (and the Monad language in this section) expose monads syntactically as parametric type constructors M; thus side-effecting functions have analogous types \(\tau \rightarrow M \tau '\). We try not to labour either this distinction or that between types (often written A, B instead of \(\tau ,\tau '\) above) and the categorical objects A, B which model them (more formally \({\llbracket {\tau }\rrbracket },{\llbracket {\tau '}\rrbracket }\)).
 
4
We use \([-]\) for translation into another language and reserve \(\llbracket - \rrbracket \) for semantic interpretation (denotation) as in the next section.
 
5
Katsumata uses ‘pre-ordered’ but we simply consider \((\sqsubseteq )\cap (\sqsubseteq ^{-1})\) equivalence classes.
 
6
Section 3 addresses the subtlety here that https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-27810-0_1/395252_1_En_1_IEq279_HTML.gif is reflected with operation \(+\) in the music effect while Katsumata’s graded monads use a relation \(\sqsubseteq \).
 
7
Categorically, a natural transformation, derived from coproducts with \(\mathbb {B} = 1 + 1\).
 
8
Laxity means that the homomorphic map \(\mathsf {T}: \mathcal {F} \rightarrow [\mathcal {C},\mathcal {C}]\) from effects to type-constructors (endofunctors) on \(\mathcal {C}\) has functions witnessing the mapping between structure on \(\mathcal {F}\) and on \([\mathcal {C},\mathcal {C}]\), e.g., \( \mathsf {merge}^{F,G}_{A,B} : \mathsf {T}_F A \times \mathsf {T}_G B \rightarrow \mathsf {T}_{F \& G} (A \times B)\), rather than equalities, e.g., \( \mathsf {T}_F A \times \mathsf {T}_G B = \mathsf {T}_{F \& G} (A \times B)\).
 
Literatur
1.
Aaron, S., Orchard, D., Blackwell, A.F.: Temporal semantics for a live coding language. In: Proceeding 2nd ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design, pp. 37–47. ACM (2014)
2.
Amtoft, T., Nielson, F., Nielson, H.: Type and Effect Systems Behaviours for Concurrency. Imperial College Press (1999)
3.
Atkey, R.: Parameterised notions of computation. Cambridge University Press. In: Proceedings of MSFP (2006)
4.
Benton, N., Kennedy, A., Hofmann, M.O., Beringer, L.: Reading, writing and relations. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 114–130. Springer, Heidelberg (2006)CrossRef
5.
Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 351–370. Springer, Heidelberg (2014)CrossRef
6.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238–252. ACM (1977)
7.
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of PLDI 2003. ACM (2003)
8.
Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 331–350. Springer, Heidelberg (2014)CrossRef
9.
Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: Proceedings of Conference on LISP and Functional Programming, LFP 1986 (1986)
10.
Goncharov, S., Schröder, L., Mossakowski, T.: Kleene monads: handling iteration in a framework of generic effects. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 18–33. Springer, Heidelberg (2009)CrossRef
11.
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)CrossRef
12.
Jouvelot, P., Gifford, D.K.: Communication Effects for Message-Based Concurrency. Technical report, Massachusetts Institute of Technology (1989)
13.
Jouvelot, P., Gifford, D.K.: Reasoning about continuations with control effects. In: Proceedings of PLDI 1989. ACM (1989)
14.
Kammar, O.: Algebraic theory of type-and-effect systems, Ph.D. dissertation. The University of Edinburgh (2014)
15.
Kammar, O., Plotkin, G.D.: Algebraic foundations for effect-dependent optimisations. In: Proceedings of POPL 2012, pp. 349–360. ACM (2012)
16.
Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Proceedings of POPL 2014, pp. 633–645. ACM (2014)
17.
Kiselyov, O., Shan, C.C., Friedman, D.P., Sabry, A.: Backtracking, interleaving, and terminating monad transformers (functional pearl). In: Proceedings of ICFP 2005, pp. 192–203. ACM (2005)
18.
Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 47–57. ACM (1988)
19.
Madhavapeddy, A., Mortier, R., Rotsos, C., Scott, D., Singh, B., Gazagnaire, T., Smith, S., Hand, S., Crowcroft, J.: Unikernels: library operating systems for the cloud. SIGPLAN Not. 48(4), 461–472 (2013)CrossRef
20.
21.
Milius, S., Pattinson, D., Schröder, L.: Generic trace semantics and graded monads. In: Proceedings of 6th International Conference in Algebra and Coalgebra in Computer Science (2015)
22.
Milner, R.: Communication and Concurrency, vol. 84. Prentice Hall, New York (1989)MATH
23.
Moggi, E.: Computational lambda-calculus and monads. In: Fourth Annual Symposium on Logic in Computer Science, pp. 14–23. IEEE (1989)
24.
25.
Nielson, F., Cousot, P., Dam, M., Degan, P., Jouvelot, P., Mycroft, A., Thomsen, B.: Logical and operational methods in the analysis of programs and systems. In: Dam, M. (ed.) LOMAPS-WS 1996. LNCS, vol. 1192, pp. 1–12. Springer, Heidelberg (1997)CrossRef
26.
Nielson, F., Riis Nielson, H.: Type and Effect Systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 114–136. Springer, Heidelberg (1999)CrossRef
27.
Orchard, D., Petricek, T.: Embedding effect systems in Haskell. In: Proceedings of ACM SIGPLAN symposium on Haskell, pp. 13–24. ACM (2014)
28.
Orchard, D.A., Petricek, T., Mycroft, A.: The semantic marriage of monads and effects. CoRR, abs/1401.5391 (2014)
29.
Petricek, T., Mycroft, A., Syme, D.: Extending monads with pattern matching. In: Proceedings of Haskell Symposium, Haskell (2011)
30.
Petricek, T., Orchard, D., Mycroft, A.: Coeffects: unified static analysis of context-dependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 385–397. Springer, Heidelberg (2013)CrossRef
31.
Petricek, T., Orchard, D., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp. 123–135. ACM (2014)
32.
Petricek, T., Syme, D.: Joinads: a retargetable control-flow construct for reactive, parallel and concurrent programming. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 205–219. Springer, Heidelberg (2011)CrossRef
33.
Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)CrossRef
34.
Plotkin, G., Pretnar, M.: A logic for algebraic effects. In: Logic in Computer Science, LICS 2008, pp. 118–129. IEEE (2008)
35.
Rivas, E., Jaskelioff, M., Schrijvers, T.: From monoids to near-semirings: the essence of monadplus and alternative. In: Proceeding of International Symposium on Principles and Practice of Declarative Programming, pp. 196–207. ACM (2015)
36.
37.
Talpin, J.P., Jouvelot, P.: The type and effect discipline. In: Logic in Computer Science, LICS 1992, pp. 162–173. IEEE (1992)
38.
Vouillon, J.: Lwt: a cooperative thread library. In: Proceedings of ACM SIGPLAN Workshop on ML, pp. 3–12. ACM, New York (2008)
39.
Metadaten
Titel
Effect Systems Revisited—Control-Flow Algebra and Semantics
verfasst von
Alan Mycroft
Dominic Orchard
Tomas Petricek
Copyright-Jahr
2016
Buch
Semantics, Logics, and Calculi

Print ISBN: 978-3-319-27809-4

Electronic ISBN: 978-3-319-27810-0

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-27810-0_1