Constraint Programming (CP) is a declarative paradigm where a programmer models a problem in terms of constraints over some set of variables. Monadic Constraint Programming (MCP) integrates CP with functional programming by modeling the constraint solver as a monad threaded through a monadic search tree. This abstraction allows us to define search as a first-class object which can be constructed from composable search transformers. We introduce Effectful Constraint Programming (ECP), a re-imagining of monadic constraint programming using the increasingly-popular framework of algebraic effects and handlers. To overcome the performance drawbacks of effects, we use multi-stage programming to generate efficient search procedures from high-level, abstract descriptions.
Structural operational semantics (SOS) is one of the most common formalisms for specifying language semantics. There has been much interest in automatically deriving small-step SOS definitions from big-step definitions and vice versa, as well as towards extrapolating language implementations from these inductive, declarative definitions. This work presents Computation-Tree Semantics (CTS) in which semantic configurations are tree-structured, unlike standard SOS-configurations which are "flat". This tree-structure is key in making our approach algorithmic, meaning it is able to describe how a transition is produced, contrary to the traditional declarative approach taken by SOS. We show how one can - in a straight-forward manner - obtain a CTS from the big-step semantics of a simple arithmetic language, a simple while language, and the call-by-need lambda-calculus as given by Launchbury. From the resulting CTS, we then obtain a small-step understanding of all these languages. The arithmetic language example is formalised in Coq/Rocq.
Many synthesizers implicitly benefit from using polymorphic types, since parametric polymorphism reduces the search space. Additional synthesis constraints may interfere with parametricity. In particular, a polymorphic type may cause otherwise feasible input-output examples to contradict each other. We present TAXI (type-and-example based inferencer), a tool for efficiently reasoning about the feasibility of polymorphic programs specified by input-output examples, and DRIVER, a tactic language for top-down program synthesis that uses feasibility reasoning to prune the search space. TAXI guarantees that every search state corresponds to a correct (albeit possibly partial) implementation. In addition, it allows for shortcutting the synthesis when a subspecification covers all cases. We show that these techniques have the potential to speed up top-down enumerative type-and-example driven synthesizers.
Syntactic sugars ease the definition of new language constructs by transforming them into an existing core language. Previous works lift independent typing rules and other semantics for these new constructs from the core language. The lifted semantics preserve the abstraction boundary of syntactic sugars, freeing users from inspecting desugared code that they did not write. While sugars may interact with contextual information during desugaring in general, these works are limited to simple sugars that do not. We identify a class of contextual sugars and present an extended algorithm for lifting their typing rules. With the addition of contexts, naively representing desugaring results in the core language may cause unexpected behavior and break hygiene. We introduce anchored terms that can point to the provenance of their contexts to represent desugaring results, which is similar to mechanisms used in Racket macros. Anchored terms need not concern authors or users of contextual sugars, but enable local reasoning. The lifted typing rules are sound with respect to the typing of anchored core language terms.
