skip to main content

Explore Research Products in the NSF-PAR

Title: A computational interpretation of compact closed categories: reversible programming with negative and fractional types
Compact closed categories include objects representing higher-order functions and are well-established as models of linear logic, concurrency, and quantum computing. We show that it is possible to construct such compact closed categories for conventional sum and product types by defining a dual to sum types, a negative type, and a dual to product types, a fractional type. Inspired by the categorical semantics, we define a sound operational semantics for negative and fractional types in which a negative type represents a computational effect that ``reverses execution flow'' and a fractional type represents a computational effect that ``garbage collects'' particular values or throws exceptions. Specifically, we extend a first-order reversible language of type isomorphisms with negative and fractional types, specify an operational semantics for each extension, and prove that each extension forms a compact closed category. We furthermore show that both operational semantics can be merged using the standard combination of backtracking and exceptions resulting in a smooth interoperability of negative and fractional types. We illustrate the expressiveness of this combination by writing a reversible SAT solver that uses backtracking search along freshly allocated and de-allocated locations. The operational semantics, most of its meta-theoretic properties, and all examples are formalized in a supplementary Agda package.  more » « less
Award ID(s):
1936353
NSF-PAR ID:
10296315
Author(s) / Creator(s):
;
Date Published:
Journal Name:
Proceedings of the ACM on Programming Languages
Volume:
5
Issue:
POPL
ISSN:
2475-1421
Page Range / eLocation ID:
1 to 29
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; ( , Proceedings of the ACM on Programming Languages)
    Hicks, Michael (Ed.)
    We propose a novel approach to soundly combining linear types with multi-shot effect handlers. Linear type systems statically ensure that resources such as file handles and communication channels are used exactly once. Effect handlers provide a rich modular programming abstraction for implementing features ranging from exceptions to concurrency to backtracking. Whereas conventional linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded (e.g. for exceptions) or invoked more than once (e.g. for backtracking). This mismatch leads to soundness bugs in existing systems such as the programming language Links, which combines linearity (for session types) with effect handlers. We introduce control-flow linearity as a means to ensure that continuations are used in accordance with the linearity of any resources they capture, ruling out such soundness bugs. We formalise the notion of control-flow linearity in a System F-style core calculus Feff∘, equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove that Feff∘ preserves the integrity of linear values in the sense that no linear value is discarded or duplicated. In order to show that control-flow linearity can be made practical, we adapt Links based on the design of Feff∘, in doing so fixing a long-standing soundness bug. Finally, to better expose the potential of control-flow linearity, we define an ML-style core calculus Qeff∘, based on qualified types, which requires no programmer provided annotations, and instead relies entirely on type inference to infer control-flow linearity. Both linearity and effects are captured by qualified types. Qeff∘ overcomes a number of practical limitations of Feff∘, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity. 
    more » « less
  2. ; ( , Logic in Computer Science)
    We present a grammar for a robust class of data types that includes algebraic data types (ADTs), (truly) nested types, generalized algebraic data types (GADTs), and their higher-kinded analogues. All of the data types our grammar defines, as well as their associated type constructors, are shown to have fully functorial initial algebra semantics in locally presentable categories. Since local presentability is a modest hypothesis, needed for such semantics for even the simplest ADTs, our semantic framework is actually quite conservative. Our results thus provide evidence that if a category supports fully functorial initial algebra semantics for standard ADTs, then it does so for advanced higher-kinded data types as well. To give our semantics we introduce a new type former called Lan that captures on the syntactic level the categorical notion of a left Kan extension. We show how left Kan extensions capture propagation of a data type’s syntactic generators across the entire universe of types, via a certain completion procedure, so that the type constructor associated with a data type becomes a bona fide functor with a canonical action on morphisms. A by-product of our semantics is a precise measure of the semantic complexity of data types, given by the least cardinal λ for which the functor underlying a data type is λ-accessible. The proof of our main result allows this cardinal to be read off from a data type definition without much effort. It also gives a sufficient condition for a data type to have semantic complexity ω, thus characterizing those data types whose data elements are effectively enumerable. 
    more » « less
  3. ; ; ; ( , Biological Cybernetics)
    Abstract

    Negative correlations in the sequential evolution of interspike intervals (ISIs) are a signature of memory in neuronal spike-trains. They provide coding benefits including firing-rate stabilization, improved detectability of weak sensory signals, and enhanced transmission of information by improving signal-to-noise ratio. Primary electrosensory afferent spike-trains in weakly electric fish fall into two categories based on the pattern of ISI correlations: non-bursting units have negative correlations which remain negative but decay to zero with increasing lags (Type I ISI correlations), and bursting units have oscillatory (alternating sign) correlation which damp to zero with increasing lags (Type II ISI correlations). Here, we predict and match observed ISI correlations in these afferents using a stochastic dynamic threshold model. We determine the ISI correlation function as a function of an arbitrary discrete noise correlation function$${{\,\mathrm{\mathbf {R}}\,}}_k$$Rk, wherekis a multiple of the mean ISI. The function permits forward and inverse calculations of the correlation function. Both types of correlation functions can be generated by adding colored noise to the spike threshold with Type I correlations generated with slow noise and Type II correlations generated with fast noise. A first-order autoregressive (AR) process with a single parameter is sufficient to predict and accurately match both types of afferent ISI correlation functions, with the type being determined by the sign of the AR parameter. The predicted and experimentally observed correlations are in geometric progression. The theory predicts that the limiting sum of ISI correlations is$$-0.5$$-0.5yielding a perfect DC-block in the power spectrum of the spike train. Observed ISI correlations from afferents have a limiting sum that is slightly larger at$$-0.475 \pm 0.04$$-0.475±0.04($$\text {mean} \pm \text {s.d.}$$mean±s.d.). We conclude that the underlying process for generating ISIs may be a simple combination of low-order AR and moving average processes and discuss the results from the perspective of optimal coding.

     
    more » « less
  4. ; ; ( , Mathematical Programming Computation)
    Abstract In recent work, we provide computational arguments for expanding the class of proper cones recognized by conic optimization solvers, to permit simpler, smaller, more natural conic formulations. We define an exotic cone as a proper cone for which we can implement a small set of tractable (i.e. fast, numerically stable, analytic) oracles for a logarithmically homogeneous self-concordant barrier for the cone or for its dual cone. Our extensible, open-source conic interior point solver, Hypatia, allows modeling and solving any conic problem over a Cartesian product of exotic cones. In this paper, we introduce Hypatia’s interior point algorithm, which generalizes that of Skajaa and Ye (Math. Program. 150(2):391–422, 2015) by handling exotic cones without tractable primal oracles. To improve iteration count and solve time in practice, we propose four enhancements to the interior point stepping procedure of Skajaa and Ye: (1) loosening the central path proximity conditions, (2) adjusting the directions using a third order directional derivative barrier oracle, (3) performing a backtracking search on a curve, and (4) combining the prediction and centering directions. We implement 23 useful exotic cones in Hypatia. We summarize the complexity of computing oracles for these cones and show that our new third order oracle is not a bottleneck. From 37 applied examples, we generate a diverse benchmark set of 379 problems. Our computational testing shows that each stepping enhancement improves Hypatia’s iteration count and solve time. Altogether, the enhancements reduce the geometric means of iteration count and solve time by over 80% and 70% respectively. 
    more » « less
  5. ; ; ; ; ; ; ; ; ; ; et al ( , PLOS Computational Biology)
    Pascual, Mercedes (Ed.)
    When Darwin visited the Galapagos archipelago, he observed that, in spite of the islands’ physical similarity, members of species that had dispersed to them recently were beginning to diverge from each other. He postulated that these divergences must have resulted primarily from interactions with sets of other species that had also diverged across these otherwise similar islands. By extrapolation, if Darwin is correct, such complex interactions must be driving species divergences across all ecosystems. However, many current general ecological theories that predict observed distributions of species in ecosystems do not take the details of between-species interactions into account. Here we quantify, in sixteen forest diversity plots (FDPs) worldwide, highly significant negative density-dependent (NDD) components of both conspecific and heterospecific between-tree interactions that affect the trees’ distributions, growth, recruitment, and mortality. These interactions decline smoothly in significance with increasing physical distance between trees. They also tend to decline in significance with increasing phylogenetic distance between the trees, but each FDP exhibits its own unique pattern of exceptions to this overall decline. Unique patterns of between-species interactions in ecosystems, of the general type that Darwin postulated, are likely to have contributed to the exceptions. We test the power of our null-model method by using a deliberately modified data set, and show that the method easily identifies the modifications. We examine how some of the exceptions, at the Wind River (USA) FDP, reveal new details of a known allelopathic effect of one of the Wind River gymnosperm species. Finally, we explore how similar analyses can be used to investigate details of many types of interactions in these complex ecosystems, and can provide clues to the evolution of these interactions. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email