title: Automated Generation of Code Contracts: Generative AI to the Rescue?

authors:
Sandra Greiner
Noah Bühlmann
Manuel Ohrndorf
Christos Tsigkanos
Oscar Nierstrasz
Timo Kehrer

abstract: Design by Contract represents an established, lightweight paradigm for engineering reliable and robust software systems by specifying verifiable expectations and obligations between software components. Due to its laborious nature, developers hardly adopt Design by Contract in practice. A plethora of research on (semi-)-automated inference to reduce the manual burden has not improved the adoption of so-called code contracts in practice. This paper examines the potential of Generative AI to automatically generate code contracts in terms of pre- and postconditions for any Java project without requiring any additional auxiliary artifact. To fine-tune two state-of-the-art Large Language Models, CodeT5 and CodeT5+, we derive a dataset of more than 14k Java methods comprising contracts in form of Java Modeling Language (JML) annotations, and train the models on the task of generating contracts. We examine the syntactic and semantic validity of the contracts generated for software projects not used in the fine-tuning and find that more than 95% of the generated contracts are syntactically correct and exhibit remarkably high completeness and semantic correctness. To this end, our fully automated method sets the stage for future research and eventual broader adoption of Design by Contract in software development practice.


venue: gpce

title: Specializing Data Access in a Distributed File System (Generative Pearl)

authors:
Pratyush Das
Anxhelo Xhebraj
Tiark Rompf

abstract: We propose DDLoader, a system that embeds information about data partitioning and data distribution in distributed file systems using a metaprogramming framework. We demonstrate that this technique has practical benefits for building applications that interact with distributed file system applications. By using metaprogramming, we bring the traditional benefits of staging, such as partial evaluation to the domain of distributed file system access. Furthermore, this approach also fuses the data access code with the computation code, allowing end-to-end optimization. We test our framework on a real-world use case and show that this approach allows users to generate code that performs faster than traditional data loading by up to 12.56x on a single thread and even more when parallelized.


title: On the Soundness of Auto-completion Services for Dynamically Typed Languages

authors:
Damian Frölich
L. Thomas van Binsbergen

abstract: Giving auto-completion candidates for dynamically typed languages requires complex analysis of the source code, especially when the goal is to ensure that the completion candidates do not introduce bugs. In this paper, we introduce an approach that builds upon abstract interpretation and the scope graph framework to obtain an over-approximation of the name binding seen at run-time. The over-approximation contains enough information to implement auto-completion services such that the given suggestions do not introduce name binding errors. To demonstrate our approach, we compare the suggestions given by our approach with the state of the art completion services on a subset of the Python programming language.


title: Seamless Scope-Safe Metaprogramming through Polymorphic Subtype Inference (Short Paper)

authors:
Cunyuan Gao
Lionel Parreaux

abstract: Practical metaprogramming applications often involve manipulating open code fragments, which is easy to get wrong in the absence of static verification that all variable occurrences remain correctly bound. Many approaches have been proposed to verify the type- and scope-safety of metaprograms, but these approaches are either incomplete or cumbersome, imposing heavy type annotation or proof obligation burdens on metaprogrammers. In this short paper, we propose a new type system to statically keep track of the context requirements of code fragments. Our system uses a novel combination of Boolean-algebraic subtyping and first-class polymorphic type inference techniques to alleviate the annotation burden. The former provides the ability to encode scope requirements as unions of types and the latter allows these types to be locally quantified through a flexible form of polymorphic subtyping. We formalize this type system and demonstrate its implementation in the nascent MLscript functional and object-oriented programming language.


title: Applying a Self-Extension Mechanism to DSLs for Establishing Model Libraries

authors:
Arkadii Gerasimov
Nico Jansen
Judith Michael
Bernhard Rumpe

abstract: When applying model-driven engineering in an agile environment, new requirements continuously expand the domain scope and trigger an extension of the concepts covered by the Domain-Specific Language (DSL). While programming languages streamline code extension and reuse through libraries, similar approaches for DSLs are more complex or target a specific language. We present and discuss an approach for designing DSLs with a self-extension mechanism to enable model library creation and seamless reuse. We use the self-extension mechanism to introduce concepts in models, gather reusable models into a library, and provide an infrastructure for its usage. We explain our language-specific realization of the self-extension mechanism using a DSL and discuss model libraries of the DSL with a use case from practice. The approach provides more flexibility for agile model-driven engineering. It enables application modelers to introduce and reuse concepts via models without changing the DSL, reducing the communication overhead within the development team.


title: An Extensible Feature-Oriented Approach for Fine-Grained Code Quality Analysis

authors:
Karim Ghallab
Tewfik Ziadi
Zaak Chalal

abstract: Assessing code quality is crucial for effective software maintenance and evolution. Traditional tools like SonarQube offer valuable insights at the application level but lack the granularity needed for detailed, feature-specific analysis. This paper emphasizes the importance of feature-oriented code quality analysis, often overlooked by mainstream tools due to the challenge of correlating high-level feature descriptions with low-level code implementations. To tackle this issue, we leverage existing feature location techniques to introduce a novel approach enabling granular analysis tailored to specific application features. We discuss the motivations for this approach, highlighting its potential to improve precision in enhancement and maintenance strategies. Additionally, this paper introduces a tool-based approach known as InsightMapper. We also present a study demonstrating the benefits of this method through the analysis of two case studies, featuring a recognized benchmark in the feature location domain.


title: Hot Call-Chain Inlining for the Glasgow Haskell Compiler

authors:
Celeste Hollenbeck
Michael F. P. O'Boyle

abstract: Inlining is a well-studied compiler transformation that can reduce call overhead and enable further optimizations. As functional programming languages such as Haskell have functions as first-class objects, they potentially have the most to gain from inlining. However, despite being acknowledged as one of the most important optimizations, there has been little recent work to significantly improve Haskell’s inlining heuristic for code performance. This paper proposes a profile-directed technique to direct inlining decisions in the Glasgow Haskell Compiler. We show that simply inlining “hot” functions, as revealed by profiling summaries, does not lead to significant improvement. However, inlining along the hot dynamic call graph is frequently beneficial. Due to the higher-order nature of Haskell, determining this call graph is non-trivial. We develop a technique to extract call chains of hot functions and leverage the Glasgow Haskell Compiler’s existing functionality to safely influence inlining decisions through pragma placement along these chains. We then show that hot call chain inlining yields a geometric mean speedup in run time of 9% over GHC’s default inlining heuristics across 17 real-world Haskell packages. This method can be used in the presence of pre-existing developer pragmas to produce a mean speedup of 10% across those same packages.


title: Type-Safe Code Generation with Algebraic Effects and Handlers

authors:
Kanaru Isoda
Ayato Yokoyama
Yukiyoshi Kameyama

abstract: Staged computation is a means to achieve maintainability and high performance simultaneously, by allowing a programmer to express domain-specific optimizations in a high-level programming language. Multi-stage programming languages such as MetaOCaml provide a static safety guarantee for generated programs by sophisticated type systems provided that program generators have no computational effects. Despite several studies, it remains a challenging problem to design a type-safe multi-stage programming language with advanced features for computational effects. This paper introduces a two-stage programming language with algebraic effects and handlers. Based on two novel principles 'handlers as future-stage binders' and 'handlers are universal', we design a type system and prove its soundness. We also show that our language is sufficiently expressive to write various effectful staged computations including multi-level let-insertion, which is a key technique to avoid code duplication in staged computation.


title: Separate Compilation and Partial Linking: Modules for Datalog IR

authors:
David Klopp
André Pacak
Sebastian Erdweg

abstract:
In recent years, Datalog has sparked renewed interest in academia and industry, leading to the development of numerous new Datalog systems. To unify these systems, recent approaches treat Datalog as an intermediate representation (IR) in a compiler framework: Compiler frontends can lower different Datalog dialects to the same IR, which is then optimized before a compiler backend targets one of many existing Datalog engines. However, a key feature is missing in these compiler frameworks: an expressive module system.

In this paper, we present the first module system for a Datalog IR. Our modules are statically typed, can be separately compiled, and partially linked to form "bundles". Since IR modules are generated by a compiler frontend, we rely on explicit declarations of required and provided relations to maximize the decoupling between modules. This also allows modules to abstract over required relations to offer reusable functionality (e.g., computing a transitive closure) that can be instantiated for different relations in a single Datalog program. We formalize the module system, its type system, and the linking algorithm. We then describe how different usage patterns that occur in Datalog dialects (e.g., inheritance, cyclic imports) can be expressed in our IR module system. Finally, we integrate our module system into an existing Datalog compiler framework, develop a Soufflé compiler frontend that translates Soufflé components to IR modules, and demonstrate its applicability to a large Doop analysis.


title: Restaging Domain-Specific Languages: A Flexible Design Pattern for Rapid Development of Optimizing Compilers

abstract: This paper addresses the complexity of developing optimizing compilers by proposing a novel design pattern named Restage. The Restage interface reduces boilerplate code in transformation passes by simplifying the extraction and reconstruction of language constructs, thereby enabling more efficient and maintainable compiler development. This approach automatically generates the necessary interface instances using metaprogramming, minimizing manual effort. Additionally, the proposed solution integrates seamlessly with existing methodologies for building optimizing compilers, including strategy-based transformations and the visitor design pattern. The Restage design pattern significantly reduces the complexity and maintenance cost of compilers for generic-purpose and domain-specific languages.


title: Imperative Program Synthesis by Abstract Static Analysis and SMT Mutations

abstract:
This paper introduces a novel technique for synthesizing imperative programs that meet behavioral specifications given in the form of assumptions and assertions (logic formulas). In particular, we combine basic statement-directed enumerative search, static analysis via abstract interpretation, and expression-directed enumerative search via (incremental) SMT-based mutations to efficiently explore all candidate complete programs generated from an input program template (with statement and expression holes) until a solution is found. Firstly, the algorithm uses a basic enumerative search through the space of all possible statements, thus filling in all statement holes. In effect, we obtain partial programs with only missing (arithmetic and boolean) expressions, which are subsequently classified by a static analysis either as potential solutions or as definite failures. Finally, we repeatedly mutate the missing expressions in potential solutions and check if the resulting complete programs become bounded correct with respect to the given assertions.

We have implemented our technique in a prototype tool and evaluated it on a set of introductory C programs. The experimental results confirm the effectiveness of our technique for synthesizing various interesting C programs.


title: A Stable Model Semantics for eFLINT Norm Specifications and Model Checking Scenarios

authors:
Christopher A. Esterhuyse
Tim Müller
L. Thomas van Binsbergen

abstract:
Since its introduction at GPCE2020, the eFLINT norm specification language has been used in academic and industrial applications to specify and automate compliance for various norms, such as privacy regulations and data processing agreements. The eFLINT interpreter has been used to automate the analysis of real-time or historical cases by computing logical consequences and reporting normative violations.

To support future language and tooling developments, we contribute a formal definition of the language as a translation to first-order logic programming with stable model semantics. The described semantics aligns with the previous semi-formal descriptions of the language, but resolves issues relating to logical inference with negative antecedent and aggregation operators. Specifically, we formalise the connection between eFLINT's derivation rules and Horn clauses under the stable model semantics. Secondly, by repurposing the Clingo answer-set solver as a highly-optimised eFLINT interpreter, we extend the toolset for eFLINT with model-checking abstract properties in addition to case analysis.

We evaluate the new semantics and interpreter via an empirical comparison of the existing implementation to our prototype implementation. We observe that the expected subset of our tests have the equivalent behaviours.


title: Comparative Analysis of Pre-trained Code Language Models for Automated Program Repair via Code Infill Generation

authors:
Iman Hemati Moghadam
Oebele Lijzenga
Vadim Zaytsev

abstract:
Automated Program Repair (APR) has advanced significantly with the emergence of pre-trained Code Language Models (CLMs), enabling the generation of high-quality patches. However, selecting the most suitable CLM for APR remains challenging due to a range of factors, including accuracy, efficiency, and scalability, among others. These factors are interdependent and interact in complex ways, making the selection of a CLM for APR a multifaceted problem.

This study systematically evaluates 20 pre-trained CLMs, ranging from 60M to 16B parameters, on the HumanEval-Java benchmark (163 buggy Java methods). The evaluation examines bug-fixing accuracy, resource consumption, compilability, patch diversity, and sampling strategies (beam search vs. nucleus sampling).

Results indicate that larger models such as CodeLLaMA-13B and StarCoder generally perform better in bug fixing and compiler error handling, but scale alone does not guarantee effectiveness, as some (e.g., CodeGen2) perform poorly despite their size. Notably, memory usage increases with model size, but time consumption does not exhibit a clear correlation, suggesting that efficiency is influenced by architecture rather than scale alone. Additionally, nucleus sampling slightly outperforms beam search, though the difference is not statistically significant. Since no single CLM fixes all bugs, these findings highlight the potential of hybrid or ensemble-based CLM-driven APR approaches for more robust bug-fixing.


title: CoCoCoLa: Code Completion Control Language

authors:
Nhat
Vadim Zaytsev

abstract:
In software development, the efficiency and accuracy of code completion systems are crucial for productivity and codebase discovery. From simple spell checkers to advanced AI-powered tools, there are more ways to complete your code than ever. This results in an explosion in the number of possible valid proposals, especially when working with today’s increasingly large codebases. Over the years, a lot of effort has been put into developing effective ranking systems to prioritise proposals with more potential. Yet developers still often struggle with an overwhelming number of suggestions, leading to reduced productivity and increased cognitive load.

In this paper, instead of just performing completion by name, we propose CoCoCoLa — an alternative approach to give back the control over the presented proposals to the developer. By investigating the recorded code completion events, frequencies of desirable code elements’ properties were calculated to identify useful control factors. To avoid adding further complexity to the completion process, we propose a simple language, defined within the boundary of a valid identifier of the 50+ most popular software languages in 2024. This language allows developers to specify and filter for desired properties of the proposals.


title: P4DDG: Data-Dependent Grammars for Packet Specification and Parsing in P4

authors:
Tommaso Pacciani
Damian Frölich
L. Thomas van Binsbergen
Chrysa Papagianni

abstract:
In software-defined networking, the domain-specific language P4 allows developers to program the behavior of networking devices at a comparatively high level of abstraction. A P4 program defines a state machine to parse incoming packets. The parsers are flexible and efficient but may be sensitive to bugs and difficult to maintain. As a possible alternative, data-dependent grammars (DDGs) can describe both packet structure and parser at a higher level of abstraction.

In this work, we investigate the use of DDGs in P4 programs. In particular, we demonstrate how DDGs can be used to simultaneously define packets and parsers. We describe a DDG to P4 compiler and evaluate our approach empirically. Input to our evaluation is a collection of P4 programs with for each: the original (handwritten) parser, the (handwritten) DDG alternative, and the compiler-generated parser. The handwritten and generated parsers are compared for equivalence and performance.

Our results show that the generated parsers are three times slower for grammars that do not utilize features distinguishing DDGs from context-free grammars. When parameterized nonterminals are used, a key feature of DDGs, the generated parsers are around six times slower.


title: Integrating Static Optimization and Dynamic Nature in JavaScript

authors:
Tadashi Saito
Hideya Iwasaki

abstract: The class definitions and class field declarations in the ECMAScript standard suggest that the JavaScript engines could be optimized like class-based static languages. This paper focuses on two well-known optimizations. One is method specialization, using fixed offsets to access properties. The other is prior hidden class construction, which involves creating runtime class-like structures called hidden classes before creating instances of the classes. However, implementing such optimizations into JavaScript faces difficulties because of its dynamic features. We point out three difficulties that must be overcome and propose reasonable solutions. We implemented these optimizations and solutions in QuickJS, a small, practical JavaScript engine, and obtained promising results.


title: Retrofitting a Virtual Instrument DSL with Programming Abstractions

authors:
Mathias Vatter
Sebastian Erdweg

abstract: KSP is an imperative DSL in music production that enables realistic modelling of musical instruments in real-time using Kontakt as a runtime environment. Once a niche topic for hobbyists, the field has since professionalized, with Kontakt becoming an industry standard. Its scripting language, however, has not evolved much, lacking modern functional and data abstractions while remaining closed-source. This paper proposes transformations that introduce modularity and basic abstraction principles to KSP. This entails functions with parameters and return values, recursive data types, and the implementation of lexical scope to replace the current global variable management. The transformations have been implemented in a preprocessing compiler framework--preceding the actual KSP interpreter--to an extend, that allows for the new syntax elements to be used in real-world KSP scripts.


title: Staged Gradual Typing

authors:
Hiroto Yaguchi
Yukiyoshi Kameyama

abstract: Staging dynamically typed programming languages safely is a challenge, as the programming-language support for staged computation typically relies on static type systems. To solve this problem, we propose a staged gradual type system that seamlessly integrates static and dynamic typing with staged computation. Our system combines the basic gradual type system and the let-polymorphic staged type system for run-time code generation safely. We discuss the design and issues in developing the calculus, and present a type system and operational semantics via a translation to a cast calculus where dynamic type checking is made explicit. We also show several applications, such as lightweight stage polymorphism.


title: Executable Counterfactuals: A Causal Calculus for Concurrent Systems (Keynote)

abstract: Modern software systems are increasingly concurrent, adaptive, and generative, yet our formal methods still focus primarily on describing what systems do rather than why particular behaviours arise. In this talk, I will present ongoing work on a causal calculus for concurrent systems that combines process algebra, modal logic, and intervention-based causality in the style of Halpern and Pearl.


title: Comparing Solver Representations for Analyzing Cardinality-Based Feature Models

authors:
Fabian Eger
Lukas Güthing
Kevin Feichtinger
Ina Schaefer

abstract: The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot be done with state-of-the-art, SAT-based tooling for analyzing Boolean Feature Models (FMs). Analyses on FMs include checking for satisfying configurations, dead features, false optional features, and whether specific configurations are valid according to the FM. In this work, we compare different solver encodings to enable analysis for CFMs. First, we generalize the analyses on Boolean FMs to the notion of cardinalities and the new anomalies that can occur. Second, we present three different mathematical encodings of CFMs for automated reasoning using solvers. Third, we implement the encoding for ILP, SMT, and CSP solvers. We evaluate the feasibility and performance of our encodings on current ILP, SMT, and CSP solvers. Our evaluation shows that our encoding for CSP solvers enables all common analyses with the best performance among the compared encodings and solvers.


title: Modular Substructural Constraints for Embedded DSLs

authors:
Anna Herlihy
Amir Shaikhha
Anastasia Ailamaki
Martin Odersky

abstract: Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to customize them. We present a technique for expressing modular substructural constraints on function arrows in embedded domain-specific languages, enabling resource disciplines to be customized to the heterogeneous requirements of real-world domains. We formalize the design as an extension of the simply-typed lambda calculus and provide a Scala 3 implementation that uses type-level programming to enforce constraints at compile-time without host-compiler modifications. We illustrate the approach on a Linear Datalog case study, showing no performance overhead on practical programs.


title: TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD

authors:
Jef Jacobs
Wolfgang De Meuter
Jens Nicolay

abstract: In programmatic CAD (PCAD), 3D shapes are generally modelled either by position-based composition of simpler shapes, or by direct generation via path-based techniques (e.g., extrusions, sweeps, revolves). While state-of-the-art PCAD tools effectively support position-based modelling, they lack expressive mechanisms for path-based modelling. As a result, shapes that are naturally formed by sweeping a 2D path into a 3D shape are difficult to model and use in these tools. This paper introduces TurtleTalk, a PCAD language that offers rich support for constructing path-based shapes and the composition of path-based and primitive shapes. TurtleTalk is an extension of PrintTalk, a PCAD language featuring constraints for composing constituent shapes into complex 3D models. TurtleTalk takes inspiration from turtle graphics for constructing paths using imperative instructions and uniquely integrates constraints to enable the declarative expression of path properties. Our evaluation shows that combining imperative instructions and declarative constraints facilitates the design of path-based shapes by reducing the need for complex manual calculations, while also enhancing their composability and reusability.


title: Programmable Record Types in Haskell

authors:
Arthur Jamet
Michael Vollmer

abstract: In Haskell, accessing an object's fields requires deconstructing it. Thankfully, it is possible to name the fields of a data type using the record syntax, allowing programmers to access objects' fields using their name. This can help improve the readability of Haskell code. However, Haskell's support for record types is limited, as its type system is nominal, and the language does not allow composing record types.


title: Metis: A Compositional DSL for Board Games and Game Tree Search

authors:
Thomas Kottenhahn
Prashant Kumar

abstract: We present Metis, a domain-specific language embedded in Haskell for two-player board games on rectangular boards that exploits their shared structure (setup, rules, win condition) through three composable mini-DSLs. Atomic operations for placing, moving, and capturing pieces combine with filters, union, and sequencing to form rulesets; win conditions and evaluation functions reuse the same compositional pattern. With just 13 rule expressions Metis can express 80% of games from a catalog of 168 abstract games. The structure also supports game-playing agents through composable search and evaluation components.


title: Stageleft: Multi-stage Programming in Standard Rust

authors:
Shadaj Laddad
Mingwei Samuel
Joseph M. Hellerstein

abstract: Rust has emerged as a popular systems language with growing interest in metaprogramming, yet it lacks staging support—developers must write unsafe, untyped macros instead. We present Stageleft, a library that brings type-safe staged programming to standard Rust without compiler modifications. Stageleft ensures hygienic code generation through ahead-of-time AST analysis, and handles free variables via a trait system that respects Rust's ownership rules. Stageleft demonstrates that staging can be practical and safe in Rust, enabling domain-specific optimizations while maintaining familiar developer interfaces.


title: Synthesizing Recursive Functional Programs via Structure-Element Separation

authors:
Junyu Lin
Akimasa Morihata

abstract: Synthesizing recursive functional programs over algebraic data types from input-output examples remains challenging, largely due to the explosion of structurally distinct candidates during search. We present a synthesis approach for structurally recursive list/tree transformations based on a structure-element separation viewpoint: a structure transformation that determines output shape, and element computations that determine the values placed into that shape. Our method first infers structural relationships from examples that describe per-step output-size evolution along recursive calls and uses them to prune partial programs during top-down enumeration. For candidates that are structurally feasible, we apply a diamond function that converts the remaining element-level holes into small local program-by-example subproblems, which are then solved using symbolic execution and output alignment, enabling early acceptance or rejection without expanding unrelated global constructs. We implement the approach in an OCaml prototype synthesizer and evaluate it on a suite of list and tree benchmarks drawn from prior work. The results show that our method substantially reduces expensive example checking and improves synthesis performance on recursive list/tree transformation programs.


title: Less Is More: Measuring How LLM Involvement Affects Chatbot Accuracy in Static Analysis

abstract: Large language models are increasingly used to make static analysis tools accessible through natural language, yet existing systems differ in how much they delegate to the LLM without treating the degree of delegation as an independent variable. We compare three architectures along a spectrum of LLM involvement for translating natural language to Joern’s Code Property Graph Query Language (): direct query generation (1), generation of a schema-constrained JSON intermediate representation (2), and tool-augmented agentic generation (3). These are evaluated on a benchmark of 20 code analysis tasks across three complexity tiers, using four open-weight models in a 2×2 design (two model families × two scales), each with three repetitions. The structured intermediate representation (2) achieves the highest result match rates across all four models, outperforming direct generation by 15–25 percentage points on large models. The agentic approach (3) ranks last on every model despite substantially higher token cost. The benefit of structured intermediates is most pronounced for large models; for small models, schema compliance becomes the bottleneck. These findings suggest that in formally structured domains, constraining the LLM’s output to a well-typed intermediate representation and delegating query construction to deterministic code yields better results than either unconstrained generation or iterative tool use.


title: ATLAS: From Access conTrol Language to ACSL Specifications

authors:
Julien Signoles
Khaoula Boukir
Amine Nasri

abstract: Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This paper presents ATLAS, a new formal specification language for expressing access control policies. This language allows for modeling an access control policy, linking it to a source code, and generating automatically formal annotations in order to verify that a source code correctly implements the modeled policy. This workflow is implemented as a new Frama-C plugin that generates ACSL annotations, which can be proved by deductive verification or checked at runtime.


title: Bringing Mixed-Stage Programming to OCaml (Keynote)

abstract: Over the last three decades, multi-stage programming has been used to write high-level, type-safe, optimising code generators for a wide variety of domains, from database queries and stream processing to geometry, parsing, and differentiable programming.


venue: haskell

title: A lightweight implementation of generics and dynamics

authors:
James Cheney
Ralf Hinze

abstract: The recent years have seen a number of proposals for extending statically typed languages by dynamics or generics. Most proposals --- if not all --- require significant extensions to the underlying language. In this paper we show that this need not be the case. We propose a particularly lightweight extension that supports both dynamics and generics. Furthermore, the two features are smoothly integrated: dynamic values, for instance, can be passed to generic functions. Our proposal makes do with a standard Hindley-Milner type system augmented by existential types. Building upon these ideas we have implemented a small library that is readily usable both with Hugs and with the Glasgow Haskell compiler.


title: Testing monadic code with QuickCheck

authors:
Koen Claessen
John Hughes

abstract: QuickCheck is a previously published random testing tool for Haskell programs. In this paper we show how to use it for testing monadic code, and in particular imperative code written using the ST monad. QuickCheck tests a program against a specification: we show that QuickCheck's specification language is sufficiently powerful to represent common forms of specifications: algebraic, model-based (both functional and relational), and pre-/post-conditional. Moreover, all these forms of specification can be used directly for testing. We define a new language of monadic properties, and make a link between program testing and the notion of observational equivalence.


title: A formal specification of the Haskell 98 module system

authors:
Iavor S. Diatchki
Mark P. Jones
Thomas Hallgren

abstract: Many programming languages provide means to split large programs into smaller modules. The module system of a language specifies what constitutes a module and how modules interact.This paper presents a formal specification of the module system for the functional programming language Haskell. Although many aspects of Haskell have been subjected to formal analysis, the module system has, to date, been described only informally as part of the Haskell language report. As a result, some aspects of it are not well understood or are under-specified; this causes difficulties in reasoning about Haskell programs, and leads to practical problems such as inconsistencies between different implementations. One significant aspect of our work is that the specification is written in Haskell, which means that it can also be used as an executable test-bed, and as a starting point for Haskell implementers.


title: A recursive do for Haskell

authors:
Levent Erkök
John Launchbury

abstract: Certain programs making use of monads need to perform recursion over the values of monadic actions. Although the do-notation of Haskell provides a convenient framework for monadic programming, it lacks the generality to support such recursive bindings. In this paper, we describe an enhanced translation schema for the donotation and its integration into Haskell. The new translation allows variables to be bound recursively, provided the underlying monad comes equipped with an appropriate fixed-point operator.


title: Eager Haskell: resource-bounded execution yields efficient iteration

abstract: The advantages of the Haskell programming language are rooted in its clean equational semantics. Those advantages evaporate as soon as programmers try to write simple iterative computations and discover that their code must be annotated with calls to seq in order to overcome space leaks introduced by lazy evaluation. The Eager Haskell compiler executes Haskell programs eagerly by default, i.e., bindings and function arguments are evaluated before bodies. When resource bounds are exceeded, computation falls back and is restarted lazily. By using a hybrid of eager and lazy evaluation, we preserve the semantics of Haskell and yet permit efficient iteration.


title: Haddock, a Haskell documentation tool

abstract: This paper describes Haddock, a tool for automatically generating documentation from Haskell source code. Haddock's unique approach to source code annotations provides a useful separation between the implementation of a library and the interface (and hence also the documentation) of that library, so that as far as possible the documentation annotations in the source code do not affect the programmer's freedom over the structure of the implementation. The internal structure and implementation of Haddock is also discussed.


title: Functional reactive programming, continued

authors:
Henrik Nilsson
Antony Courtney
John Peterson

abstract: Functional Reactive Programming (FRP) extends a host programming language with a notion of time flow. Arrowized FRP (AFRP) is a version of FRP embedded in Haskell based on the arrow combinators. AFRP is a powerful synchronous dataflow programming language with hybrid modeling capabilities, combining advanced synchronous dataflow features with the higher-order lazy functional abstractions of Haskell. In this paper, we describe the AFRP programming style and our Haskell-based implementation. Of particular interest are the AFRP combinators that support dynamic collections and continuation-based switching. We show how these combinators can be used to express systems with an evolving structure that are difficult to model in more traditional dataflow languages.


title: Techniques for embedding postfix languages in Haskell

abstract: One popular use for Haskell in recent years has been as a host language for domain-specific embedded languages. But how can one embed a postfix language in Haskell, given that Haskell only supports prefix and infix syntax? This paper describes several such embeddings for increasingly complex postfix languages.


title: Template meta-programming for Haskell

authors:
Tim Sheard
Simon Peyton Jones

abstract: We propose a new extension to the purely functional programming language Haskell that supports compile-time meta-programming. The purpose of the system is to support the algorithmic construction of programs at compile-time. The ability to generate code at compile time allows the programmer to implement such features as polytypic programs, macro-like expansion, user directed optimization (such as inlining), and the generation of supporting data structures and functions from existing data structures and functions. Our design is being implemented in the Glasgow Haskell Compiler, ghc. 1


title: Functional Pearl trouble shared is trouble halved

authors:
Richard S. Bird
Ralf Hinze

abstract: than one incoming arc. Shared nodes are created in almost every functional program---for instance, when updating a purely functional data structure---though programmers are seldom aware of this. In fact, there are only a few algorithms that exploit sharing of nodes consciously. One example is constructing a tree in sublinear time. In this pearl we discuss an intriguing application of nexuses; we show that they serve admirably as memo structures featuring constant time access to memoized function calls. Along the way we encounter Boolean lattices and binomial trees.


title: The Yampa arcade

authors:
Antony Courtney
Henrik Nilsson
John Peterson

abstract: Simulated worlds are a common (and highly lucrative) application domain that stretches from detailed simulation of physical systems to elaborate video game fantasies. We believe that Functional Reactive Programming (FRP) provides just the right level of functionality to develop simulated worlds in a concise, clear and modular way. We demonstrate the use of FRP in this domain by presenting an implementation of the classic Space Invaders game in Yampa, our most recent Haskell-embedded incarnation of FRP.


authors:
Robert Ennals
Simon L. Peyton Jones

abstract: Article Share on HsDebug: debugging lazy programs by not being lazy Authors: Robert Ennals University of Cambridge University of CambridgeView Profile , Simon Peyton Jones Microsoft Research Ltd, Cambridge Microsoft Research Ltd, CambridgeView Profile Authors Info & Claims Haskell '03: Proceedings of the 2003 ACM SIGPLAN workshop on HaskellAugust 2003Pages 84–87https://doi.org/10.1145/871895.871904Published:28 August 2003Publication History 7citation345DownloadsMetricsTotal Citations7Total Downloads345Last 12 Months7Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Haskell and principal types

abstract: This paper points out two problems which prevent Haskell from having principal types. For each problem, we discuss a program which exhibits it. The first problem has to do with type signatures and class constraints containing both generic and nongeneric type variables. The second problem is caused by the monomorphism restriction. In both cases there is an interaction between generalization and class constraints where substituting a nonvariable type for a constrained type variable makes the constraint tautological and opens up for more aggressive generalization.We also discuss how these problems can be solved by introducing quantified class constraints and strengthening the monomorphism restriction from prohibiting only the generalization of constrained type variables to prohibiting any generalization at all. We also give an inference algorithm producing principal types for the new system.


abstract: Article Share on Haskell tools from the programatica project Author: Thomas Hallgren Oregon Health & Science University, Beaverton, OR Oregon Health & Science University, Beaverton, ORView Profile Authors Info & Claims Haskell '03: Proceedings of the 2003 ACM SIGPLAN workshop on HaskellAugust 2003Pages 103–106https://doi.org/10.1145/871895.871907Published:28 August 2003Publication History 13citation362DownloadsMetricsTotal Citations13Total Downloads362Last 12 Months4Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Helium, for learning Haskell

authors:
Bastiaan Heeren
Daan Leijen
Arjan van IJzendoorn

abstract: Helium is a user-friendly compiler designed especially for learning the functional programming language Haskell. The quality of the error messages has been the main concern both in the choice of the language features and in the implementation of the compiler. Helium implements almost full Haskell, where the most notable difference is the absence of type classes. Our goal is to let students learn functional programming more quickly and with more fun. The compiler has been successfully employed in two introductory programming courses at Utrecht University.


title: Structure and interpretation of quantum mechanics: a functional framework

abstract: We present a framework for representing quantum entities in Haskell. States and operators are functional objects, and their semantics is defined --- as far as possible --- independently of the base in the Hilbert space. We construct effectively the tensor states for composed systems, and we present a toy model of quantum circuit toolbox. We conclude that functional languages are right tools for formal computations in quantum physics. The paper focuses mainly on the representation, not on computational problems.


title: Tool support for refactoring functional programs

authors:
Huiqing Li
Claus Reinke
Simon J. Thompson


title: Modeling quantum computing in Haskell

abstract: The paper develops a model of quantum computing from the perspective of functional programming. The model explains the fundamental ideas of quantum computing at a level of abstraction that is familiar to functional programmers. The model also illustrates some of the inherent difficulties in interpreting quantum mechanics and highlights the differences between quantum computing and traditional (functional or otherwise) computing models.


title: Interactive type debugging in Haskell

authors:
Peter J. Stuckey
Martin Sulzmann
Jeremy Wazny

abstract: Proceedings of the 2003 ACM SIGPLAN Haskell Workshop


title: XML templates and caching in WASH

abstract: Caching of documents is an important concern on the Web. It is a major win in all situations where bandwidth is limited. Unfortunately, the increasing spread of dynamically generated documents seriously hampers traditional caching techniques in browsers and on proxy servers.WASH/CGI is a Haskell-based domain specific language for creating interactive Web applications. The Web pages generated by a WASH/CGI application are highly dynamic and cannot be cached with traditional means.We show how to implement the dynamic caching scheme of the BigWig language [2] in the context of WASH/CGI. The main issue in BigWig's caching scheme is the distinction between fixed parts (that should be cached) and variable parts (that need not be cached) of a document. Since BigWig is a standalone domain-specific language, its compiler can perform the distinction as part of its static analysis. Hence, the challenge in our implementation is to obtain the same information without involving the compiler. To this end, we extend WASH/CGI's document language by mode annotations and define the translation of the resulting annotated document language into JavaScript.To alleviate the awkwardness of programming directly in annotated language, we have defined a surface syntax in the style of HSP (Haskell Server Pages) [11].


title: Simulating quantified class constraints

abstract: Defining nontrivial class instances for irregular and exponential datatypes in Haskell is challenging, and as a solution it has been proposed to extend the language with quantified class constraints of the form ∀a. C a ⇒ C' (f a) in the contexts of instance declarations. We show how to express the equivalent of such constraints in vanilla Haskell 98, but their utility in this language is limited. We also present a more flexible solution, which relies on a widely-supported language extension.


title: Type-safe, self inspecting code

authors:
Arthur I. Baars
S. Doaitse Swierstra

abstract: We present techniques for representing typed abstract syntax trees in the presence of observable recursive structures. The need for this arose from the desire to cope with left-recursion in combinator based parsers. The techniques employed can be used in a much wider setting however, since it enables the inspection and transformation of any program structure, which contains internal references. The hard part of the work is to perform such analyses and transformations in a setting in which the Haskell type checker is still able to statically check the correctness of the program representations, and hence the type correctness of the transformed program.


title: Student paper: HaskellDB improved

authors:
Björn Bringert
Anders Höckersten
Conny Andersson
Martin Andersson
Mary Bergman
Victor Blomqvist
Torbjörn Martin

abstract: We present an improved version of the HaskellDB database library. The original version relied on TRex, a Haskell extension supported only by the Hugs interpreter. We have replaced the use of TRex by a record implementation which uses more commonly implemented Haskell extensions.Additionally, HaskellDB now supports two different cross-platform database backends. Other changes include database creation functionality, bounded string support, performance enhancements, fixes to the optimisation logic, transaction support and more fine grained expression types.


title: Programming graphics processors functionally

abstract: Graphics cards for personal computers have recently undergone a radical transformation from fixed-function graphics pipelines to multi-processor, programmable architectures. Multi-processor architectures are clearly advantageous for graphics for the simple reason that graphics computations are naturally concurrent, mapping well to stateless stream processing. They therefore parallelize easily and need no random access to memory with its problematic latencies.This paper presents Vertigo, a purely functional, Haskell-embedded language for 3D graphics and an optimizing compiler that generates graphics processor code. The language integrates procedural surface modeling, shading, and texture generation, and the compiler exploits the unusual processor architecture. The shading sub-language is based on a simple and precise semantic model, in contrast to previous shading languages. Geometry and textures are also defined via a very simple denotational semantics. The formal semantics yields not only programs that are easy to understand and reason about, but also very efficient implementation, thanks to a compiler based on partial evaluation and symbolic optimization, much in the style of Pan [2].Haskell's overloading facility is extremely useful throughout Vertigo. For instance, math operators are used not just for floating point numbers, but also expressions (for differentiation and compilation), tuples, and functions. Typically, these overloadings cascade, as in the case of surfaces, which may be combined via math operators, though they are really functions over tuples of expressions on floating point numbers. Shaders may be composed with the same notational convenience. Functional dependencies are exploited for vector spaces, cross products, and derivatives.


title: BNF converter

authors:
Markus Forsberg
Aarne Ranta

abstract: We will demonstrate BNFC (the BNF Converter) [7, 6], a multi-lingual compiler tool. BNFC takes as its input a grammar written in LBNF (Labelled BNF) notation, and generates a compiler front-end (an abstract syntax, a lexer, and a parser). Furthermore, it generates a case skeleton usable as the starting point of back-end construction, a pretty printer, a test bench, and a LaTeX document usable as language specification. The program components can be generated in Haskell, Java, C and C++ and their standard parser and lexer tools. BNFC itself was written in Haskell.The methodology used for the generated front-end is based on Appel's books on compiler construction [3, 1, 2]. BNFC has been used as a teaching tool in compiler construction courses at Chalmers. It has also been applied to research-related programming language development, and in an industrial application producing a compiler for a telecommunications protocol description language [4].BNFC is freely available under the GPL license at its website and in the testing distribution of Debian Linux.


title: Strongly typed heterogeneous collections

authors:
Oleg Kiselyov
Ralf Lämmel
Keean Schupke

abstract: A heterogeneous collection is a datatype that is capable of storing data of different types, while providing operations for look-up, update, iteration, and others. There are various kinds of heterogeneous collections, differing in representation, invariants, and access operations. We describe HLIST - a Haskell library for strongly typed heterogeneous collections including extensible records. We illustrate HLIST's benefits in the context of type-safe database access in Haskell. The HLIST library relies on common extensions of Haskell 98. Our exploration raises interesting issues regarding Haskell's type system, in particular, avoidance of overlapping instances, and reification of type equality and type unification.


title: Functional pearl: implicit configurations-or, type classes reflect the values of types

authors:
Oleg Kiselyov
Chung-chieh Shan

abstract: The configurations problem is to propagate run-time preferences throughout a program, allowing multiple concurrent configuration sets to coexist safely under statically guaranteed separation. This problem is common in all software systems, but particularly acute in Haskell, where currently the most popular solution relies on unsafe operations and compiler pragmas.We solve the configurations problem in Haskell using only stable and widely implemented language features like the type-class system. In our approach, a term expression can refer to run-time configuration parameters as if they were compile-time constants in global scope. Besides supporting such intuitive term notation and statically guaranteeing separation, our solution also helps improve the program's performance by transparently dispatching to specialized code at run-time. We can propagate any type of configuration data-numbers, strings, IO actions, polymorphic functions, closures, and abstract data types. No previous approach to propagating configurations implicitly in any language provides the same static separation guarantees.The enabling technique behind our solution is to propagate values via types, with the help of polymorphic recursion and higher-rank polymorphism. The technique essentially emulates local type-class instance declarations while preserving coherence. Configuration parameters are propagated throughout the code implicitly as part of type inference rather than explicitly by the programmer. Our technique can be regarded as a portable, coherent, and intuitive alternative to implicit parameters. It motivates adding local instances to Haskell, with a restriction that salvages principal types.


title: wxHaskell: a portable and concise GUI library for haskell

abstract: wxHaskell is a graphical user interface (GUI) library for Haskell that is built on wxWidgets: a free industrial strength GUI library for C++ that has been ported to all major platforms, including Windows, Gtk, and MacOS X. In contrast with many other libraries, wxWidgets retains the native look-and-feel of each particular platform. We show how distinctive features of Haskell, like parametric polymorphism, higher-order functions, and first-class computations, can be used to present a concise and elegant monadic interface for portable GUI programs.


title: Extending the Haskell foreign function interface with concurrency

authors:
Simon Marlow
Simon L. Peyton Jones
Wolfgang Thaller

abstract: A Haskell system that includes both the Foreign Function Interface and the Concurrent Haskell extension must consider how Concurrent Haskell threads map to external Operating System threads for the purposes of specifying in which thread a foreign call is made.Many concurrent languages take the easy route and specify a one-to-one correspondence between the language's own threads and external OS threads. However, OS threads tend to be expensive, so this choice can limit the performance and scalability of the concurrent language.The main contribution of this paper is a language design that provides a neat solution to this problem, allowing the implementor of the language enough flexibility to provide cheap lightweight threads, while still providing the programmer with control over the mapping between internal threads and external threads where necessary.


title: Functional pearl: i am not a number-i am a free variable

authors:
Conor McBride
James McKinna

abstract: In this paper, we show how to manipulate syntax with binding using a mixed representation of names for free variables (with respect to the task in hand) and de Bruijn indices [5] for bound variables. By doing so, we retain the advantages of both representations: naming supports easy, arithmetic-free manipulation of terms; de Bruijn indices eliminate the need for α-conversion. Further, we have ensured that not only the user but also the implementation need never deal with de Bruijn indices, except within key basic operations.Moreover, we give a hierarchical representation for names which naturally reflects the structure of the operations we implement. Name choice is safe and straightforward. Our technology combines easily with an approach to syntax manipulation inspired by Huet's 'zippers'[10].Without the ideas in this paper, we would have struggled to implement EPIGRAM [19]. Our example-constructing inductive elimination operators for datatype families-is but one of many where it proves invaluable.


title: Haskell type browser

authors:
Matthias Neubauer
Peter Thiemann

abstract: No abstract available.


title: Plugging Haskell in

authors:
André T. H. Pang
Don Stewart
Sean Seefried
Manuel M. T. Chakravarty

abstract: Extension languages enable users to expand the functionality of an application without touching its source code. Commonly, these languages are dynamically typed languages, such as Lisp, Python, or domain-specific languages, which support runtime plugins via dynamic loading of components. We show that Haskell can be comfortably used as a statically typed extension language for both Haskell and foreign-language applications supported by the Haskell FFI, and that it can perform type-safe dynamic loading of plugins using dynamic types. Moreover, we discuss how plugin support is especially useful to applications where Haskell is used as an embedded domain-specific language (EDSL). We explain how to realise type-safe plugins using dynamic types, runtime compilation, and dynamic linking, exploiting infrastructure provided by the Glasgow Haskell Compiler. We demonstrate the practicability of our approach with several applications that serve as running examples.


title: Improving type error diagnosis

abstract: All in-text\treferences\tunderlined\tin\tblue\tare\tlinked\tto\tpublications\ton\tResearchGate, letting you\taccess\tand\tread\tthem\timmediately.


title: Verifying haskell programs using constructive type theory

authors:
Andreas Abel
Marcin Benke
Ana Bove
John Hughes
Ulf Norell

abstract: Proof assistants based on dependent type theory are closely related to functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In this paper, we show how Agda, such a proof assistant, can be used to prove theorems about Haskell programs. Haskell programs are translated into an Agda model of their semantics, by translating via GHC's Core language into a monadic form specially adapted to represent Haskell's polymorphism in Agda's predicative type system. The translation can support reasoning about either total values only, or total and partial values, by instantiating the monad appropriately. We claim that, although these Agda models are generated by a relatively complex translation process, proofs about them are simple and natural, and we offer a number of examples to support this claim.


title: There and back again: arrows for invertible programming

authors:
Artem Alimarine
Sjaak Smetsers
Arjen van Weelden
Marko C. J. D. van Eekelen
Rinus Plasmeijer

abstract: Invertible programming occurs in the area of data conversion where it is required that the conversion in one direction is the inverse of the other. For that purpose, we introduce bidirectional arrows (bi-arrows). The bi-arrow class is an extension of Haskell's arrow class with an extra combinator that changes the direction of computation.The advantage of the use of bi-arrows for invertible programming is the preservation of invertibility properties using the bi-arrow combinators. Programming with bi-arrows in a polytypic or generic way exploits this the most. Besides bidirectional polytypic examples, including invertible serialization, we give the definition of a monadic bi-arrow transformer, which we use to construct a bidirectional parser/pretty printer.


title: Visual haskell: a full-featured haskell development environment

authors:
Krasimir Angelov
Simon Marlow

abstract: We describe the design and implementation of a full-featured Haskell development environment, based on Microsoft's extensible Visual Studio environment.Visual Haskell provides a number of features not found in existing Haskell development environments: interactive error-checking, displaying of inferred types in the editor, and other features based on static properties of the source code. Visual Haskell also provides full support for developing and building multi-module Haskell projects, based on the Cabal architecture. Visual Haskell supports the full GHC language, and can be used to develop real Haskell applications (including the code of the plugin itself).Visual Haskell has driven developments in other Haskell-related projects: Cabal, the Concurrent FFI extension, and an API to allow programmatic access to GHC itself. Furthermore, development of the Visual Haskell plugin required industrial-strength foreign language interoperability; we describe all our experiences in detail.


title: Polymorphic string matching

abstract: Calculational developments of functional programs have been likened to conjuring tricks: enjoyable to watch but often a mystery as to how they are done. This pearl explains the trick. The aim is to give new calculations of two famous algorithms in string matching, the Knuth-Morris-Pratt algorithm and the Boyer-Moore algorithm. The string matching problem is formulated polymorphically, so the only available property of elements of the alphabet is an equality test.


title: Haskell server pages through dynamic loading

abstract: Haskell Server Pages (HSP) is a domain specific language, based on Haskell, for writing dynamic web pages. Its main features are concrete XML expressions as first class values, pattern-matching on XML, and a runtime system for evaluating dynamic web pages.The first design of HSP was made by Erik Meijer and Danny van Velzen in 2000, but it was never fully designed nor implemented. In this paper we refine, extend and improve their design of the language and describe how to implement HSP using dynamic loading of pages.


title: Haskell on a shared-memory multiprocessor

authors:
Tim Harris
Simon Marlow
Simon L. Peyton Jones

abstract: Multi-core processors are coming, and we need ways to program them. The combination of purely-functional programming and explicit, monadic threads, communicating using transactional memory, looks like a particularly promising way to do so. This paper describes a full-scale implementation of shared-memory parallel Haskell, based on the Glasgow Haskell Compiler. Our main technical contribution is a lock-free mechanism for evaluating shared thunks that eliminates the major performance bottleneck in parallel evaluation of a lazy language. Our results are preliminary but promising: we can demonstrate wall-clock speedups of a serious application (GHC itself), even with only two processors, compared to the same application compiled for a uni-processor.


title: Halfs: a haskell filesystem

abstract: In the course of developing a web server for an embedded operating system, we had need of a filesystem which was small enough to alter to our needs and written in a high-level language so that we could show certain high assurance properties about its behavior. Since we had already ported the Haskell runtime to this operating system, Haskell was the obvious language of choice.This presentation will give a brief overview of the design principals of Halfs, present the Halfs library interface and its integration with the Linux FUSE module, and show basic tasks such as reading and writing to the filesystem.


title: TypeCase: a design pattern for type-indexed functions

authors:
Bruno C. d. S. Oliveira
Jeremy Gibbons

abstract: A type-indexed function is a function that is defined for each member of some family of types. Haskell's type class mechanism provides collections of open type-indexed functions, in which the indexing family can be extended by defining a new type class instance but the collection of functions is fixed. The purpose of this paper is to present TypeCase: a design pattern that allows the definition of closed type-indexed functions, in which the index family is fixed but the collection of functions is extensible. It is inspired by Cheney and Hinze's work on lightweight approaches to generic programming. We generalise their techniques as a design pattern. Furthermore, we show that type-indexed functions with type-indexed types, and consequently generic functions with generic types, can also be encoded in a lightweight manner, thereby overcoming one of the main limitations of the lightweight approaches.


title: Darcs: distributed version management in haskell

abstract: A common reaction from people who hear about darcs, the source control system I created, is that it sounds like a great tool, but it is a shame that it is written in Haskell. People think that because darcs is written in Haskell it will be a slow memory hog with very few contributors to the project. I will give a somewhat historical overview of my experiences with the Haskell language, libraries and tools.I will begin with a brief overview of the darcs advanced revision control system, how it works and how it differs from other version control systems. Then I will go through various problems and successes I have had in using the Haskell language and libraries in darcs, roughly in the order I encountered them. In the process I will give a bit of a tour through the darcs source code. In each case, I will tell about the problem I wanted to solve, what I tried, how it worked, and how it might have worked better (if that is possible).


title: Haskell ready to dazzle the real world

authors:
Martijn M. Schrage
Arjan van IJzendoorn
Linda C. van der Gaag

abstract: Haskell has proved itself to be a suitable implementation language for large software projects. Nevertheless, surprisingly few graphical end-user applications have been written in Haskell. Based on our experience with the development of the Bayesian network toolbox Dazzle, we argue that the language is indeed very well suited for writing such applications. Popular language features, such as higher-order functions, laziness, and light syntax for data structures, turn out to hold their ground in a large interactive end-user application. Haskell, combined with the truly platform-independent GUI library wxHaskell, is ready for building real-world applications.


title: Putting curry-howard to work

abstract: Abstract The Curry-Howard isomorphism states that types are propositionsand that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately,the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this prob-lem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized AlgebraicDatatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new fea-tures are backward compatible with existing features, and combine to enable a new programming paradigm for functional program-mers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this inmanner that leaves intact the functional programming style, known and loved by functional programmers everywhere. Categories and Subject Descriptors D.3 [Software]: Program-ming Languages


title: Dynamic applications from the ground up

authors:
Don Stewart
Manuel M. T. Chakravarty

abstract: Some Lisp programs such as Emacs, but also the Linux kernel (when fully modularised) are mostly dynamic; i.e., apart from a small static core, the significant functionality is dynamically loaded. In this paper, we explore fully dynamic applications in Haskell where the static core is minimal and code is hot swappable. We demonstrate the feasibility of this architecture by two applications: Yi, an extensible editor, and Lambdabot, a plugin-based IRC robot. Benefits of the approach include hot swappable code and sophisticated application configuration and extension via embedded DSLs. We illustrate both benefits in detail at the example of a novel embedded DSL for editor interfaces.


title: Running the manual: an approach to high-assurance microkernel development

authors:
Philip Derrin
Kevin Elphinstone
Gerwin Klein
David A. Cock
Manuel M. T. Chakravarty

abstract: We propose a development methodology for designing and prototyping high assurance microkernels, and describe our application of it. The methodology is based on rapid prototyping and iterative refinement of the microkernel in a functional programming language. The prototype provides a precise semi-formal model, which is also combined with a machine simulator to form a reference implementation capable of executing real user-level software, to obtain accurate feedback on the suitability of the kernel API during development phases. We extract from the prototype a machine-checkable formal specification in higher-order logic, which may be used to verify properties of the design, and also results in corrections to the design without the need for full verification. We found the approach leads to productive, highly iterative development where formal modelling, semi-formal design and prototyping, and end use all contribute to a more mature final design in a shorter period of time.


title: Strongly typed memory areas programming systems-level data structures in a functional language

authors:
Iavor S. Diatchki
Mark P. Jones

abstract: Modern functional languages offer several attractive features to support development of reliable and secure software. However, in our efforts to use Haskell for systems programming tasks-including device driver and operating system construction-we have also encountered some significant gaps in functionality. As a result, we have been forced, either to code some non-trivial components in more traditional but unsafe languages like C or assembler, or else to adopt aspects of the foreign function interface that compromise on strong typing and type safety.In this paper, we describe how we have filled one of these gaps by extending a Haskell-like language with facilities for working directly with low-level, memory-based data structures. Using this extension, we are able to program a wide range of examples, including hardware interfaces, kernel data structures, and operating system APIs. Our design allows us to address concerns about representation, alignment, and placement (in virtual or physical address spaces) that are critical in some systems applications, but clearly beyond the scope of most existing functional languages.Our approach leverages type system features that are wellknown and widely supported in existing Haskell implementations, including kinds, multiple parameter type classes, functional dependencies, and improvement. One interesting feature is the use of a syntactic abbreviation that makes it easy to define and work with functions at the type level.


title: Statically typed linear algebra in Haskell

abstract: Numerical computations are often specified in terms of operations on vectors and matrices. This is partly because it is often natural to do so; but it is also partly because, being otherwise useful, such operations have been provided very fast implementations in linear algebra libraries such as ATLAS (implementing BLAS), LAPACK, fftw, etc. Due to their better cache awareness and use of specialized processor instructions, a high-level invocation of an operation such as matrix multiplication using these libraries may execute orders of magnitude more quickly than a straightforward low-level implementation written in, say, C. The combination of efficiency and expressivity has made the framework of linear algebra an exceedingly popular one for scientists. For example, Matlab[1], an interpreter of a simple linear algebra language, has become a standard research tool in many fields.The process of expressing an algorithm in terms of matrices can be error-prone. Matlab and other popular matrix languages are dynamically-typed, which means that type errors are only detected at run-time. Even statically typed languages rarely keep track of more information in an object type than its tensor rank (e.g., to discriminate between matrices and vectors) and element type.If we could additionally expose object dimensions to the type system then we would ideally be able to detect a much wider variety of common errors at compile time than is currently possible. This would in turn make it easier to build and maintain larger numericsintensive software projects.We call our idea of exposing dimensions to the type system "strongly typed linear algebra". We have written a prototype implementation in Haskell, which is based on Alberto Ruiz's GSLHaskell[2] and which uses techniques from Kiselyov and Shan's "Implicit Configurations" paper[3].The presentation will cover the key aspects of our design such as the use of GADTs to combine matrix and vector types, and the use of higher-rank types and staging (namely, Template Haskell) to closely approximate a dependent-type system. Then, we will give a demonstration of interactive use, and compare our system to existing systems in the areas of speed and usability.


title: Introducing the Haskell equational reasoning assistant

abstract: We introduce the new, improved version of the Haskell Equational Reasoning Assistant, which consists of an Ajax application for rewriting Haskell fragments in their context, and an API for scripting non-trivial rewrites.


title: Interactive debugging with GHCi

abstract: With my presentation I intend to demonstrate an implementation of breakpoint combinators in GHCi. These combinators are designed to aid the debugging process of Haskell programs by halting the execution and letting the user observe variables of their choice. In contrast to the existing tools (such as Hat, Hood, Buddha and Debug. Trace), which in effect allow something similar, the combinators I will be demonstrating give the user the ability to observe the properties, not just the stringification, of variables. The combinators are a more low-level approach to the problem of debugging and do not provide as advanced features as Hat or Buddha. However, no sophisticated debugging system for Haskell has been really widely adopted by the Haskell community, primarily because they lack support for a variety of commonly used Glasgow Haskell extensions. The breakpoint combinators, on the other hand, are integrated in GHCi and work out-of-the-box with all Glasgow Haskell programs.


title: Haskell' status report

abstract: The Haskell programming language is more-or-less divided into two "branches". The Haskell 98 standard is the "stable" branch of the language, and that has been a big success. A lot of progress has been made over the last few years in the "research" branch of the Haskell language. It is constantly advancing, and we feel that it is time for a new standard which reflects those advancements. This talk is a status report from the Haskell' committee to the Haskell community.


title: Polymorphic variants in Haskell

abstract: In languages that support polymorphic variants, a single variant value can be passed to many contexts that accept different sets of constructors. Polymorphic variants can be used in order to introduce extensible algebraic datatypes into functional programming languages and are potentially useful for application domains such as interpreters, graphical user interface (GUI) libraries and database interfaces, where the number of necessary constructors cannot be determined in advance. Very few functional languages, however, have a mechanism to extend existing datatypes by adding new constructors. In general, for polymorphic variants to be useful, we would need some mechanisms to reuse existing functions and extend them for new constructors.Actually, the type system of Haskell, when extended with parametric type classes (or multi-parameter type classes with functional dependencies), has enough power not only to mimic polymorphic variants but also to extend existing functions for new constructors.This paper, first, explains how to do this in Haskell's type system (Haskell 98 with popular extensions). However, this encoding of polymorphic variants is difficult to use in practice. This is because it is quite tedious for programmers to write mimic codes by hand and because the problem of ambiguous overloading resolution would embarrass programmers. Therefore, the paper proposes an extension of Haskell's type classes that supports polymorphic variants directly. It has a novel form of instance declarations where records and variants are handled symmetrically.This type system can produce vanilla Haskell codes as a result of type inference. Therefore it behaves as a preprocessor which translates the extended language into plain Haskell. Programmers would be able to use polymorphic variants without worrying nasty problems such as ambiguities.


title: GenI: natural language generation in Haskell

abstract: In this article we present GenI, a chart based surface realisation tool implemented in Haskell. GenI takes as input a set of first order terms (the input semantics) and a grammar for a given target language (e.g., English, French, Spanish, etc.) and generates sentences in the target language, whose semantic meaning corresponds to the input semantics.The aim of the article is not so much to present GenI or to describe how it is implemented. Rather, we will focus on the aspects of functional programming (higher order functions, monads) and Haskell (typeclasses) that we found important to its design.


title: An extensible dynamically-typed hierarchy of exceptions

abstract: In this paper we address the lack of extensibility of the exception type in Haskell. We propose a lightweight solution involving the use of existential types and the Typeable class only, and show how our solution allows a fully extensible hierarchy of exception types to be declared, in which a single overloaded catch operator can be used to catch either specific exception types, or exceptions belonging to any subclass in the hierarchy. We also show how to combine the existing object-oriented framework OOHaskell with our design, such that OOHaskell objects can be thrown and caught as exceptions, with full support for implicit OOHaskell subtyping in the catch operator.


title: A generic recursion toolbox for Haskell or: scrap your boilerplate systematically

authors:
Deling Ren
Martin Erwig

abstract: Haskell programmers who deal with complex data types often need to apply functions to specific nodes deeply nested inside of terms. Typically, implementations for those applications require so-called boilerplate code, which recursively visits the nodes and carries the functions to the places where they need to be applied. The scrap-your-boilerplate approach proposed by Lämmel and Peyton Jones tries to solve this problem by defining a general traversal design pattern that performs the traversal automatically so that the programmers can focus on the code that performs the actual transformation.In practice we often encounter applications that require variations of the recursion schema and call for more sophisticated generic traversals. Defining such traversals from scratch requires a profound understanding of the underlying mechanism and is everything but trivial.In this paper we analyze the problem domain of recursive traversal strategies, by integrating and extending previous approaches. We then extend the scrap-your-boilerplate approach by rich traversal strategies and by a combination of transformations and accumulations, which leads to a comprehensive recursive traversal library Reclib in a statically typed framework.We define a two-layer library targeted at general programmers and programmers with knowledge in traversal strategies. The highlevel interface defines a universal combinator that can be customized to different one-pass traversal strategies with different coverage and different traversal order. The lower-layer interface provides a set of primitives that can be used for defining more sophisticated traversal strategies such as fixpoint traversals. The interfaceis simple and succinct. Like the original scrap-your-boilerplate approach, it makes use of rank-2 polymorphism and functional dependencies, implemented in GHC.


title: Strong types for relational databases

authors:
Alexandra Silva
Joost Visser

abstract: Haskell's type system with multi-parameter constructor classes and functional dependencies allows static (compile-time) computations to be expressed by logic programming on the level of types. This emergent capability has been exploited for instance to model arbitrary-length tuples (heterogeneous lists), extensible records, functions with variable length argument lists, and (homogenous) lists of statically fixed length (vectors).We explain how type-level programming can be exploited to define a strongly-typed model of relational databases and operations on them. In particular, we present a strongly typed embedding of a significant subset of SQL in Haskell. In this model, meta-data is represented by type-level entities that guard the semantic correctness of database operations at compile time.Apart from the standard relational database operations, such as selection and join, we model functional dependencies (among table attributes), normal forms, and operations for database transformation. We show how functional dependency information can be represented at the type level, and can be transported through operations. This means that type inference statically computes functional dependencies on the result from those on the arguments.Our model shows that Haskell can be used to design and prototype typed languages for designing, programming, and transforming relational databases.


title: User-level transactional programming in Haskell

abstract: Correct handling of concurrently accessed external resources is a demanding problem in programming. The standard approaches rely on database transactions or concurrency mechanisms like locks. The paper considers two such resources, global variables and databases, and defines transactional APIs for them in Haskell. The APIs provide a novel flavor of user-level transactions which are particularly suitable in the context of web-based systems. This suitability is demonstrated by providing a second implementation in the context of WASH, a Haskell-based Web programming system. The underlying implementation framework works for both kinds of resources and can serve as a blueprint for further implementations of user-level transactions. The Haskell type system provides an encapsulation of the transactional scope that avoids unintended breakage of the transactional guarantees.


title: RepLib: a library for derivable type classes

abstract: Some type class instances can be automatically derived from the structure of types. As a result, the Haskell language includes the "deriving" mechanism to automatic generates such instances for a small number of built-in type classes. In this paper, we present RepLib, a GHC library that enables a similar mechanism for arbitrary type classes. Users of RepLib can define the relationship between the structure of a datatype and the associated instance declaration by a normal Haskell functions that pattern-matches a representation type. Furthermore, operations defined in this manner are extensible-instances for specific types not defined by type structure may also be incorporated. Finally, this library also supports the definition of operations defined by parameterized types.


title: Extended static checking for haskell

abstract: Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and to systems that are guarded by runtime checks. Extended static checking can reduce these costs by helping to detect bugs at compile-time, where possible. Extended static checking has been applied to objectoriented languages, like Java and C#, but it has not been applied to a lazy functional language, like Haskell. In this paper, we describe an extended static checking tool for Haskell, named ESC/Haskell, that is based on symbolic computation and assisted by a few novel strategies. One novelty is our use of Haskell as the specification language itself for pre/post conditions. Any Haskell function (including recursive and higher order functions) can be used in our specification which allows sophisticated properties to be expressed. To perform automatic verification, we rely on a novel technique based on symbolic computation that is augmented by counter-example guided unrolling. This technique can automate our verification process and be efficiently implemented.


title: A shortcut fusion rule for circular program calculation

authors:
João Paulo Fernandes
Alberto Pardo
João Saraiva

abstract: Circular programs are a powerful technique to express multiple traversal algorithms as a single traversal function in a lazy setting. In this paper, we present a shortcut deforestation technique to calculate circular programs. The technique we propose takes as input the composition of two functions, such that the first builds an intermediate structure and some additional context information which are then processed by the second one, to produce the final result. Our transformation into circular programs achieves intermediate structure deforestation and multiple traversal elimination. Furthermore, the calculated programs preserve the termination properties of the original ones.


title: Haskell program coverage

authors:
Andy Gill
Colin Runciman

abstract: We describe the design, implementation and use of HPC, a tool-kit to record and display Haskell Program Coverage. HPC includes tools that instrument Haskell programs to record program coverage, run instrumented programs, and display information derived from coverage data in various ways.


title: Demo outline: switched-on yampa

authors:
George Giorgidze
Henrik Nilsson

abstract: In this demonstration, we present an implementation of a modular synthesizer in Haskell using Yampa. A synthesizer, be it a hardware instrument or a pure software implementation, as here, is said to be modular if it provides sound-generating and sound-shaping components that can be interconnected in arbitrary ways. Yampa, a Haskell-embedded implementation of Functional Reactive Programming, supports flexible construction of hybrid systems. Since music is a hybrid continuous-time and discrete-time phenomenon, Yampa and is a good fit for such applications, offering some unique possibilities compared to most languages targeting music or audio applications. The demonstration illustrates this point by showing how simple audio blocks can be described and then interconnected in a network with dynamically changing structure, reflecting the changing demands of a musical performance.


title: Harpy: run-time code generation in haskell

authors:
Martin Grabmüller
Dirk Kleeblatt

abstract: We present Harpy, a Haskell library for run-time code generation of x86 machine code. Harpy provides efficient generation of machine code, a convenient domain specific language for generating code and a collection of code generation combinators.


title: A type-preserving closure conversion in haskell

authors:
Louis-Julien Guillemette
Stefan Monnier

abstract: The use of typed intermediate languages can significantly increase the reliability of a compiler. By type-checking the code produced at each transformation stage, one can identify bugs in the compiler that would otherwise be much harder to find. Also it guarantees that any property that was enforced by the source-level type-system is holds also or the generated code. Recently, several people have tried to push this effort a bit further by verifying formally that the compiler indeed preserves typing. This is usually done with proof assistants or experimental languages.


title: Comprehensive comprehensions

authors:
Simon L. Peyton Jones
Philip Wadler

abstract: We propose an extension to list comprehensions that makes it easy to express the kind of queries one would write in SQL using ORDER BY, GROUP BY, and LIMIT. Our extension adds expressive power to comprehensions, and generalises the SQL constructs that inspired it. It is easy to implement, using simple desugaring rules.


title: Lightweight concurrency primitives for GHC

authors:
Peng Li
Simon Marlow
Simon L. Peyton Jones
Andrew P. Tolmach

abstract: The Glasgow Haskell Compiler (GHC) has quite sophisticated support for concurrency in its runtime system, which is written in low-level C code. As GHC evolves, the runtime system becomes increasingly complex, error-prone, difficult to maintain and difficult to add new concurrency features.


title: Why it's nice to be quoted: quasiquoting for haskell

abstract: Quasiquoting allows programmers to use domain specific syntax to construct program fragments. By providing concrete syntax for complex data types, programs become easier to read, easier to write, and easier to reason about and maintain. Haskell is an excellent host language for embedded domain specific languages, and quasiquoting ideally complements the language features that make Haskell perform so well in this area. Unfortunately, until now no Haskell compiler has provided support for quasiquoting. We present an implementation in GHC and demonstrate that by leveraging existing compiler capabilities, building a full quasiquoter requires little more work than writing a parser. Furthermore, we provide a compile-time guarantee that all quasiquoted data is type-correct.


title: A lightweight interactive debugger for haskell

authors:
Simon Marlow
José Iborra
Bernard J. Pope
Andy Gill

abstract: This paper describes the design and construction of a Haskell source-level debugger built into the GHCi interactive environment. We have taken a pragmatic approach: the debugger is based on the traditional stop-examine-continue model of online debugging, which is simple and intuitive, but has traditionally been shunned in the context of Haskell because it exposes the lazy evaluation order. We argue that this drawback is not as severe as it may seem, and in some cases is an advantage.


title: Uniform boilerplate and list processing

authors:
Neil Mitchell
Colin Runciman

abstract: Generic traversals over recursive data structures are often referred to as boilerplate code. The definitions of functions involving such traversals may repeat very similar patterns, but with variations for different data types and different functionality. Libraries of operations abstracting away boilerplate code typically rely on elaborate types to make operations generic. The motivating observation for this paper is that most traversals have value-specific behaviour for just one type. We present the design of a new library exploiting this assumption. Our library allows concise expression of traversals with competitive performance.


title: A functional-logic library for wired

authors:
Matthew Naylor
Emil Axelsson
Colin Runciman

abstract: We develop a Haskell library for functional-logic programming, motivated by the implementation of Wired, a relational embedded domain-specific language for describing and analysing digital circuits at the VLSI-layout level. Compared to a previous library for logic programming by Claessen and Ljunglöf, we support residuation, easier creation of logical data types, and pattern matching. We discuss other applications of our library, including test-data generation, and various extensions, including lazy narrowing.


title: Xmonad

authors:
Don Stewart
Spencer Sjanssen

abstract: xmonad is a tiling window manager for the X Window system, implemented, configured and dynamically extensible in Haskell. This demonstration presents the case that software dominated by side effects can be developed with the precision and efficiency we expect from Haskell by utilising purely functional data structures, an expressive type system, extended static checking and property-based testing. In addition, we describe the use of Haskell as an application configuration and extension language.


title: Beauty in the beast

authors:
Wouter Swierstra
Thorsten Altenkirch

abstract: It can be very difficult to debug impure code, let alone prove its correctness. To address these problems, we provide a functional specification of three central components of Peyton Jones's awkward squad: teletype IO, mutable state, and concurrency. By constructing an internal model of such concepts within our programming language, we can test, debug, and reason about programs that perform IO as if they were pure. In particular, we demonstrate how our specifications may be used in tandem with QuickCheck to automatically test complex pointer algorithms and concurrent programs.


title: Shared subtypes: subtyping recursive parametrized algebraic data types

authors:
Ki Yung Ahn
Tim Sheard

abstract: A newtype declaration in Haskell introduces a new type renaming an existing type. The two types are viewed by the programmer as semantically different, but share the same runtime representation. When operations on the two semantic views coincide, the run-time cost of conversion between the two types is reduced to zero (in both directions) because of this common representation.


title: Clase: cursor library for a structured editor

authors:
Tristan Oliver Richard Allwood
Susan Eisenbach

abstract: The zipper is a well known design pattern for providing a cursor-like interface to a data structure. However, the classic treatise by Huet (1) only scratches the surface of some of the potential applications of the zipper. In this work we have taken inspiration from Huet, and built a library suitable as an underpinning for a structured editor for programming languages. We consider a zipper structure that is suitable for traversing heterogeneous data types, encoding routes to other places in the tree (for bookmark or quick-jump functionality), expressing lexically bound information using contexts, and traversals for rendering a program indicating where the cursor is currently focused in the whole.


title: Yi: an editor in haskell for haskell

abstract: Yi is a text editor written in Haskell and extensible in Haskell. We take advantage of Haskell's expressive power to define embedded DSLs that form the foundation of the editor. In turn, these DSLs provide a flexible mechanism to create extended versions of the editor. Yi also provides some support for editing Haskell code.


title: Haskell: batteries included

authors:
Duncan Coutts
Isaac Potoczny-Jones
Don Stewart

abstract: The quality of a programming language itself is only one component in the ability of application writers to get the job done. Programming languages can succeed or fail based on the breadth and quality of their library collection. Over the last few years, the Haskell community has risen to the task of building the library infrastructure necessary for Haskell to succeed as a programming language suitable for writing real-world applications.


title: Language and program design for functional dependencies

authors:
Mark P. Jones
Iavor S. Diatchki

abstract: Eight years ago, functional dependencies, a concept from the theory of relational databases, were proposed as a mechanism for avoiding common problems with multiple parameter type classes in Haskell. In this context, functional dependencies give programmers a means to specify the semantics of a type class more precisely, and to obtain more accurate inferred types as a result. As time passed, however, several issues were uncovered - both in the design of a language to support functional dependencies, and in the ways that programmers use them - that led some to search for new, better alternatives.


title: Making monads first-class with template haskell

authors:
Pericles S. Kariotis
Adam M. Procter
William L. Harrison

abstract: Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.


title: Lightweight monadic regions

authors:
Oleg Kiselyov
Chung-chieh Shan

abstract: We present Haskell libraries that statically ensure the safe use of resources such as file handles. We statically prevent accessing an already closed handle or forgetting to close it. The libraries can be trivially extended to other resources such as database connections and graphic contexts.Because file handles and similar resources are scarce, we want to not just assure their safe use but further deallocate them soon after they are no longer needed. Relying on Fluet and Morrisett's [4] calculus of nested regions, we contribute a novel, improved, and extended implementation of the calculus in Haskell, with file handles as resources.Our library supports region polymorphism and implicit region subtyping, along with higher-order functions, mutable state, recursion, and run-time exceptions. A program may allocate arbitrarily many resources and dispose of them in any order, not necessarily LIFO. Region annotations are part of an expression's inferred type.Our new Haskell encoding of monadic regions as monad transformers needs no witness terms. It assures timely deallocation even when resources have markedly different lifetimes and the identity of the longest-living resource is determined only dynamically.For contrast, we also implement a Haskell library for manual resource management, where deallocation is explicit and safety is assured by a form of linear types. We implement the linear typing in Haskell with the help of phantom types and a parameterized monad to statically track the type-state of resources.