An official website of the United States government
We consider the problem of type-directed component-based synthesis where, given a set of (typed) components and a querytype, the goal is to synthesize atermthat inhabits the query. Classical approaches based on proof search in intuitionistic logics do not scale up to the standard libraries of modern languages, which span hundreds or thousands of components. Recent graph reachability based methods proposed for Java do scale, but only apply to monomorphic data and components: polymorphic data and components infinitely explode the size of the graph that must be searched, rendering synthesis intractable. We introducetype-guided abstraction refinement(TYGAR), a new approach for scalable type-directed synthesis over polymorphic datatypes and components. Our key insight is that we can overcome the explosion by building a graph overabstract typeswhich represent a potentially unbounded set of concrete types. We show how to use graph reachability to search for candidate terms over abstract types, and introduce a new algorithm that usesproofs of untypeabilityof ill-typed candidates to iterativelyrefinethe abstraction until a well-typed result is found. We have implemented TYGAR in H+, a tool that takes as input a set of Haskell libraries and a query type, and returns a Haskell term that uses functions from the provided libraries to implement the query type. Our support for polymorphism allows H+ to work with higher-order functions and type classes, and enables more precise queries due to parametricity. We have evaluated H+ on 44 queries using a set of popular Haskell libraries with a total of 291 components. H+ returns an interesting solution within the first five results for 32 out of 44 queries. Our results show that TYGAR allows H+ to rapidly return well-typed terms, with the median time to first solution of just 1.4 seconds. Moreover, we observe that gains from iterative refinement over exhaustive enumeration are more pronounced on harder queries.
more »
« less
Generating Well-Typed Terms That Are Not “Useless”
Random generation of well-typed terms lies at the core of effective random testing of compilers for functional languages. Existing techniques have had success following a top-down type-oriented approach to generation that makes choices locally, which suffers from an inherent limitation: the type of an expression is often generated independently from the expression itself. Such generation frequently yields functions with argument types that cannot be used to produce a result in a meaningful way, leaving those arguments unused. Such “use-less” functions can hinder both performance, as the argument generation code is dead but still needs to be compiled, and effectiveness, as a lot of interesting optimizations are tested less frequently. In this paper, we introduce a novel algorithm that is significantly more effective at generating functions that use their arguments. We formalize both the “local” and the “nonlocal” algorithms as step-relations in an extension of the simply-typed lambda calculus with type and arguments holes, showing how delaying the generation of types for subexpressions by allowing nonlocal generation steps leads to “useful” functions. We implement our algorithm demonstrating that it’s much closer to real programs in terms of argument usage rate, and we replicate a case study from the literature that finds bugs in the strictness analyzer of GHC, with our approach finding bugs four times faster than the current state-of-the-art local approach.
more »
« less
- PAR ID:
- 10603038
- Publisher / Repository:
- Association for Computing Machinery (ACM)
- Date Published:
- Journal Name:
- Proceedings of the ACM on Programming Languages
- Volume:
- 8
- Issue:
- POPL
- ISSN:
- 2475-1421
- Format(s):
- Medium: X Size: p. 2318-2339
- Size(s):
- p. 2318-2339
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
It is well-known that GADTs do not admit standard map functions of the kind supported by ADTs and nested types. In addition, standard map functions are insufficient to distribute their data-changing argument functions over all of the structure present in elements of deep GADTs, even just deep ADTs or nested types. This paper develops an algorithm that characterizes those functions on a (deep) GADT’s type arguments that are mappable over its elements. The algorithm takes as input a term t whose type is an instance of a (deep) GADT G, and returns a set of constraints a function must satisfy to be mappable over t. This algorithm, and thus this paper, can in some sense be read as defining what it means for a function to be mappable over t: f is mappable over an element t of G precisely when it satisfies the constraints returned when our algorithm is run on t and G. This is significant: to our knowledge, there is no existing definition or other characterization of the intuitive notion of mappability for functions over GADTs.more » « less
-
Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. This paper, set in the context of Haskell, presents a bidirectional type-inference algorithm that infers where to introduce and eliminate existentials without any annotations in terms, along with an explicitly typed, type-safe core language usable as a compilation target. This approach is backward compatible. The key ingredient is to usestrongexistentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.more » « less
-
Effective argumentation is essential towards a purposeful conversation with a satisfactory outcome. For example, persuading someone to reconsider smoking might involve empathetic, well founded arguments based on facts and expert opinions about its ill-effects and the consequences on one’s family. However, the automatic generation of high-quality factual arguments can be challenging. Addressing existing controllability issues can make the recent advances in computational models for argument generation a potential solution. In this paper, we introduce ArgU: a neural argument generator capable of producing factual arguments from input facts and real-world concepts that can be explicitly controlled for stance and argument structure using Walton’s argument scheme-based control codes. Unfortunately, computational argument generation is a relatively new field and lacks datasets conducive to training. Hence, we have compiled and released an annotated corpora of 69,428 arguments spanning six topics and six argument schemes, making it the largest publicly available corpus for identifying argument schemes; the paper details our annotation and dataset creation framework. We further experiment with an argument generation strategy that establishes an inference strategy by generating an “argument template” before actual argument generation. Our results demonstrate that it is possible to automatically generate diverse arguments exhibiting different inference patterns for the same set of facts by using control codes based on argument schemes and stance.more » « less
-
TheIsing modelof statistical physics has served as a keystone example of phase transitions, thermodynamic limits, scaling laws, and many other phenomena and mathematical methods. We introduce and explore anIsing game, a variant of the Ising model that features competing agents influencing the behavior of the spins. With long-range interactions, we consider a mean-field limit resulting in a nonlocal potential game at the mesoscopic scale. This game exhibits a phase transition and multiple constant Nash-equilibria in the supercritical regime. Our analysis focuses on a sharp interface limit for which potential minimizing solutions to the Ising game concentrate on two of the constant Nash-equilibria. We show that the mesoscopic problem can be recast as a mixed local/nonlocal space-time Allen-Cahn type minimization problem. We prove, using a Γ-convergence argument, that the limiting interface minimizes a space-time anisotropic perimeter type energy functional. This macroscopic scale problem could also be viewed as a problem of optimal control of interface motion. Sharp interface limits of Allen-Cahn type functionals have been well studied. We build on that literature with new techniques to handle a mixture of local derivative terms and nonlocal interactions. The boundary conditions imposed by the game theoretic considerations also appear as novel terms and require special treatment.more » « less
