Another DSL for pictures? Seems fishy. But hold fast as we chart a course to an embedded DSL for the domain of slide presentations with animations. Our DSL programs interact with the host language in two ways: by allowing pictures and animations to be built using host-language functions (resembling a shallow embedding), and by allowing host-language reflection on their construction (resembling a deep embedding). As a result, users can define their own animation combinators but still also inspect, adjust, and reassemble animations. To demonstrate our DSL’s expressive power, we show how it supports a Keynote-like Magic Move operation. Having made the DSL shipshape, we dive into a lesson learned about deep and shallow DSL design. While deep and shallow may seem like mutually exclusive options, we argue they are actually points on an entire spectrum of possible DSL designs. More importantly, our paper demonstrates that points on the spectrum between deep and shallow are where DSL designs achieve full sail.
A transient data structure is a combination of an ephemeral data structure, a persistent data structure, and fast conversions between them. We present a transient sequence data structure that supports efficient read and write access at an arbitrary index with worst-case time complexity O ( K log K n ), pushing and popping at either end with complexity O ( K log K n ), and splitting and concatenation with complexity O K log K n + log K 2 n , where K is a user-defined chunk size and n is the length of the sequence. We provide a detailed analysis of this data structure and show that, in many favorable scenarios, it performs much better than these pessimistic bounds might suggest. Furthermore, we describe its implementation, and provide a synthetic benchmark to evaluate the performance of push and pop . We believe that it is a good candidate for a one-size-fits-all, general-purpose sequence data structure.
We propose yet another approach to type inference with first-class implicit polymorphism, based on the interleaving of an Algorithm ℳ-style constraint-generating elaboration of terms and a solver for the generated constraints. The novelty of our approach is that types include explicit syntactic representations of unknown polymorphic types during type inference. Solving unification constraints with unknown polymorphic types also computes type arguments for the elaborated terms. The resulting system is uniform, simple, extends to support domain-specific constraints, and compares favorably with other approaches to first-class implicit polymorphism.
This article extends tail-call optimisation by applying it to asynchronous calls. We first introduce Tail-Modulo-Await , a novel code transformation for asynchronous tail recursive functions that prevents the creation of unnecessary tasks. We then show how to combine Tail-Modulo-Await with the existing Tail-Modulo-Cons optimisation; we obtain an optimisation able to turn a recursive function with multiple tail calls under constructors into a parallel version of the function, also optimised in space. We formalise both optimisations over representative calculi, and prove them correct through backward simulations. Finally, we provide a proof-of-concept implementation as an OCaml syntax extension and evaluate it experimentally, showing our approach optimises both memory and execution time.
We study a first-class treatment of constrained types, which were previously confined mostly to ML-style polymorphism. We define System FCCT, an extension of System F with polymorphic subtyping and constraint abstraction in types. A value of type c ⇒ τ can be used at type τ in any context where the subtyping constraint c can be discharged. We show that FCCT exhibits interesting properties. First, all well-typed FCCT terms terminate under call-by-name evaluation (CBN), which can be shown by elaboration into System F. Second, all CBN-terminating terms are well-typed in FCCT. Together, these two properties mean that typability in System FCCT characterizes call-by-name termination. Third, FCCT admits a principal type inference semialgorithm, called FCCT ℐ , which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCT ℐ indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCT ℐ to track abstracted call contexts and perform approximation by sharing polymorphic instantiations, ensuring termination on all input terms while preserving soundness. In addition to making the connection between polymorphic subtype constraint solving and term reduction, this paper also establishes a connection between constrained types and existing intersection type systems, which are known to characterize various normalization properties.
