Search

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 use strong existentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.

The curriculum design is quite a challenge in the academy, mainly because it requires an adequate distribution of content for the development of the expected professional competencies regarding the available time, the necessary academic load, and their gradual progress in the higher educational institutions. Considering the above, the main objective of this work is to present and exemplify a computational solution to minimize the cost of designing curriculum plans using bio-inspired algorithms to automate and reduce errors in such a process. Specifically, the purpose of this research focuses on solving the Curriculum Mesh Balancing (BACP) problem through metaheuristic optimization based on the behavior or algorithm of fireflies and the use of functional programming in the Haskell lang curricular meshes, rolling of curricular meshes, metaheuristics; firefly algorithm, functional programming in Haskell programming language. The firefly algorithm will be applied to a set of test instances to demonstrate its effectiveness. According to the obtained results, this proposal allows the efficient gathering of solutions to the problem under study.

We prove a tight bound on the number of realized $0/1$ patterns (or equivalently on the Vapnik-Chervonenkis codensity) of definable families in models of the theory of algebraically closed valued fields with a non-archimedean valuation. Our result improves the best known result in this direction proved by Aschenbrenner, Dolich, Haskell, Macpherson and Starchenko, who proved a weaker bound in the restricted case where the characteristics of the field $K$ and its residue field are both assumed to be $0$. The bound obtained here is optimal and without any restriction on the characteristics. We obtain the aforementioned bound as a consequence of another result on bounding the Betti numbers of semi-algebraic subsets of certain Berkovich analytic spaces, mirroring similar results known already in the case of o-minimal structures and for real closed, as well as, algebraically closed fields. The latter result is the first result in this direction and is possibly of independent interest. Its proof relies heavily on recent results of Hrushovski and Loeser on the topology of semi-algebraic subsets of Berkovich analytic spaces., 40 pages. Extensively revised

We present , an extensible Stream Runtime Verification (SRV) tool, that borrows from the functional language Haskell (1) rich types for data in events and verdicts; and (2) functional features for parametrization, libraries, high-order specification transformations, etc.SRV is a formal dynamic analysis technique that generalizes Runtime Verification (RV) algorithms from temporal logics like LTL to stream monitoring, allowing the computation of verdicts richer than Booleans (quantitative values and beyond). The keystone of SRV is the clean separation between temporal dependencies and data computations. However, in spite of this theoretical separation previous engines include hardwired implementations of just a few datatypes, requiring complex changes in the tool chain to incorporate new data types. Additionally, when previous tools implement features like parametrization these are implemented in an ad-hoc way. In contrast, is implemented as a Haskell embedded DSL, borrowing datatypes and functional aspects from Haskell, resulting in an extensible engine (The tool is available open-source athttp://github.com/imdea-software/hlola). We illustrate through several examples, including a UAV monitoring infrastructure with predictive characteristics that has been validated in online runtime verification in real mission planning.

In 1904 Paul Morawitz postulated that an enzyme, which he named thrombokinase, would be the primary activator of prothrombin. Fifty years passed before J Haskell Milstone isolated, purified and functionally characterized the enzyme we now call Factor Xa. This essay summarizes Milstone's work on thrombokinase, and finds context for why his efforts succeeded while others struggled.

Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive sums, and a unit type. Since standard operational semantics is resource-agnostic, we develop a heap-based operational semantics and prove a soundness theorem that shows correct accounting of resource usage. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources in computation and single pointer property for linear resources, can be derived from this theorem. We hope that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.

The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic datatypes by a limited form of structural subtyping and environment-level intersection. We describe a fully automatic, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds.

Because of its many desirable properties, such as its ability to control effects and thus potentially disastrous race conditions, functional programming offers a viable approach to programming modern multicore computers. Over the past decade several parallel functional languages, typically based on dialects of ML and Haskell, have been developed. These languages, however, have traditionally underperformed procedural languages (such as C and Java). The primary reason for this is their hunger for memory, which only grows with parallelism, causing traditional memory management techniques to buckle under increased demand for memory. Recent work opened a new angle of attack on this problem by identifying a memory property of determinacy-race-free parallel programs, called disentanglement, which limits the knowledge of concurrent computations about each other’s memory allocations. The work has showed some promise in delivering good time scalability. In this paper, we present provably space-efficient automatic memory management techniques for determinacy-race-free functional parallel programs, allowing both pure and imperative programs where memory may be destructively updated. We prove that for a program with sequential live memory of R * , any P -processor garbage-collected parallel run requires at most O ( R * · P ) memory. We also prove a work bound of O ( W + R * P ) for P -processor executions, accounting also for the cost of garbage collection. To achieve these results, we integrate thread scheduling with memory management. The idea is to coordinate memory allocation and garbage collection with thread scheduling decisions so that each processor can allocate memory without synchronization and independently collect a portion of memory by consulting a collection policy, which we formulate. The collection policy is fully distributed and does not require communicating with other processors. We show that the approach is practical by implementing it as an extension to the MPL compiler for Parallel ML. Our experimental results confirm our theoretical bounds and show that the techniques perform and scale well.

In this paper, we propose a framework capable of dealing with anaphora and ellipsis which is both general and algorithmic. This generality is ensured by the compination of two general ideas. First, we use a dynamic semantics which reperent effects using a monad structure. Second we treat scopes flexibly, extending them as needed. We additionally implement this framework as an algorithm which translates abstract syntax to logical formulas. We argue that this framework can provide a unified account of a large number of anaphoric phenomena. Specifically, we show its effectiveness in dealing with pronominal and VP-anaphora, strict and lazy pronouns, lazy identity, bound variable anaphora, e-type pronouns, and cataphora. This means that in particular we can handle complex cases like Bach–Peters sentences, which require an account dealing simultaneously with several phenomena. We use Haskell as a meta-language to present the theory, which also consitutes an implementation of all the phenomena discussed in the paper. To demonstrate coverage, we propose a test suite that can be used to evaluate computational approaches to anaphora.

We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

Resumen: El principal objetivo de este trabajo es presentar y ejemplificar una solución computacional para minimizar el costo de diseñar planes curriculares mediante algoritmos bio-inspirados con el fin de automatizar y reducir los errores. Se resuelve el problema de balanceo de mallas curriculares (BACP, por sus siglas en inglés) mediante la metaheurística de optimización basada en el comportamiento o algoritmo de las luciérnagas y el uso de programación funcional en el lenguaje Haskell. Se aplica el algoritmo de las luciérnagas sobre un conjunto de instancias de prueba para demostrar su efectividad. Los resultados muestran que al aplicar la propuesta de funciones solución en los problemas de optimización de carga académica balanceada de ocho, diez y doce semestres, el rendimiento considerando 50 ejecuciones suele ser oscilante, pero permite obtener los valores esperados de mínima carga académica para cada caso. Se concluye que esta propuesta permite la generación eficiente de soluciones para el diseño de planes curriculares. Abstract: The main objective of this study is to present and exemplify a computational solution to minimize the cost of designing curriculum plans by using bio-inspired algorithms to automate and reduce errors. The study focuses on solving the balanced academic curriculum problem (BACP) through metaheuristic optimization, based on the behavior or algorithm of fireflies and based on the use of functional programming in the Haskell language. The firefly algorithm is applied to a set of test instances to demonstrate its effectiveness. The results show that by applying the proposed solution function to optimize load balance in curricular meshes of eight, 10, and 12 semesters, the performance is oscillating when considering 50 runs. But, it permits obtaining expected values for the minimum academic load in each case. It is concluded that the proposal presented here allows generating efficient solutions for designing balanced curricular meshes.

We present Hoogle+, a web-based API discovery tool for Haskell. A Hoogle+ user can specify a programming task using either a type, a set of input-output tests, or both. Given a specification, the tool returns a list of matching programs composed from functions in popular Haskell libraries, and annotated with automatically-generated examples of their behavior. These features of Hoogle+ are powered by three novel techniques. First, to enable efficient type-directed synthesis from tests only, we develop an algorithm that infers likely type specifications from tests . Second, to return high-quality programs even with ambiguous specifications, we develop a technique that automatically eliminates meaningless and repetitive synthesis results . Finally, we show how to extend this elimination technique to automatically generate informative inputs that can be used to demonstrate program behavior to the user. To evaluate the effectiveness of Hoogle+ compared with traditional API search techniques, we perform a user study with 30 participants of varying Haskell proficiency. The study shows that programmers equipped with Hoogle+ generally solve tasks faster and were able to solve 50% more tasks overall.

This paper presents an extension to Liquid Haskell that facilitates stating and semi-automatically proving properties of typeclasses. Liquid Haskell augments Haskell with refinement types —our work allows such types to be attached to typeclass method declarations, and ensures that instance implementations respect these types. The engineering of this extension is a modular interaction between GHC, the Glasgow Haskell Compiler, and Liquid Haskell’s core proof infrastructure. The design sheds light on the interplay between modular proofs and typeclass resolution, which in Haskell is coherent by default (meaning that resolution always selects the same implementation for a particular instantiating type), but in other dependently typed languages is not. We demonstrate the utility of our extension by using Liquid Haskell to modularly verify that 34 instances satisfy the laws of five standard typeclasses. More substantially, we implement a framework for programming distributed applications based on replicated data types (RDTs). We define a typeclass whose Liquid Haskell type captures the mathematical properties RDTs should satisfy; prove in Liquid Haskell that these properties are sufficient to ensure that replicas’ states converge despite out-of-order update delivery; implement (and prove correct) several instances of our RDT typeclass; and use them to build two realistic applications, a multi-user calendar event planner and a collaborative text editor.

For the rapid development of internetware, functional programming languages, such as Haskell and Scala, can be used to implement complex domain-specific applications. In functional programming languages, a higher-order function is a function that takes functions as parameters or returns a function. Using higher-order functions in programs can increase the generality and reduce the redundancy of source code. To test a higher-order function, a tester needs to check the requirements and write another function as the test input. However, due to the complex structure of higher-order functions, testing higher-order functions is a time-consuming and labor-intensive task. Testers have to spend an amount of manual effort in testing all higher-order functions. Such testing is infeasible if the time budget is limited, such as a period before a project release. In practice, not every higher-order function is actually called. We refer to higher-order functions that are about to be called as calling-prone ones. Calling-prone higher-order functions should be tested first. In this paper, we propose an automatic approach, namely Phof, which predicts whether a higher-order function of Scala programs will be called in the future, i.e., identifying calling-prone higher-order functions. Our approach can assist testers to reduce the number of higher-order functions of Scala programs under test. In Phof, we extracted 24 features from source code and logs to train a predictive model based on known higher-order function calls. We empirically evaluated our approach on 4 832 higher-order functions from 27 real-world Scala projects. Experimental results show that Phof based on the random forest algorithm and the Synthetic Minority Oversampling Technique Processing strategy (SMOTE) performs well in the prediction of calls of higher-order functions. Our work can be used to support the scheduling of limited test resources.

Type inference is a feature that is common to a variety of programming languages. While, in the past, it has been prominently present in functional ones (e.g., ML and Haskell), today, many object-oriented/multi-paradigm languages such as C# and C++ offer, to a certain extent, such a feature. Nevertheless, type inference still is an unexplored subject in the realm of C. In particular, it remains open whether it is possible to devise a technique that encompasses the idiosyncrasies of this language. The first difficulty encountered when tackling this problem is that parsing C requires, not only syntactic, but also semantic information. Yet, greater challenges emerge due to C’s intricate type system. In this work, we present a unification-based framework that lets us infer the missing struct, union, enum, and typedef declarations in a program. As an application of our technique, we investigate the reconstruction of partial programs. Incomplete source code naturally appears in software development: during design and while evolving, testing, and analyzing programs; therefore, understanding it is a valuable asset. With a reconstructed well-typed program, one can: (i) enable static analysis tools in scenarios where components are absent; (ii) improve precision of “zero setup” static analysis tools; (iii) apply stub generators, symbolic executors, and testing tools on code snippets; and (iv) provide engineers with an assortment of compilable benchmarks for performance and correctness validation. We evaluate our technique on code from a variety of C libraries, including GNU’s Coreutils and on snippets from popular projects such as CPython, FreeBSD, and Git.

Modern functional programming languages, such as Haskell, Scala, ML, and F#, have properties that make it possible to implement logically complicated algorithms relatively easily. Among such properties is the composition of functions, currying, metafunctions (functions over functions), and some others. This makes it possible to obtain complex functions by combining simpler functions. An example of a complicated algorithm is a parser. In Haskell, there is a library called Parsec, which is a set of elementary parsers; by combining these parsers, one can create more complicated parsers. This fact makes the library relatively simple, yet powerful. The majority of these tools are not explicitly included in C++. However, C++ is sufficiently powerful for implementing many properties of functional programming languages. In this paper, an attempt is made to develop such a library.

Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.

Implicit functions are dependently typed functions, such that arguments are provided (by default) by inference machinery instead of programmers of the surface language. Implicit functions in Agda are an archetypal example. In the Haskell language as implemented by the Glasgow Haskell Compiler (GHC), polymorphic types are another example. Implicit function types are first-class if they are treated as any other type in the surface language. This holds in Agda and partially holds in GHC. Inference and elaboration in the presence of first-class implicit functions poses a challenge; in the context of Haskell and ML-like languages, this has been dubbed “impredicative instantiation” or “impredicative inference”. We propose a new solution for elaborating first-class implicit functions, which is applicable to full dependent type theories and compares favorably to prior solutions in terms of power, generality and simplicity. We build atop Norell’s bidirectional elaboration algorithm for Agda, and we note that the key issue is incomplete information about insertions of implicit abstractions and applications. We make it possible to track and refine information related to such insertions, by adding a function type to a core Martin-L'of type theory, which supports strict (definitional) currying. This allows us to represent undetermined domain arities of implicit function types, and we can decide at any point during elaboration whether implicit abstractions should be inserted.

Regular expressions are part of every programmer’s toolbox. They are used for a wide variety of language-related tasks and there are many algorithms for manipulating them. In particular, matching algorithms that detect whether a word belongs to the language described by a regular expression are well explored, yet new algorithms appear frequently. However, there is no satisfactory methodology for testing such matchers. We propose a testing methodology which is based on generating positive as well as negative examples of words in the language. To this end, we present a new algorithm to generate the language described by a generalized regular expression with intersection and complement operators. The complement operator allows us to generate both positive and negative example words from a given regular expression. We implement our generator in Haskell and OCaml and show that its performance is more than adequate for testing.

We present KReach, a tool for deciding reachability in general Petri nets. The tool is a full implementation of Kosaraju’s original 1982 decision procedure for reachability in VASS. We believe this to be the first implementation of its kind. We include a comprehensive suite of libraries for development with Vector Addition Systems (with States) in the Haskell programming language. KReach serves as a practical tool, and acts as an effective teaching aid for the theory behind the algorithm. Preliminary tests suggest that there are some classes of Petri nets for which we can quickly show unreachability. In particular, using KReach for coverability problems, by reduction to reachability, is competitive even against state-of-the-art coverability checkers.\ud \ud

The earthquake magnitude prediction is a task of utmost difficulty that has been addressed by using many different strategies, with no further transformation thus far. This work evaluates the Haskell based deterministic dendritic cell algorithm (hDCA)’s accuracy when used to predict earthquake magnitude in Sichuan and surroundings. First, eight seismicity indicators have been retrieved from the literature and used as input for the algorithms, and they are calculated from the earthquake catalog of the Sichuan and surroundings by well-known geophysical theory, named Gutenberg-Richter inverse power-law, and characteristic earthquake magnitude distribution and also conclusions drawn by recent related studies. Then, the hDCA is used to predict earthquakes with magnitude larger than 4.5 in the next month. In this work, the proposed method has been compared to the well-known machine learning algorithms, such as Dendritic Cell Algorithm (DCA), Support Vector Machine (SVM), K-Nearest Neighbor (KNN), Back Propagation Neural Network (BPNN), Recurrent Neural Network (RNN), Probabilistic Neural Network (PNN) and Neural Dynamic Classification (NDC). Overall our method yields the promising results in terms of all qualify parameters evaluated.

We expose some basic elements of a style of programming supported by functional languages like Haskell by relating them to a coherent set of notions and techniques from Curry’s work in combinatory logic and formal systems, and their algebraic and categorical interpretations. Our account takes the form of a commentary to a simple fragment of Haskell code attempting to isolate the conceptual sources of the linguistic abstractions involved.