pith. sign in

arxiv: 1907.02990 · v1 · pith:R5PLHO5Anew · submitted 2019-07-05 · 💻 cs.PL · cs.DB

Type-safe, Polyvariadic Event Correlation

Oliver Bra\v{c}evac , Guido Salvaneschi , Sebastian Erdweg , Mira Mezini This is my paper

Pith reviewed 2026-05-25 01:29 UTC · model grok-4.3

classification 💻 cs.PL cs.DB
keywords event correlationtype-safe embeddingpolyvariadic patternstagless final encodinghigher-order abstract syntaxjoin querieslibrary embedding
0
0 comments X

The pith

Event patterns with any number of variables can be embedded as a pure library using join notation while the host type system rejects all ill-typed cases.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that a tagless final encoding combined with uncurried higher-order abstract syntax can represent fully polyvariadic event patterns for arbitrary numbers of variables. This encoding works inside an ordinary programming language without any code generation step and supports polymorphic correlation semantics that are not limited to monads. A sympathetic reader cares because the same join-query notation already familiar from databases becomes usable for complex event processing while type errors are caught at compile time by construction. The approach therefore removes the need to switch to a specialized event language or to generate code in order to obtain static guarantees.

Core claim

PolyJoin shows that a tagless final encoding with uncurried HOAS representation of event patterns with n variables, for arbitrary n, can be defined entirely inside the host language. The encoding exploits the host type system to model the pattern language, so that ill-typed patterns are impossible to write. The resulting library accepts the familiar join-query notation yet is not restricted to monadic semantics, and an implementation in multicore OCaml demonstrates that the embedding is practical, type-safe and extensible.

What carries the argument

tagless final encoding with uncurried higher-order abstract syntax (HOAS) for representing event patterns with n variables for arbitrary n

If this is right

  • Event patterns become expressible in ordinary join notation inside a general-purpose language.
  • No code generation is required to obtain the type safety guarantees.
  • Correlation semantics can be polymorphic and are not forced into a monadic form.
  • The same library mechanism can be extended with new correlation operators while preserving type safety.
  • An implementation in multicore OCaml already demonstrates usability for realistic event workloads.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same encoding technique might be applied to other polyvariadic query notations that currently rely on code generation.
  • If the approach scales to larger n, it removes a practical barrier that has kept event correlation libraries from offering full static checking.
  • Programmers could begin to treat complex event patterns as ordinary, type-checked library calls rather than as a separate language feature.

Load-bearing premise

A tagless final encoding with uncurried HOAS can represent and type-check fully polyvariadic patterns with polymorphic correlation semantics for arbitrary n while remaining a pure library without code generation.

What would settle it

A concrete implementation attempt in which a pattern containing a type mismatch between events and the correlation function still type-checks under the library would show the central claim is false.

Figures

Figures reproduced from arXiv: 1907.02990 by Guido Salvaneschi, Mira Mezini, Oliver Bra\v{c}evac, Sebastian Erdweg.

Figure 1
Figure 1. Figure 1: Event Correlation Example: Fire Alarm. smoke events are relevant, i.e., those that occur at points in time at most 5 minutes apart, the smoke event’s value is true and the temperature event’s value is above 50◦ Celsius. The yield clause generates a new event from each relevant pair, in this example a string-valued event con￾taining a warning message along with the temperature value. Overall, the join query… view at source ↗
Figure 2
Figure 2. Figure 2: Basic Tagless Final Examples. Line 2 defines the pattern’s variables and body in terms of an OCaml function literal and OCaml variables, in higher-order abstract syntax (HOAS) [Huet and Lang 1978; Pfenning and Elliott 1988]. This way, we avoid the delicate and error-prone task of modeling variable binding, free variables and substitution for the DSL by ourselves, instead delegating it to the host language … view at source ↗
Figure 3
Figure 3. Figure 3: Core Syntax and Typing Rules of PolyJoin. 1 module type Symantics = sig 2 type 'a shape (* Shape[·] Constructor *) 3 (* Judgments (cf [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Tagless Final Representation of Core [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Heterogeneous Lists Definition. 1 module StdContext(T: sig type 'a repr type 'a shape end) = struct 2 open T 3 type _ var = Bind: 'a shape repr -> 'a var 4 module Ctx = HList(struct type 'a t = 'a var end) 5 type (_,_) shape = (* Shape translation judgment *) 6 | Base: (unit, unit) shape 7 | Step: ('s, 'a) jsig -> ('t * 's, 't repr * 'a) shape 8 (* Implementation of Context Formation (Figures 3 and 4) *) 9… view at source ↗
Figure 6
Figure 6. Figure 6: Default Variable Context Representation with Hetero [PITH_FULL_IMAGE:figures/full_fig_p011_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Sequential Cartesian Product in [PITH_FULL_IMAGE:figures/full_fig_p011_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Join Computations in Cartesius. 3.4.5 Example: Sequential Cartesian Product. We conclude this section with an example PolyJoin interpreter, implementing an old friend: the nested monadic translation from LINQ/comprehen￾sions (Section 2) over lists, yielding a cartesian product [PITH_FULL_IMAGE:figures/full_fig_p015_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: PolyJoin with Meta Data and Contextual Extensions. 1 join ((from temp_sensor) @. (from smoke_sensor) @. cnil) 2 ((most_recently p0) |++| (most_recently p1)) 3 (fun ((temp,t1), ((smoke,t2), ())) -> 4 yield (pair temp smoke)) [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗
Figure 11
Figure 11. Figure 11: Generative Effects from Modules in Multicore OCaml. [PITH_FULL_IMAGE:figures/full_fig_p019_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Example Polyvariadic State Handler. 1 let where: bool repr -> ('c,'a) pat -> ('c,'a) pat = 2 fun cond body meta yf -> 3 if cond then (body meta yf) else fail_with yf 1 let yield: 'a repr -> ('c,'a) pat = 2 fun result meta yf -> (result, (merge_all meta)) [PITH_FULL_IMAGE:figures/full_fig_p020_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Cartesius Pa ern Implementation in Context/Capability-Passing Style. 1 let join: type s a b. (s, a) ctx -> s ext -> (a -> (s, b) pat) -> b shape repr 2 = fun ctx extension pattern_body -> 3 (* (effect Pushi: si -> unit)1≤i ≤n: *) 4 let slots: s Slots.hlist = gen_slots_from ctx in 5 (* effect Yield: b -> unit and effect Fail: unit -> 'c: *) 6 let yf: b yieldfail = gen_yieldfail () in 7 (* instantiate and r… view at source ↗
Figure 14
Figure 14. Figure 14: Implementation of Cartesius Join Pa erns. A tagless interpreter requires a policy for computing the metadata of joined events from the meta data of input events. However, we do not expose merging explicitly in the pattern syntax. E.g., the pattern body in [PITH_FULL_IMAGE:figures/full_fig_p020_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: The Focusing Continuations Problem. is the only way to obtain b-typed events, which may be communicated over the output event source b shape repr. However, the types are too weak to enforce that the implementation is always pro￾ductive, i.e., it might be inert or diverging. More sophisticated type systems are necessary to en￾force productivity, e.g., where types represent theorems in linear temporal logic… view at source ↗
Figure 16
Figure 16. Figure 16: Multicore OCaml Solution to the Focusing Continuat [PITH_FULL_IMAGE:figures/full_fig_p025_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Illustration of Dynamic Execution Context during Foc [PITH_FULL_IMAGE:figures/full_fig_p025_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: GADTs for Type-safe Pointers and Sets of Pointers. [PITH_FULL_IMAGE:figures/full_fig_p025_18.png] view at source ↗
Figure 20
Figure 20. Figure 20: Type-safe Element Access [PITH_FULL_IMAGE:figures/full_fig_p026_20.png] view at source ↗
Figure 21
Figure 21. Figure 21: Example: Position-polymorphic Restriction Handle [PITH_FULL_IMAGE:figures/full_fig_p026_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Tagless Final Representation of Extended [PITH_FULL_IMAGE:figures/full_fig_p037_22.png] view at source ↗
read the original abstract

The pivotal role that event correlation technology plays in todays applications has lead to the emergence of different families of event correlation approaches with a multitude of specialized correlation semantics, including computation models that support the composition and extension of different semantics. However, type-safe embeddings of extensible and composable event patterns into statically-typed general-purpose programming languages have not been systematically explored so far. Event correlation technology has often adopted well-known and intuitive notations from database queries, for which approaches to type-safe embedding do exist. However, we argue in the paper that these approaches, which are essentially descendants of the work on monadic comprehensions, are not well-suited for event correlations and, thus, cannot without further ado be reused/re-purposed for embedding event patterns. To close this gap we propose PolyJoin, a novel approach to type-safe embedding for fully polyvariadic event patterns with polymorphic correlation semantics. Our approach is based on a tagless final encoding with uncurried higher-order abstract syntax (HOAS) representation of event patterns with n variables, for arbitrary $n \in \mathbb{N}$. Thus, our embedding is defined in terms of the host language without code generation and exploits the host language type system to model and type check the type system of the pattern language. Hence, by construction it impossible to define ill-typed patterns. We show that it is possible to have a purely library-level embedding of event patterns, in the familiar join query notation, which is not restricted to monads. PolyJoin is practical, type-safe and extensible. An implementation of it in pure multicore OCaml is readily usable.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper claims that PolyJoin, a tagless-final encoding based on uncurried higher-order abstract syntax (HOAS), provides a purely library-level embedding of fully polyvariadic event patterns (arbitrary n) in familiar join-query notation inside a statically typed host language (OCaml). The encoding is said to enforce the pattern language's typing rules by construction, support polymorphic correlation semantics, remain free of monadic restrictions and code generation, and be practical and extensible.

Significance. If the central claim holds, the result would be significant: it supplies a non-monadic, library-only route to type-safe event correlation that directly exploits the host type system for safety and extensibility. The explicit availability of a pure multicore OCaml implementation is a concrete strength that supports reproducibility and usability claims.

major comments (1)
  1. [Abstract] Abstract (paragraph on PolyJoin approach): the claim that the uncurried-HOAS tagless-final encoding supports fully polyvariadic patterns 'for arbitrary n ∈ ℕ' and enforces type safety 'by construction' is load-bearing, yet the abstract supplies neither an inductive definition nor a proof sketch showing how the host-language types scale without bound or additional code generation; this gap prevents verification of the central type-safety guarantee.
minor comments (1)
  1. The abstract states that the approach is 'not restricted to monads' but does not contrast the encoding with monadic-comprehension descendants at the level of typing rules or example patterns; a short comparative table would clarify the claimed advantage.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed review and constructive feedback. We address the single major comment below, agreeing where the abstract is indeed concise and proposing a targeted revision.

read point-by-point responses

  1. Referee: [Abstract] Abstract (paragraph on PolyJoin approach): the claim that the uncurried-HOAS tagless-final encoding supports fully polyvariadic patterns 'for arbitrary n ∈ ℕ' and enforces type safety 'by construction' is load-bearing, yet the abstract supplies neither an inductive definition nor a proof sketch showing how the host-language types scale without bound or additional code generation; this gap prevents verification of the central type-safety guarantee.

    Authors: We acknowledge that the abstract, as a high-level summary, does not contain an inductive definition or proof sketch; these details appear in the body of the manuscript, where the tagless-final encoding is defined and the host-language type system is shown to enforce the pattern rules for any n. The uncurried HOAS representation is constructed so that the host type checker directly validates arity and typing without code generation or monadic wrappers. To make the central claim more self-contained in the abstract, we will add one sentence briefly indicating the scaling mechanism via the encoding. This revision addresses the concern without altering the manuscript's technical content. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central claim is a library-level tagless-final encoding with uncurried HOAS that embeds polyvariadic patterns and enforces their typing rules via the host language type system by construction. No load-bearing step reduces to a fitted parameter renamed as prediction, a self-citation chain, an ansatz smuggled via prior work, or a renaming of a known result. The derivation is self-contained: the type safety follows directly from the encoding's use of host-language types, with no equations or premises that equate to their own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on domain assumptions about the expressiveness of tagless final encodings and HOAS rather than new physical entities or fitted parameters; no free parameters are introduced.

axioms (2)
  • domain assumption The host language type system can model and enforce the type system of the event pattern language for arbitrary n
    Invoked to support the claim that ill-typed patterns are impossible by construction.
  • domain assumption Uncurried HOAS with tagless final encoding suffices for polymorphic correlation semantics without code generation
    Required for the polyvariadic and extensible aspects of the embedding.
invented entities (1)
  • PolyJoin encoding no independent evidence
    purpose: Library-level representation of polyvariadic event patterns
    New construct introduced to achieve type-safe embedding; no independent evidence provided outside the paper.

pith-pipeline@v0.9.0 · 5824 in / 1457 out tokens · 35187 ms · 2026-05-25T01:29:28.020077+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    The VLDB Journal (2006)

    The CQL continuous query language: Semantic foundations and query execution. The VLDB Journal (2006). 34 Bračevac, Salvaneschi, Erdweg, and Mezini Kenichi Asai

    work page 2006

  2. [2]

    Higher-Order and Symbolic Computation 22, 3 (2009), 275–291

    On typing delimited continuations: Three new solutions t o the printf problem. Higher-Order and Symbolic Computation 22, 3 (2009), 275–291. Engineer Bainomugisha, Andoni Lombide Carreton, Tom Van Cutsem, Stijn M ostinckx, and Wolfgang De Meuter

    work page 2009

  3. [3]

    ACM Computing Surveys 45, 4 (2013)

    A survey on reactive programming. ACM Computing Surveys 45, 4 (2013). Aggelos Biboudis, Nick Palladinos, George Fourtounis, and Yannis Sma ra gda kis

    work page 2013

  4. [4]

    Proceedings of the ACM on Programming Languages (PACMPL) 2, International Conference on Functional Programming (ICFP) (9 2018)

    Versatile event correlation with algebraic effects. Proceedings of the ACM on Programming Languages (PACMPL) 2, International Conference on Functional Programming (ICFP) (9 2018). Paris Carbone, Asterios Katsifodimos, Stephan Ewen, Volker Markl, Seif Haridi, and Kostas Tzoumas

    work page 2018

  5. [5]

    IEEE Data Eng

    Apache flink ™ : Stream and batch processing in a single engine. IEEE Data Eng. Bull. 38, 4 (2015), 28–38. Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan

    work page 2015

  6. [6]

    Journal of Functional Programming 19, 5 (2009), 509–543

    Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming 19, 5 (2009), 509–543. Andrew Cave, Francisco Ferreira, Prakash Panangaden, and Brigitte Pient ka

    work page 2009

  7. [7]

    Proceedings of the VLDB Endowment 8, 4 (2014), 401–412

    Trill: A high-performance incremental query process or for diverse analytics. Proceedings of the VLDB Endowment 8, 4 (2014), 401–412. James Cheney and Ralf Hinze

    work page 2014

  8. [8]

    ACM Computing Surveys 44, 3 (2012), 15:1–15:62

    Processing flows of information: From data stream to complex event processing. ACM Computing Surveys 44, 3 (2012), 15:1–15:62. Olivier Danvy

    work page 2012

  9. [9]

    Journal of Functional Programming 8, 6 (1998), 621–625

    Functional unparsing. Journal of Functional Programming 8, 6 (1998), 621–625. Nicolaas Govert De Bruijn

    work page 1998

  10. [10]

    Transactions on Programming Languages and Systems (TOPLAS) (2009)

    Revisiting corou tines. Transactions on Programming Languages and Systems (TOPLAS) (2009). Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Madhava ped dy, KC Sivaramakrishnan, and Leo White

    work page 2009

  11. [11]

    Retrieved June 11, 2018 from http://web.archive.org/web/20180611025539/https://github.com/scala/scala-async EsperTech Inc

    Scala Async. Retrieved June 11, 2018 from http://web.archive.org/web/20180611025539/https://github.com/scala/scala-async EsperTech Inc. 2006.Esper. Retrieved April 22, 2018 from https://web.archive.org/web/20180422212134/http://www.espertech.com/esper/ Patrick Eugster and K.R. Jayaram

    work page arXiv 2018

  12. [12]

    Christian Hofer, Klaus Ostermann, Tillmann Rendel, and Adriaan Moors

    Do we need dependent types? Journal of Functional Programming (2000). Christian Hofer, Klaus Ostermann, Tillmann Rendel, and Adriaan Moors

    work page 2000

  13. [13]

    ACM Computing Surveys 28, 4es (1996),

    Building domain-specific embedded languages. ACM Computing Surveys 28, 4es (1996),

    work page 1996

  14. [14]

    Journal of Functional Programming (1997)

    The zipper. Journal of Functional Programming (1997). Gérard Huet and Bernard Lang

    work page 1997

  15. [15]

    Acta Informatica (1978)

    Proving and applying program transformations expressed with second-order patterns. Acta Informatica (1978). John Hughes

    work page 1978

  16. [16]

    Science of Computer Programming 37, 1-3 (2000)

    Generalising monads to arrows. Science of Computer Programming 37, 1-3 (2000). Patricia Johann and Neil Ghani

    work page 2000

  17. [17]

    Retrieved October 10, 2018 from https://web.archive.org/web/20181013042601/http://okmij.org/ftp/Haskell/polyvariadic.html Oleg Kiselyov, Ralf Lämmel, and Keean Schupke

    Polyvariadic functions and keyword arguments: Pattern-ma tching on the type of the context . Retrieved October 10, 2018 from https://web.archive.org/web/20181013042601/http://okmij.org/ftp/Haskell/polyvariadic.html Oleg Kiselyov, Ralf Lämmel, and Keean Schupke

    work page arXiv 2018

  18. [18]

    Journal of Functional Programming 12, 4&5 (2002), 375–392

    Faking it: Simulating dependent types in haskell. Journal of Functional Programming 12, 4&5 (2002), 375–392. Conor McBride and Ross Paterson

    work page 2002

  19. [19]

    Journal of Functional Programming (2008)

    Applicative programming with effects. Journal of Functional Programming (2008). Erik Meijer, Brian Beckman, and Gavin Bierman

    work page 2008

  20. [20]

    Information and computation 93, 1 (1991), 55–92

    Notions of computation and monads. Information and computation 93, 1 (1991), 55–92. Luc Moreau

    work page 1991

  21. [21]

    Higher-Order and Symbolic Computation 11, 3 (1998)

    A syntactic theory of dynamic binding. Higher-Order and Symbolic Computation 11, 3 (1998). Alan Mycroft, Dominic A. Orchard, and Tomas Petricek

    work page 1998

  22. [22]

    Proceedings of the ACM on Programming Languages (PACMPL) 2, Symposium on Principles of Programming Languages (POPL) (2018)

    Simplicitly: Foundations and applications of implicit function types. Proceedings of the ACM on Programming Languages (PACMPL) 2, Symposium on Principles of Programming Languages (POPL) (2018). Bruno C.d.S. Oliveira and William R. Cook

    work page 2018

  23. [23]

    In Proceedings of European Conference on Object-Oriented Pro gramming (ECOOP)

    Feature-oriented programming with object algebras. In Proceedings of European Conference on Object-Oriented Pro gramming (ECOOP). Jennifer Paykin, Neelakantan R. Krishnaswami, and Steve Zdancewic. 2016 . The essence of event-driven programming. (2016). Unpublished Draft (https://web.archive.org/web/20161018163751/http://www.mpi-sws.org/~neelk/essence-of-e...

    work page arXiv 2016

  24. [24]

    Applied Categorical Structures (2003)

    Algebraic operations and ge neric effects. Applied Categorical Structures (2003). Gordon D. Plotkin and Matija Pretnar

    work page 2003

  25. [25]

    Retrieved May 3, 2019 from https://web.archive.org/web/20190503085703/http://reactivex.io/ John C

    Reactive Extensions. Retrieved May 3, 2019 from https://web.archive.org/web/20190503085703/http://reactivex.io/ John C. Reynolds

    work page arXiv 2019

  26. [26]

    Programming Methodology: A Collection of Articles by Membe rs of IFIP WG2.3 (1978), 309–317

    User-defined types and procedural data s tructures as complementary approaches to data abstrac- tion. Programming Methodology: A Collection of Articles by Membe rs of IFIP WG2.3 (1978), 309–317. Morten Rhiger

    work page 1978

  27. [27]

    Journal of Functional Programming (2009)

    Type-safe pattern combinators. Journal of Functional Programming (2009). Tiark Rompf and Martin Odersky

    work page 2009

  28. [28]

    In Proceedings of Symposium on Principles of Programming Languages (POPL)

    How to make ad-hoc polymo rphism less ad-hoc. In Proceedings of Symposium on Principles of Programming Languages (POPL) . Stephanie Weirich and Chris Casinghino. 2010a. Arity-generic datatype-g eneric programming. In Proceedings of the Work- shop on Programming Languages Meets Program Verification (P LPV). Stephanie Weirich and Chris Casinghino. 2010b. Gen...

    work page 2010

  29. [29]

    Lisp and Symbolic Computation 8, 4 (1995)

    Simple imperative polymorphism. Lisp and Symbolic Computation 8, 4 (1995). Jeremy Yallop and Leo White

    work page 1995