arXiv subjects

Oleg Kiselyov

Publications and source records attributed to Oleg Kiselyov.

At least 19 recordsLinked to original sources

arXiv2026

Complete Fusion for Stateful Streams: Equational Theory of Stateful Streams and Fusion as Normalization-by-Evaluation

Processing large amounts of data fast, in constant and small space is the point of stream processing and the reason for its increasing use. Alas, the most performant, imperative processing code tends to be almost impossible to read, let alone modify, reuse -- or write correctly. We present both a stream compilation theory and its implementation as a portable stream processing library Strymonas that lets us assemble complex stream pipelines just by plugging in simple combinators, and yet attain the performance of hand-written imperative loops and state machines. The library supports finite and infinite streams and offers a rich set of combinators. They may be freely composed, and yet the resulting convoluted imperative code has no traces of combinator abstractions: no closures or intermediate objects. The high-performance is portable and statically guaranteed, without relying on compiler or black-box optimizations. We greatly exceed in performance the available stream processing libraries in OCaml. The library generates C and OCaml code. The declaratively built Strymonas pipelines are all stateful. The stream state introduced in the library is not directly observable. Therefore, the Strymonas API looks like the familiar interface of `pure functional' combinators. Programmers may introduce their own stream state and share it across the pipeline. Strymonas has been developed in tandem with the equational theory of stateful streams. Our theoretical model represents all desired pipelines and guarantees the existence of unique normal forms, which are mappable to (fused) state machines. We describe the normalization algorithm, as a form of normalization-by-evaluation. The equational theory lets us state and prove the correctness of the complete fusion optimization.

cs.PL↗

arXiv2026

Handling Scope Checks (Extended Version)

Metaprogramming and effect handlers interact in unexpected, and sometimes undesirable, ways. One example is scope extrusion: the generation of ill-scoped code. Scope extrusion can either be preemptively prevented, via static type systems, or retroactively detected, via dynamic checks. Static type systems exist in theory, but struggle with a range of implementation and usability problems in practice. In contrast, dynamic checks exist in practice (e.g. in MetaOCaml), but are understudied in theory. Designers of metalanguages are thus given little guidance regarding the design and implementation of checks. We present the first formal study of dynamic scope extrusion checks, introducing a calculus ($λ_{\langle\langle\text{op}\rangle\rangle}$) for describing and evaluating checks. Further, we introduce a novel dynamic check $\unicode{x2014}$ the "Cause-for-Concern" check $\unicode{x2014}$ which we prove correct, characterise without reference to its implementation, and argue combines the advantages of existing dynamic checks. Finally, we extend our framework with refined environment classifiers, which statically prevent scope extrusion, and compare their expressivity with the dynamic checks.

cs.PL↗

arXiv2023

Free Variable as Effect, in Practice

Variable environment is the time-honored way of making sense of free variables, used in programming language theory as well when writing interpreters and some compilers. Algebraic effects give another way, as was pointed already at HOPE 2017. Although a theoretical curiosity, it may have surprising practical benefits: a new way of writing compilers, with the incremental type-checking, with easy variable usage, leaf function analyses. This work-in-progress report prototypes and illustrates the idea.

cs.PL↗

arXiv2023

MetaOCaml Theory and Implementation

Quasi-quotation (or, code templates) has long been used as a convenient tool for code generation, commonly implemented as a pre-processing/translation into code-generation combinators. The original MetaOCaml was also based on such translation, done post type checking. BER MetaOCaml employs a significantly different, efficient (especially in version N114) translation integrated with type-checking, in the least intrusive way. This paper presents the integrated efficient translation for the first time.

cs.PL↗

arXiv2022

Demo: New View on Plasma Fractals -- From the High Point of Array Languages

Plasma fractals is a technique to generate random and realistic clouds, textures and terrains~-- traditionally using recursive subdivision. We demonstrate a new approach, based on iterative expansion. It gives a family of algorithms that includes the standard square-diamond algorithm and offers various interesting ways of extending it, and hence generating nicer pictures. The approach came about from exploring plasma fractals from the point of view of an array language (which we implemented as an embedded DSL in OCaml)~-- that is, from the perspective of declaring whole image transformations rather than fiddling with individual pixels.

cs.GR↗

arXiv2022

Highest-performance Stream Processing

We present the stream processing library that achieves the highest performance of existing OCaml streaming libraries, attaining the speed and memory efficiency of hand-written state machines. It supports finite and infinite streams with the familiar declarative interface, of any combination of map, filter, take(while), drop(while), zip, flatmap combinators and tupling. Experienced users may use the lower-level interface of stateful streams and implement accumulating maps, compression and windowing. The library is based on assured code generation (at present, of OCaml and C) and guarantees in all cases complete fusion.

cs.PL↗

arXiv2022

Do Mutable Variables Have Reference Types?

Implicit heterogeneous metaprogramming (a.k.a. offshoring) is an attractive approach for generating C with some correctness guarantees: generate OCaml code, where the correctness guarantees are easier to establish, and then map that code to C. The key idea is that simple imperative OCaml code looks like a non-standard notation for C. Regretfully, it is false, when it comes to mutable variables. In the past, the approach was salvaged by imposing strong ad hoc restrictions. The present paper for the first time investigates the problem systematically and discovers general solutions needing no restrictions. In the process we explicate the subtleties of modeling mutable variables by values of reference types and arrive at an intuitively and formally clear correspondence. We also explain C assignment without resorting to L-values.

cs.PL↗

arXiv2022

Complete Stream Fusion for Software-Defined Radio

Software-Defined Radio (SDR) is widely used not only as a practical application but also as a fitting benchmark of high-performance signal processing. We report using the SDR benchmark -- specifically, FM Radio reception -- to evaluate the recently developed single-thread stream processing library strymonas, contrasting it with the synchronous dataflow system StreamIt. Despite the absence of parallel processing or windowing as a core primitive, strymonas turns out to easily support SDR, offering high expressiveness and performance, approaching the peak single-core floating-point performance, sufficient for real-time FM reception.

cs.PL↗

arXiv2022

let (rec) insertion without Effects, Lights or Magic

Let insertion in program generation is producing code with definitions (let-statements). Although definitions precede uses in generated code, during code generation `uses' come first: we might not even know a definition is needed until we encounter a reoccurring expression. Definitions are thus generated `in hindsight', which explains why this process is difficult to understand and implement -- even more so for parameterized, recursive and mutually recursive definitions. We have earlier presented an interface for let(rec) insertion -- i.e. for generating (mutually recursive) definitions. We demonstrated its expressiveness and applications, but not its implementation, which relied on effects and compiler magic. We now show how one can understand let insertion, and hence implement it in plain OCaml. We give the first denotational semantics of let(rec)-insertion, which does not rely on any effects at all. The formalization has guided the implementation of let(rec) insertion in the current version of MetaOCaml.

cs.PL↗

arXiv2019

Effects Without Monads: Non-determinism -- Back to the Meta Language

We reflect on programming with complicated effects, recalling an undeservingly forgotten alternative to monadic programming and checking to see how well it can actually work in modern functional languages. We adopt and argue the position of factoring an effectful program into a first-order effectful DSL with a rich, higher-order 'macro' system. Not all programs can be thus factored. Although the approach is not general-purpose, it does admit interesting programs. The effectful DSL is likewise rather problem-specific and lacks general-purpose monadic composition, or even functions. On the upside, it expresses the problem elegantly, is simple to implement and reason about, and lends itself to non-standard interpretations such as code generation (compilation) and abstract interpretation. A specialized DSL is liable to be frequently extended; the experience with the tagless-final style of DSL embedding shown that the DSL evolution can be made painless, with the maximum code reuse. We illustrate the argument on a simple but representative example of a rather complicated effect -- non-determinism, including committed choice. Unexpectedly, it turns out we can write interesting non-deterministic programs in an ML-like language just as naturally and elegantly as in the functional-logic language Curry -- and not only run them but also statically analyze, optimize and compile. The richness of the Meta Language does, in reality, compensate for the simplicity of the effectful DSL. The key idea goes back to the origins of ML as the Meta Language for the Edinburgh LCF theorem prover. Instead of using ML to build theorems, we now build (DSL) programs.

cs.PL↗

arXiv2018

Eff Directly in OCaml

The language Eff is an OCaml-like language serving as a prototype implementation of the theory of algebraic effects, intended for experimentation with algebraic effects on a large scale. We present the embedding of Eff into OCaml, using the library of delimited continuations or the multicore OCaml branch. We demonstrate the correctness of the embedding denotationally, relying on the tagless-final-style interpreter-based denotational semantics, including the novel, direct denotational semantics of multi-prompt delimited control. The embedding is systematic, lightweight, performant and supports even higher-order, 'dynamic' effects with their polymorphism. OCaml thus may be regarded as another implementation of Eff, broadening the scope and appeal of that language.

cs.PL↗

arXiv2017

Generating Code with Polymorphic let: A Ballad of Value Restriction, Copying and Sharing

Getting polymorphism and effects such as mutation to live together in the same language is a tale worth telling, under the recurring refrain of copying vs. sharing. We add new stanzas to the tale, about the ordeal to generate code with polymorphism and effects, and be sure it type-checks. Generating well-typed-by-construction polymorphic let-expressions is impossible in the Hindley-Milner type system: even the author believed that. The polymorphic-let generator turns out to exist. We present its derivation and the application for the lightweight implementation of quotation via a novel and unexpectedly simple source-to-source transformation to code-generating combinators. However, generating let-expressions with polymorphic functions demands more than even the relaxed value restriction can deliver. We need a new deal for let-polymorphism in ML. We conjecture the weaker restriction and implement it in a practically-useful code-generation library. Its formal justification is formulated as the research program.

cs.PL↗

arXiv2016

Stream Fusion, to Completeness

Stream processing is mainstream (again): Widely-used stream libraries are now available for virtually all modern OO and functional languages, from Java to C# to Scala to OCaml to Haskell. Yet expressivity and performance are still lacking. For instance, the popular, well-optimized Java 8 streams do not support the zip operator and are still an order of magnitude slower than hand-written loops. We present the first approach that represents the full generality of stream processing and eliminates overheads, via the use of staging. It is based on an unusually rich semantic model of stream interaction. We support any combination of zipping, nesting (or flat-mapping), sub-ranging, filtering, mapping-of finite or infinite streams. Our model captures idiosyncrasies that a programmer uses in optimizing stream pipelines, such as rate differences and the choice of a "for" vs. "while" loops. Our approach delivers hand-written-like code, but automatically. It explicitly avoids the reliance on black-box optimizers and sufficiently-smart compilers, offering highest, guaranteed and portable performance. Our approach relies on high-level concepts that are then readily mapped into an implementation. Accordingly, we have two distinct implementations: an OCaml stream library, staged via MetaOCaml, and a Scala library for the JVM, staged via LMS. In both cases, we derive libraries richer and simultaneously many tens of times faster than past work. We greatly exceed in performance the standard stream libraries available in Java, Scala and OCaml, including the well-optimized Java 8 streams.

cs.PL↗

arXiv2016

Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators

The salient feature of delimited-control operators is their ability to modify answer types during computation. The feature, answer-type modification (ATM for short), allows one to express various interesting programs such as typed printf compactly and nicely, while it makes it difficult to embed these operators in standard functional languages. In this paper, we present a typed translation of delimited-control operators shift and reset with ATM into a familiar language with multi-prompt shift and reset without ATM, which lets us use ATM in standard languages without modifying the type system. Our translation generalizes Kiselyov's direct-style implementation of typed printf, which uses two prompts to emulate the modification of answer types, and passes them during computation. We prove that our translation preserves typing. As the naive prompt-passing style translation generates and passes many prompts even for pure terms, we show an optimized translation that generate prompts only when needed, which is also type-preserving. Finally, we give an implementation in the tagless-final style which respects typing by construction.

cs.PL↗

arXiv2015

Proceedings ML Family/OCaml Users and Developers workshops

This volume collects the extended versions of selected papers originally presented at the two ACM SIGPLAN workshops: ML Family Workshop 2014 and OCaml 2014. Both were affiliated with ICFP 2014 and took place on two consecutive days, on September 4 and 5, 2014 in Gothenburg, Sweden. The ML Family workshop aims to recognize the entire extended family of ML and ML-like languages: languages that are Higher-order, Typed, Inferred, and Strict. It provides the forum to discuss common issues, both practical (compilation techniques, implementations of concurrency and parallelism, programming for the Web) and theoretical (fancy types, module systems, metaprogramming). The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of the members of the ML family. The OCaml workshop is more specifically targeted at the OCaml community, with an emphasis on new proposals and tools aiming to improve OCaml, its environment, and the functioning of the community. As such, it is interested in works on the type system, language extensions, compiler and optimizations, applications, tools, and experience reports of exciting uses.

cs.PL↗

arXiv2012

Monolingual Probabilistic Programming Using Generalized Coroutines

Probabilistic programming languages and modeling toolkits are two modular ways to build and reuse stochastic models and inference procedures. Combining strengths of both, we express models and inference as generalized coroutines in the same general-purpose language. We use existing facilities of the language, such as rich libraries, optimizing compilers, and types, to develop concise, declarative, and realistic models with competitive performance on exact and approximate inference. In particular, a wide range of models can be expressed using memoization. Because deterministic parts of models run at full speed, custom inference procedures are trivial to incorporate, and inference procedures can reason about themselves without interpretive overhead. Within this framework, we introduce a new, general algorithm for importance sampling with look-ahead.

cs.PL↗

arXiv2011

Implementing Explicit and Finding Implicit Sharing in Embedded DSLs

Aliasing, or sharing, is prominent in many domains, denoting that two differently-named objects are in fact identical: a change in one object (memory cell, circuit terminal, disk block) is instantly reflected in the other. Languages for modelling such domains should let the programmer explicitly define the sharing among objects or expressions. A DSL compiler may find other identical expressions and share them, implicitly. Such common subexpression elimination is crucial to the efficient implementation of DSLs. Sharing is tricky in embedded DSL, since host aliasing may correspond to copying of the underlying objects rather than their sharing. This tutorial summarizes discussions of implementing sharing in Haskell DSLs for automotive embedded systems and hardware description languages. The technique has since been used in a Haskell SAT solver and the DSL for music synthesis. We demonstrate the embedding in pure Haskell of a simple DSL with a language form for explicit sharing. The DSL also has implicit sharing, implemented via hash-consing. Explicit sharing greatly speeds up hash-consing. The seemingly imperative nature of hash-consing is hidden beneath a simple combinator language. The overall implementation remains pure functional and easy to reason about.

cs.PL↗

arXiv2005

Haskell's overlooked object system

Haskell provides type-class-bounded and parametric polymorphism as opposed to subtype polymorphism of object-oriented languages such as Java and OCaml. It is a contentious question whether Haskell 98 without extensions, or with common extensions, or with new extensions can fully support conventional object-oriented programming with encapsulation, mutable state, inheritance, overriding, statically checked implicit and explicit subtyping, and so on. We systematically substantiate that Haskell 98, with some common extensions, supports all the conventional OO features plus more advanced ones, including first-class lexically scoped classes, implicitly polymorphic classes, flexible multiple inheritance, safe downcasts and safe co-variant arguments. Haskell indeed can support width and depth, structural and nominal subtyping. We address the particular challenge to preserve Haskell's type inference even for objects and object-operating functions. The OO features are introduced in Haskell as the OOHaskell library. OOHaskell lends itself as a sandbox for typed OO language design.

cs.PL↗