Abstract The precision of a static analysis can be improved by increasing the context-sensitivity of the analysis. In a type-based formulation of static analysis for functional languages this can be achieved by, e.g., introducing let-polyvariance or subtyping. In this paper we go one step further by defining a higher-ranked polyvariant type system so that even properties of lambda-bound identifiers can be generalized over. We do this for dependency analysis, a generic analysis that can be instantiated to a range of different analyses that in this way all can profit. We prove that our analysis is sound with respect to a call-by-name semantics and that it satisfies a so-called noninterference property. We provide a type reconstruction algorithm that we have proven to be terminating, and sound and complete with respect to its declarative specification. Our principled description can serve as a blueprint for making other analyses higher-ranked.

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.

The popularity of JavaScript (JS) is enormous. Together with HTML and CSS, it is the core technology for modern web development. Because of the dynamic nature and complex interplay with HTML, JS applications are often error-prone and vulnerable. Despite active research efforts to devise intricate static and dynamic analyses to facilitate JS testing, the problem of test data generation for JS code interacting with the DOM has not yet been addressed. In this paper, we present a Javascript Evolutionary testing framework with DOM as an Input, called JEDI. In order to reach a target branch, it applies genetic search for relevant input parameters of the JS function in combination with the global DOM state. We conducted an empirical evaluation to study the effectiveness and efficiency of our testing framework. It shows that the genetic with restart algorithm, proposed in this paper, is able to achieve complete branch coverage for all experimental subjects, taking on average 19 seconds per branch.

The design space for type systems that support impredicative instantiation is extremely complicated. One needs to strike a balance between expressiveness, simplicity for both the end programmer and the type system implementor, and how easily the system can be integrated with other advanced type system concepts. In this paper, we propose a new point in the design space, which we call guarded impredicativity. Its key idea is that impredicative instantiation in an application is allowed for type variables that occur under a type constructor. The resulting type system has a clean declarative specification — making it easy for programmers to predict what will type and what will not —, allows for a smooth integration with GHC’s OutsideIn(X) constraint solving framework, while giving up very little in terms of expressiveness compared to systems like HMF, HML, FPH and MLF. We give a sound and complete inference algorithm, and prove a principal type property for our system.

In this paper, we apply fine-grained slicing techniques to the models generated from the Rebel modeling language before passing them on to an SMT solver. We show that our slicing techniques have a significant positive effect on performance, allowing us to verify larger problem instances and with higher path bounds than with unsliced models. For small and shallow instances, however, the overhead of slicing dominates verification time, and slicing should not be resorted to.

Puppet is a declarative language for configuration management that has rapidly gained popularity in recent years. Numerous organizations now rely on Puppet code for deploying their software systems onto cloud infrastructures. In this paper we provide a definition of code quality for Puppet code and an automated technique for measuring and rating Puppet code quality. To this end, we first explore the notion of code quality as it applies to Puppet code by performing a survey among Puppet developers. Second, we develop a measurement model for the maintainability aspect of Puppet code quality. To arrive at this measurement model, we derive appropriate quality metrics from our survey results and from existing software quality models. We implemented the Puppet code quality model in a software analysis tool. We validate our definition of Puppet code quality and the measurement model by a structured interview with Puppet experts and by comparing the tool results with quality judgments of those experts. The validation shows that the measurement model and tool provide quality judgments of Puppet code that closely match the judgments of experts. Also, the experts deem the model appropriate and usable in practice. The Software Improvement Group (SIG) has started using the model in its consultancy practice.

This special issue represents a selection of the best papers of TFP'13 and TFP'14, in substantially revised versions.The authors of the three best papers in each instance were invited to submit revised versions of their research, reflecting new developments since the TFP version of the paper.In each case, at least 30% of the material in the journal paper is new.The Symposium on Trends in Functional Programming (TFP) is dedicated to promoting new research directions related to the field of functional programming and to investigate the relationships of functional programming with other branches of computer science.It is designed to be a platform for novel and upcoming research, offering a lively environment for presenting the latest research results.A formal post-symposium refereeing process then selects a high-quality set of articles from those presented at the symposium and submitted for formal publication.The journal versions of the best papers from these proceedings then offer an opportunity for the authors to take a longer term view of their research effort s and to present new results since the original presentation at TFP.This special issue covers two instances of the TFP symposium.TFP 2013 was held in Provo, Utah in the United States of America in May 2013, hosted by Brigham Young University.For TFP 2013, 24 papers were submitted to the formal refereeing process and 10 of these were accepted by the programme committee.TFP 2014 was the main event of a series of events around functional programming, was held in Soesterberg, the Netherlands in May 2014.In total, 22 papers were submitted to the formal refereeing process and eight papers were accepted.TFP traditionally pays special attention to research students, acknowledging that students are almost by definition part of new subject trends.These papers also receive an extra round of feedback by the programme committee before they are submitted to the standard review process for formal publication.In this way, students can improve their papers before they compete within a full formal refereeing process.This is often a useful stepping stone in the process of academic publications, although in this specific special issue no student papers are presented.Details on TFP can be found on this webpage: http: //www.tifp.org/ .The paper by Joachim Breitner, Call Arity, discusses an analysis to improve run-time performance of functional programs, by eta-expanding functions based on how they are used.Introducing the notion of co-call graphs, it improves on existing analyses, enabling fusion for foldl-like functions.It has been implemented in the de facto standard Haskell compiler GHC, and part of the default setting since version 7.10.1.The paper shows by means of a benchmark that the gains are large in some cases, and good overall.Debugging has always been a challenge for (lazy) functional languages.In the paper by Maarten Faddegon and Olaf Chitil, the authors apply generic programming techniques to reduce to burden on the programmer for defining how values observed, and use metaprogramming techniques to specify which parts of those values can be observed.We would like to thank the sponsors for these two TFP instances: Erlang Solutions Ltd, Well-

In this paper we describe a variation of monotone frameworks that enables us to perform approximate typing of Python, in particular for dealing with some of its more dynamic features such as first-class functions and Python's dynamic class system. We additionally introduce a substantial number of variants of the basic analysis in order to experimentally discover which configurations attain the best balance of cost and precision. For example, the analysis allows us to be selectively flow-insensitive for certain classes of identifiers, and the amount of call-site context is configurable. Results of our evaluation include that adding call-site sensitivity and parameterized types has little effect on precision; in terms of speed call-site sensitivity is very costly. On the other hand, flow-insensitive treatment of module scope identifiers has a strongly positive effect, often both in terms of precision and speed.

We present a type and effect system for static analysis of programs written in a simplified version of iTasks. iTasks is a workflow specification language embedded in Clean, a general-purpose functional programming language. Given costs for basic tasks, our analysis calculates an upper bound of the total cost of a workflow. The analysis has to deal with the domain-specific features of iTasks, in particular parallel and sequential composition of tasks, as well as the general-purpose features of Clean, in particular let-polymorphism, higher-order functions, recursion and lazy evaluation. Costs are vectors of natural numbers where every element represents some resource, either consumable or reusable.

It is quite natural to define a software language as an extension of a base language. A compiler builder usually prefers to work on a representation in the base language, while programmers prefer to program in the extended language. As we define a language extension, we want to ensure that desugaring it into the base language is provably sound.

We discuss two adaptations of the implementation of type guards and narrowing in the TypeScript compiler. The first is an improvement on the original syntax-directed implementation, and has now replaced the original one in the TypeScript compiler. It is specifically suited for the scenario in which an IDE requests the type of a particular variable in the program. The second implementation is defined as a whole program analysis, and is therefore able to compute more precise narrowed types, but at the price of a higher run-time cost.

Abstract Constraint handling rules provide descriptions for constraint solvers. However, they fall short when those constraints specify some binding structure, like higher-rank types in a constraint-based type inference algorithm. In this paper, the term syntax of constraints is replaced by λ-tree syntax, in which binding is explicit, and a new ∇ generic quantifier is introduced, which is used to create new fresh constants.

Architectural patterns represent reusable design of software architecture at a high level of abstraction. They can be used to structure new applications and to recover the modular structure of existing systems. Techniques like Architecture Compliance Checking (ACC) focus on testing whether the realised artefacts adhere to the architecture. Typically, these techniques require a complete architecture as input. In this paper, we focus on defining architectural patterns in such a way that we can use ACC tools to recognise architectural pattern instances. This requires us to explicitly define architectural patterns in terms of allowed and disallowed software dependencies. We base ourselves on Semantically Rich Modular Architectures. Defining architectural patterns this way allows us to reason about them. For example, how patterns should be interpreted as incomplete architectures and how different interpretations affect the pattern recognition process. Recognising architectural patterns using ACC techniques also has great potential in architecture design and Software Architecture Reconstruction.

Programs often contain branches to break off from their main execution. These branches contribute to the total cost of testing, because they also need to be tested. The paper presents a new approach to improve the testing of such branches by annotating them. Our tool automatically generates test-sequences. Then, invariants in the form of pre-and post-condition over the executions passing each annotated branch are dynamically inferred, and reported to the programmer for inspection. Contradiction with the programmer's assumption on what the behavior should be indicates a bug. As invariants, a certain class of simple expressions are proposed, which are discriminative enough for testing break-off behavior, while keeping their amount feasible for inspection.

Type classes and type families are key ingredients in Haskell programming. Type classes were introduced to deal with ad-hoc polymorphism, although with the introduction of functional dependencies, their use expanded to type-level programming. Type families also allow encoding type-level functions, but more directly in the form of rewrite rules. In this paper we show that type families are powerful enough to simulate type classes (without overlapping instances), and we provide a formal proof of the soundness and completeness of this simulation. Encoding instance constraints as type families eases the path to proposed extensions to type classes, like closed sets of instances, instance chains, and control over the search procedure. The only feature which type families cannot simulate is elaboration, that is, generating code from the derivation of a rewriting. We look at ways to solve this problem in current Haskell, and propose an extension to allow elaboration during the rewriting phase.

Software modernization has been extensively researched, primarily focusing on observing the associated phenomena, and providing technical solutions to facilitate the modernization process. Software modernization is claimed to be successful when the modernization is completed using those technical solutions. Very limited research, if any, is reported with an aim at documenting the post-modernization impacts, i.e., whether any of the pre-modernization business goals are in fact achieved after modernization. In this research, we attempt to address this relative absence of empirical study through five retrospective software modernization case studies. We use an explanatory case study approach to document the pre-modernization business goals, and to decide whether those goals have been achieved. The intended benefits for each of the five cases we considered were all (partially) met, and in most cases fully. Moreover, many cases exhibited a number of unintended benefits, and some reported detrimental effects of modernization.

Topic modeling has seen a surge in use for software comprehension. Although the models inferred from the source code are a great source of knowledge, they fail to fully capture the conceptual relationships between the topics. Here we investigate the use of interactive topic modeling for source code analysis by feeding-in information from the end-users, including developers and architects, to refine the inferred topic models. We have implemented a web-based toolkit called ITMViz to provide support to interpret the topic models, and use the results to cluster modules together. A medium-sized Java project is used to evaluate our approach in understanding the software system.

In this paper we develop an object-sensitive type analysis for PHP, based on an extension of the notion of monotone frameworks to deal with the dynamic aspects of PHP, and following the framework of Smaragdakis et al. for object-sensitive analysis.

Most statically typed functional programming languages allow programmers to write partial functions: functions that are not defined on all the elements of their domain as specified by their type. Applying a partial function to a value on which it is not defined will raise a run-time exception, thus in practice well-typed programs can and do still go wrong.

In this brief announcement we outline work we have done on defining a polyvariant cardinality analysis for a non-strict higher-order language equipped with user defined datatypes and explicit strictness that includes sharing analysis, absence analysis, strictness analysis and uniqueness typing as a special case. It aims to be the basis of an analysis framework in a compiler for a Haskell-like language, that does not have access to an aggressive inliner such as the one present in GHC.

Voronoi treemaps can be used to effectively visualize software quality attributes of a given software system. To easily keep track of how the values of such attributes change over time as the software evolves from one version to the next, it is essential that the produced visualizations are stable in the sense that small changes to the values of the attributes lead to small changes in the visualization. Due to the non-deterministic nature of the standard algorithm for computing Voronoi treemaps, stability is not guaranteed. In this paper we introduce stable Voronoi treemaps for additively weighted power Voronoi diagrams. We employ scaled Hilbert curves to place Voronoi sites in the plane, thereby achieving a predictable first good approximation of the final location of the sites, and then retain the order in which sites are placed along that curve for easy comparison with revisions of the same software system. We show that our algorithm not only provides more stability, but also that because of better placement it needs fewer iterations to compute its result.

Unsupervised software clustering is the problem of automatically decomposing the software system into meaningful units. Some approaches solely rely on the structure of the system, such as the module dependency graph, to decompose the software systems into cohesive groups of modules. Other techniques focus on the informal knowledge hidden within the source code itself to retrieve the modular architecture of the system. However both techniques in the case of large systems fail to produce decompositions that correspond to the actual architecture of the system. To overcome this problem, we propose a novel approach to clustering software systems by incorporating knowledge from different viewpoints of the system, such as the knowledge embedded within the source code as well as the structural dependencies within the system, to produce a clustering. In this setting, we adopt a search-based approach to the encoding of multi-view clustering and investigate two approaches to tackle this problem, one based on a linear combination of objectives into a single objective, the other a multi-objective approach to clustering. We evaluate our approach against a set of substantial software systems. The two approaches are evaluated on a dataset comprising of 10 Java open source projects. Finally, we propose two techniques based on interpolation and hierarchical clustering to combine different results obtained to yield a single result for single-objective and multi-objective encodings, respectively.

Existing research in legacy system modernization has traditionally focused on technical challenges, and takes the standpoint that legacy systems are obsolete, yet crucial for an organization's operation. Nonetheless, it remains unclear whether practitioners in the industry also share this perception. This paper describes the outcome of an exploratory study in which 26 industrial practitioners were interviewed on what makes a software system a legacy system, what the main drivers are that lead to the modernization of such systems, and what challenges are faced during the modernization process. The findings of the interviews have been validated by means of a survey with 198 respondents. The results show that practitioners value their legacy systems highly, the challenges they face are not just technical, but also include business and organizational aspects.

We combine the type error slicing and heuristics based approaches to type error diagnostic improvement within the context of type based security analysis on a let-polymorphic call by value lambda calculus extended with lists, pairs and the security specific constructs declassify and protect. We define and motivate four classes of heuristics that help diagnose inconsistencies among the constraints, and show their effect on a selection of security incorrect programs.

Gain graphs are graphs in which each edge has a gain (a label from a group so that reversing the direction of an edge inverts the gain). In this paper we take a generalized view of gain graphs in which the gain of an edge is related to the gain of th

My main reason for wanting to read this book was to find out what a well-known publicist from the world of OO would have to say about the state of the art of domain specific languages (DSLs), in particular when it comes to type error feedback, functional programming, and the combination. As most readers will be aware, languages like Scheme and Haskell are very well suited to embed DSLs in: Scheme can be considered a core language to which new language facilities can be easily added by means of hygienic syntax macro's (Abelson et al . 1998), and there are so many papers on embedded DSLs in Haskell (Hudak, 1998), that any realistic selection would aggravate more people than I would please. Great was my disappointment when I read on page XXV that these topics were not discussed at all in the book. Although I can imagine that Fowler does not feel comfortable writing about subjects he is not sufficiently at home with, the question does arise whether the title of this book is sufficiently covered by its contents.

Legacy systems are vitally important for the continuation of business in an enterprise as they support complex core business processes. However, legacy systems have several well-known disadvantages such as being inflexible and hard to maintain, so momentum is growing to evolve those systems into new technology environments. Recently, service-oriented architecture has emerged as a promising architectural style that enables existing legacy systems to expose their functionality as services, without making significant changes to the legacy systems themselves. A significant number of the legacy to service migration approaches address the technical perspective (i.e., supporting technology) to expose the legacy code as services. The other approaches focus on determining the feasibility of the migration that includes economical and technical feasibility, based on the characteristics of existing legacy system and the requirements of the target SOA system. In this paper, a legacy to SOA migration method that does not single out the migration feasibility and technical perspectives, but combines these two perspectives of migration, is proposed. Method engineering is used to develop the migration method by reusing method fragments from existing service-oriented development methods. Then, concept slicing is used to develop the service by extracting the relevant parts of the legacy code. The method is evaluated and enhanced by interviewing experts and further validated with two case studies. The method is found to be appropriate and effective in extracting services from legacy code with the aim of reusing these services in new configurations.

When analyzing software systems we face the challenge of how to implement a particular analysis for different programming languages. A solution for this problem is to write a single analysis using a code query language, abstracting from the specificities of languages being analyzed. Over the past ten years many code query technologies have been developed, based on different formalisms. Each technology comes with its own query language and set of features. To determine the state of the art of code querying we compare the languages and tools for seven code query technologies: Grok, Rscript, JRelCal, Semmle Code, JGraLab, CrocoPat and JTransformer. The specification of a package stability metric is used as a running example to compare the languages. The comparison involves twelve criteria, some of which are concerned with properties of the query language (paradigm, types, parametrization, polymorphism, modularity, and libraries), and some of which are concerned with the tool itself (output formats, interactive interface, API support, interchange formats, extraction support, and licensing). We contextualize the criteria in two usage scenarios: interactive and tool integration. We conclude that there is no particularly weak or dominant tool. As important improvement points, we identify the lack of library mechanisms, interchange formats, and possibilities for integration with source code extractors.

Language Implementation Patterns: Create your own Domain-Specific and General Programming Languages, by Terence Parr, Pragmatic Bookshelf, http://www.pragprog.com, ISBN 9781934356456 - Volume 21 Issue 2

We present a type and effect system for flow analysis that makes essential use of higher-ranked polymorphism. We show that, for higher-order functions, the expressiveness of higher-ranked types enables us to improve on the precision of conventional let-polymorphic analyses. Modularity and decidability of the analysis are guaranteed by making the analysis of each program parametric in the analyses of its inputs; in particular, we have that higher-order functions give rise to higher-order operations on effects. As flow typing is archetypical to a whole class of type and effect systems, our approach can be used to boost the precision of a wide range of type-based program analyses for higher-order languages.

Since version 1.5, generics (parametric polymorphism) are part of the Java language. Experience with implementations of the Java Language Specification such as EJC and JAVAC has shown that the type error messages provided by these tools leave more than a little to be desired. Type error messages are often uninformative and sometimes show artifacts of the type checking process in the messages. Apparently, providing good type error messages for a language as large and complex as Java currently is, is not easy.

Adapting a strictness analyser to have it take into account explicit strictness annotations can be a tricky business. Straightforward extensions of analyses based on relevance typing are likely to either be unsafe or fail to pick the fruits of increases in strictness that are introduced through annotations. We propose a more involved adaptation of relevance typing, that can be used to derive strictness analyses that are both safe and effective in the presence of explicit strictness annotations. The resulting type system provides a firm foundation for implementations of type-based strictness analysers in compilers for lazy programming languages such as Haskell and Clean.

Since version 1.5, generics (parametric polymorphism) are part of the Java language. However, adding parametric polymorphism to a language that is built on inclusion polymorphism can be confusing to a novice programmer, because the typing rules are suddenly different and, in the case of Generic Java, quite complex. Indeed, the main Java compilers, Eclipse's EJC compiler and Sun's JAVAC, do not even accept the same set of programs. Moreover, experience with these compilers shows that the error messages provided by them leave more than a little to be desired. To alleviate the latter problem, we describe how to adapt the type inference process of Java to obtain better error diagnostics for generic method invocations. The extension has been implemented into the JastAdd extensible Java compiler.

The ICFP programming contest is a 72-hour contest, which attracts thousands of contestants from all over the world. In this report we describe what it takes to organise this contest, the main ideas behind the contest we organised, the task, how to solve it, how we created it, and how well the contestants did.

Pure functional programming languages preclude destructive updates of heap-allocated data. In such languages, all newly computed algebraic values claim freshly allocated heap space, which typically causes idiomatic programs to be notoriously inefficient when compared to their imperative and impure counterparts. We partly overcome this shortcoming by considering a syntactically light language construct for enabling user-controlled in-place updates of algebraic values. The resulting calculus, that is based on a combination of type-based uniqueness and constructor analysis, is guaranteed to maintain referential transparency and is fully compatible with existing run-time systems for nonstrict, pure functional languages.

Sharing analysis and uniqueness typing are static analyses that aim at determining which of a program's objects are to be used at most once. There are many commonalities between these two forms of usage analysis. We make their connection precise by developing an expressive generic analysis that can be instantiated to both sharing analysis and uniqueness typing. The resulting system, which combines parametric polymorphism with effect subsumption, is specified within the general framework of qualified types, so that readily available tools and techniques can be used for the development of implementations and metatheory.

We characterize the switching classes that do not contain an acyclic graph. The characterization is by means of a set of forbidden induced subgraphs. We prove that in addition to switches of the cycles C n for $n\geq 7$, there are only finitely many such graphs in 24 switching classes, all having at most 9 vertices. We give a representative of each of the 24 switching classes.

To improve the quality of type error messages in functional programming languages, we propose four techniques which influence the behaviour of constraint-based type inference processes. These techniques take the form of externally supplied type inference directives, precluding the need to make any changes to the compiler. A second advantage is that the directives are automatically checked for soundness with respect to the underlying type system. We show how the techniques can be used to improve the type error messages reported for a combinator library. More specifically, how they can help to generate error messages which are conceptually closer to the domain for which the library was developed. The techniques have all been incorporated in the Helium compiler, which implements a large subset of Haskell.

Gain graphs are graphs in which each edge has a gain (a label from a group so that reversing the direction of an edge inverts the gain). In this paper we take a generalized view of gain graphs in which the gain of an edge is related to the gain of the reverse edge by an anti-involution, i.e., an anti-automorphism of order at most two. We call these skew gain graphs. Switching classes are equivalence classes of gain graphs under the switching operation. The membership (or equivalence) problem is important to the theory of switching classes. The problem is to decide for two given skew gain graphs, on the same underlying graph and having gains from the same group, whether or not they belong to the same switching class. We give efficient algorithms. If a certain skew gain graph in the switching class has only abelian gains, then we can reduce the membership problem to an elegant problem on anti-involutions. Finally we show that the word problem can be reduced to the general membership problem, thereby establishing undecidability of the latter for some groups.