title: A pattern for almost compositional functions

authors:
Björn Bringert
Aarne Ranta

abstract: Abstract This paper introduces a pattern for almost compositional functions over recursive data types, and over families of mutually recursive data types. Here “almost compositional” means that for all of the constructors in the type(s), except a limited number of them, the result of the function depends only on the constructor and the results of calling the function on the constructor's arguments. The pattern consists of a generic part constructed once for each data type or family of data types, and a task-specific part. The generic part contains the code for the predictable compositional cases, leaving the interesting work to the task-specific part. Examples of the pattern are given, implemented in dependent type theory with inductive families, in Haskell with generalized algebraic data types and rank-2 polymorphism, and in Java using a variant of the Visitor design pattern. The relationships to the “Scrap Your Boilerplate” approach to generic programming, and to general tree types in dependent type theory, are investigated by reimplementing our operations using those frameworks.


venue: jfp

title: Logic in Computer Science: Modelling and Reasoning About Systems by Michael Huth and Mark Ryan, second edition. ISBN 0 521 54310 X


title: Modular development of certified program verifiers with a proof assistant,

abstract: Abstract We report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checked proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. We take advantage of Coq's support for programming with dependent types and modules in the structure of the development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it is possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.


title: Transactional events

authors:
Kevin Donnelly
Matthew Fluet

abstract: Abstract Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional events , which combines first-class synchronous message passing events with all-or-nothing transactions. This combination enables simple solutions to interesting problems in concurrent programming. For example, guarded synchronous receive can be implemented as an abstract transactional event, whereas in other languages it requires a non-abstract, non-modular protocol. As another example, three-way rendezvous can be implemented as an abstract transactional event, which is impossible using first-class events alone. Both solutions are easy to code and easy to reason about. The expressive power of transactional events arises from a sequencing combinator whose semantics enforces an all-or-nothing transactional property – either both of the constituent events synchronize in sequence or neither of them synchronizes. This sequencing combinator, along with a non-deterministic choice combinator, gives transactional events the compositional structure of a monad-with-plus. We provide a formal semantics for transactional events and give a detailed account of an implementation.


title: Building language towers with Ziggurat

authors:
David Fisher
Olin Shivers

abstract: Abstract Ziggurat is a meta-language system that permits programmers to develop Scheme-like macros for languages with nontrivial static semantics, such as C or Java (suitably encoded in an S-expression concrete syntax). Ziggurat permits language designers to construct ‘towers’ of language levels with macros; each level in the tower may have its own static semantics, such as type systems or flow analyses. Crucially, the static semantics of the languages at two adjacent levels in the tower can be connected, allowing improved reasoning power at a higher level to be reflected down to the static semantics of the language level below. We demonstrate the utility of the Ziggurat framework by implementing higher level language facilities as macros on top of an assembly language, utilizing static semantics such as termination analysis, a polymorphic type system and higher order flow analysis.


title: Efficient execution in an automated reasoning environment

authors:
David A. Greve
Matt Kaufmann
Panagiotis Manolios
J Strother Moore
Sandip Ray
José-Luis Ruiz-Reina
Rob Sumners
Daron Vroon
Matthew Wilding

abstract: Abstract We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.


title: Algebraic fusion of functions with an accumulating parameter and its improvement

authors:
Shin-ya Katsumata
Susumu Nishimura

abstract: Abstract This paper develops a new framework for fusion that is designed for eliminating the intermediate data structures involved in the composition of functions that have one accumulating parameter. The new fusion framework comprises two steps: algebraic fusion and its subsequent improvement process. The key idea in our development is to regard functions with an accumulating parameter as functions that operate over the monoid of data context s. Algebraic fusion composes each such function with a monoid homomorphism that is derived from the definition of the consumer function to obtain a higher-order function that computes over the monoid of endofunctions. The transformation result may be further refined by an improvement process, which replaces the operation over the monoid of endofunctions (i.e., function closures) with another monoid operation over a monoid structure other than function closures. Using our framework, one can formulate a particular solution to the fusion problem by devising appropriate monoids and monoid homomorphisms. This provides a unified exposition of a variety of fusion methods that have been developed so far in different formalisms. Furthermore, the cleaner formulation makes it possible to argue about some delicate issues on a firm mathematical basis. We demonstrate that algebraic fusion and improvement in the world of complete pointed partial orders (CPOs) and continuous functions can correctly fuse functions that operate on partial and infinite data structures. We also show that subtle differences in termination behaviours of transformed programmes caused by certain different fusion methods can be cleanly explained by corresponding improvement processes that have different underlying monoid structures.


title: Translation of tree-processing programs into stream-processing programs based on ordered linear type

authors:
Koichi Kodama
Kohei Suenaga
Naoki Kobayashi

abstract: Abstract There are two ways to write a program for manipulating tree-structured data such as XML documents: One is to write a tree-processing program focusing on the logical structure of the data and the other is to write a stream-processing program focusing on the physical structure. While tree-processing programs are easier to write than stream-processing programs, tree-processing programs are less efficient in memory usage since they use trees as intermediate data. Our aim is to establish a method for automatically translating a tree-processing program to a stream-processing one in order to take the best of both worlds. We first define a programming language for processing binary trees and a type system based on ordered linear type, and show that every well-typed program can be translated to an equivalent stream-processing program. We then extend the language and the type system to deal with XML documents. We have implemented an XML stream processor generator based on our algorithm, and obtained promising experimental results.


title: Editorial

abstract: The Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP 2006) took place on September 18–20, 2006 in Portland, Oregon. ICFP 2006 provides a forum for researchers and developers to hear about the latest work on the design, implementation, principles, and uses of functional programming. The conference covers the entire spectrum of work, from theory to practice, and beyond. There were 74 submissions, of which the program committee selected 24 for presentation at the conference. Following the conference, the program committee selected eight papers for which the authors were invited to submit extended versions for this special issue of JFP. The seven papers that appear in this volume were reviewed, revised, and accepted following standard JFP procedures. These papers cover a wide range of topics related to functional programming, including programming, program verification, language design, language development, program transformation, and program analysis. This range of topics reflects the variety of the work presented at the ICFP conference.


title: An operational semantics for Scheme

authors:
Jacob Matthews
Robert Bruce Findler

abstract: Abstract This paper presents an operational semantics for the core of Scheme. Our specification improves over the denotational semantics from the Revised 5 Report on Scheme specification in four ways. First, it covers a larger part of the language, specifically eval , quote , dynamic-wind , and the top level. Second, it models multiple values in a way that does not require changes to unrelated parts of the language. Third, it provides a faithful model of Scheme's undefined order of evaluation. Finally, we have implemented our specification in PLT Redex, a domain-specific language for writing operational semantics. The implementation allows others to experiment with our specification and allows us to build a specification test suite, which improves our confidence that our system is a faithful model of Scheme. In addition to a specification of Scheme, this paper contributes three novel modeling techniques for Felleisen Hieb-style rewriting semantics. All three techniques are applicable to a wider range of problems than modeling Scheme, and they combine seamlessly in our model, suggesting that they would scale to complete models of other languages.


title: Applicative programming with effects

authors:
Conor McBride
Ross Paterson

abstract: Abstract In this article, we introduce Applicative functors – an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this programming pattern that drew us to the abstraction. We retrace our steps in this article, introducing the applicative pattern by diverse examples, then abstracting it to define the Applicative type class and introducing a bracket notation that interprets the normal application syntax in the idiom of an Applicative functor. Furthermore, we develop the properties of applicative functors and the generic operations they support. We close by identifying the categorical structure of applicative functors and examining their relationship both with Monads and with Arrow.


title: Exploiting reachability and cardinality in higher-order flow analysis

authors:
Matthew Might
Olin Shivers

abstract: Abstract We present two complementary improvements for abstract-interpretation-based flow analysis of higher-order languages: (1) abstract garbage collection and (2) abstract counting . Abstract garbage collection is an analog to its concrete counterpart: the analysis determines when an abstract resource has become unreachable, and then, re-allocates it as fresh. This prevents flow sets from joining during abstract interpretation, which has two immediate effects: (1) the precision of the interpretation increases and (2) its running time often falls. In abstract counting, the analysis tracks how many times an abstract resource has been allocated. A count of one implies that the abstract resource momentarily represents only one concrete resource. This knowledge, in turn, drives environment analysis, expanding the kind (rather than just the degree) of optimization available to the compiler.


title: Caml trading - experiences with functional programming on Wall Street

authors:
Yaron Minsky
Stephen Weeks

abstract: Abstract Jane Street Capital is a successful proprietary trading company that uses OCaml as its primary development language. We have over twenty OCaml programmers and hundreds of thousands of lines of OCaml code. We use OCaml for a wide range of tasks: critical trading systems, quantitative research, systems software, and system administration. We value OCaml because it allows us to rapidly produce readable, correct, efficient code to solve complex problems, and to change that code quickly to adapt to a changing world. We believe that using OCaml gives us a significant advantage over competitors that use languages like VB, Perl, C++, C#, or Java. It also makes finding and hiring high-quality software developers easier than with mainstream languages. We have invested deeply in OCaml and intend to use OCaml and grow our team of functional programmers for the foreseeable future.


title: Hoare type theory, polymorphism and separation

authors:
Aleksandar Nanevski
J. Gregory Morrisett
Lars Birkedal

abstract: Abstract We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and nontermination. We propose Hoare type theory (HTT), which incorporates Hoare-style specifications into types, making it possible to statically track and enforce correct use of side effects. The main feature of HTT is the Hoare type { P } x : A { Q } specifying computations with precondition P and postcondition Q that return a result of type A . Hoare types can be nested, combined with other types, and abstracted, leading to a smooth integration with higher-order functions and type polymorphism. We further show that in the presence of type polymorphism, it becomes possible to interpret the Hoare types in the “small footprint” manner, as advocated by separation logic, whereby specifications tightly describe the state required by the computation. We establish that HTT is sound and compositional, in the sense that separate verifications of individual program components suffice to ensure the correctness of the composite program.


title: Lightweight family polymorphism

authors:
Chieri Saito
Atsushi Igarashi
Mirko Viroli

abstract: Abstract Family polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the original proposal, due to the design decision that families are represented by objects, dependent types had to be introduced, resulting in a rather complex type system. In this article, we propose a simpler solution of lightweight family polymorphism, based on the idea that families are represented by classes rather than by objects. This change makes the type system significantly simpler without losing much expressive power of the language. Moreover, “family-polymorphic” methods now take a form of parametric methods; thus, it is easy to apply method type argument inference as in Java 5.0. To rigorously show that our approach is safe, we formalize the set of language features on top of Featherweight Java and prove that the type system is sound. An algorithm for type inference for family-polymorphic method invocations is also formalized and proved to be correct. Finally, a formal translation by erasure to Featherweight Java is presented; it is proved to preserve typing and execution results, showing that our new language features can be implemented in Java by simply extending the compiler.


title: Safety of Nöcker's strictness analysis

authors:
Manfred Schmidt-Schauß
David Sabel
Marko Schütz

abstract: Abstract This paper proves correctness of Nöcker's method of strictness analysis, implemented in the Clean compiler, which is an effective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work Clark, Hankin and Hunt did on the correctness of the abstract reduction rules in two aspects. Our correctness proof is based on a functional core language and a contextual semantics, thus proving a wider range of strictness-based optimizations as correct, and our method fully considers the cycle detection rules, which contribute to the strength of Nöcker's strictness analysis. Our algorithm SAL is a reformulation of Nöcker's strictness analysis algorithm in a functional core language LR. This is a higher order call-by-need lambda calculus with case , constructors, letrec , and seq , which is extended during strictness analysis by set constants like Top or Inf , denoting sets of expressions, which indicate different evaluation demands. It is also possible to define new set constants by recursive equations with a greatest fixpoint semantics. The operational semantics of LR is a small-step semantics. Equality of expressions is defined by a contextual semantics that observes termination of expressions. Basically, SAL is a nontermination checker. The proof of its correctness and hence of Nöcker's strictness analysis is based mainly on an exact analysis of the lengths of evaluations, i.e., normal-order reduction sequences to WHNF. The main measure being the number of “essential” reductions in evaluations. Our tools and results provide new insights into call-by-need lambda calculi, the role of sharing in functional programming languages, and into strictness analysis in general. The correctness result provides a foundation for Nöcker's strictness analysis in Clean, and also for its use in Haskell.


title: Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction

authors:
Peter Sewell
Gareth Paul Stoyle
Michael Hicks
Gavin M. Bierman
Keith Wansbrough

abstract: Abstract Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example, when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically, it is provided only by ad hoc mechanisms that lack clean semantics. In this paper, we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply typed call-by-value λ calculus. To do so, we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex - time and destruct - time strategies. The latter forms the basis for a λ marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically typed. We sketch an extension of λ marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a λ update calculus with simple primitives to provide type-safe updating of running code. We show how the ideas of this simple calculus extend to more real-world, module-level dynamic updating in the style of Erlang. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.


title: Types and trace effects of higher order programs

authors:
Christian Skalka
Scott F. Smith
David Van Horn

abstract: Abstract This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so-called event traces . Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the λ-calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the trace effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain trace event checks that can fail at run-time.


title: HM(X) type inference is CLP(X) solving

authors:
Martin Sulzmann
Peter J. Stuckey

abstract: Abstract The HM(X) system is a generalization of the Hindley/Milner system parameterized in the constraint domain X. Type inference is performed by generating constraints out of the program text, which are then solved by the domain-specific constraint solver X. The solver has to be invoked at the latest when type inference reaches a let node so that we can build a polymorphic type. A typical example of such an inference approach is Milner's algorithm W. We formalize an inference approach where the HM(X) type inference problem is first mapped to a CLP(X) program. The actual type inference is achieved by executing the CLP(X) program. Such an inference approach supports the uniform construction of type inference algorithms and has important practical consequences when it comes to reporting type errors. The CLP(X) style inference system, where X is defined by Constraint Handling Rules, is implemented as part of the Chameleon system.


title: Data types à la carte

abstract: Abstract This paper describes a technique for assembling both data types and functions from isolated individual components. We also explore how the same technology can be used to combine free monads and, as a result, structure Haskell's monolithic IO monad.


title: Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism

authors:
Geoffrey Washburn
Stephanie Weirich

abstract: Abstract Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higher-order abstract syntax. To fold over such a data type, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the data type are parametric. In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data structures containing functionals. From this implementation, we derive “fusion laws” that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schürmann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System . This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.


title: Implementing a normalizer using sized heterogeneous types

abstract: Abstract In the simply typed λ-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a , removing freshly created redexes on the fly. It can be defined by lexicographic induction on a and r , thus giving rise to a structurally recursive normalizer for the simply typed λ-calculus. We implement hereditary substitutions in a functional programming language with sized heterogeneous inductive types $\Fhat$ , arriving at an interpreter whose termination can be tracked by the type system of its host programming language.


title: Big-step normalisation

authors:
Thorsten Altenkirch
James Chapman

abstract: Abstract Traditionally, decidability of conversion for typed λ-calculi is established by showing that small-step reduction is confluent and strongly normalising. Here we investigate an alternative approach employing a recursively defined normalisation function which we show to be terminating and which reflects and preserves conversion. We apply our approach to the simply typed λ-calculus with explicit substitutions and βη-equality, a system which is not strongly normalising. We also show how the construction can be extended to system T with the usual β-rules for the recursion combinator. Our approach is practical, since it does verify an actual implementation of normalisation which, unlike normalisation by evaluation, is first order. An important feature of our approach is that we are using logical relations to establish equational soundness (identity of normal forms reflects the equational theory), instead of the usual syntactic reasoning using the Church–Rosser property of a term rewriting system.


title: The lambda-calculus with constructors: Syntax, confluence and separation

authors:
Ariel Arbiser
Alexandre Miquel
Alejandro Ríos

abstract: Abstract We present an extension of the λ(η)-calculus with a case construct that propagates through functions like a head linear substitution, and show that this construction permits to recover the expressiveness of ML-style pattern matching. We then prove that this system enjoys the Church–Rosser property using a semi-automatic ‘divide and conquer’ technique by which we determine all the pairs of commuting subsystems of the formalism (considering all the possible combinations of the nine primitive reduction rules). Finally, we prove a separation theorem similar to Böhm's theorem for the whole formalism.


title: Parameterised notions of computation

abstract: Abstract Moggi's Computational Monads and Power et al .'s equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-determinism, exceptions, continuations, side effects and input/output. We present generalisations of both computational monads and Freyd categories, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with parameters. Examples of such are composable continuations, side effects where the type of the state varies and input/output where the range of inputs and outputs varies. By considering structured parameterisation also, we extend the range of effects to cover separated side effects and multiple independent streams of I/O. We also present two typed λ-calculi that soundly and completely model our categorical definitions – with and without symmetric monoidal parameterisation – and act as prototypical languages with parameterised effects.


title: Programming in Haskell by Graham Hutton, Cambridge University Press, 2007, 184 pp., ISBN 0-521-69269-5


title: Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages

authors:
Jacques Carette
Oleg Kiselyov
Chung-chieh Shan

abstract: Abstract We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.


title: Essentials of Programming Languages (third edition) by Daniel P. Friedman and Mitchell Wand, MIT Press, ISBN 978-0-262-06279-4, 2008

abstract: Book review


title: From natural semantics to C: A formal derivation of two STG machines

authors:
Alberto de la Encina
Ricardo Peña-Marí

abstract: Abstract The Spineless Tag-less G-machine (STG machine) was defined as the target abstract machine for compiling the lazy functional language Haskell. It is at the heart of the Glasgow Haskell Compiler (GHC) which is claimed to be the Haskell compiler that generates the most efficient code. A high-level description of the STG machine can be found in Peyton Jones (In Journal of Functional programming, 2(2), 127–202, 1992), Marlow & Peyton Jones (In Sigplan Not., 39(9), 4–5, 2004), and Marlow & Peyton Jones (In Journal of Functional Programming, 16(4–5), 415–449, 2006). Should the reader be interested in a more detailed view, then the only additional information available is the Haskell code of GHC and the C code of its runtime system. It is hard to prove that this machine correctly implements the lazy semantics of Haskell. Part of the problem lies in the fact that the STG machine executes a bare-bones functional language, called STGL, much lower level than Haskell. Therefore, part of the correctness should be—and it is—established by showing that the translation from Haskell to STGL preserves Haskell's semantics. The other part involves showing that the STG machine correctly implements the lazy semantics of STGL. In this paper we provide a step-by-step formal derivation of the STG machine and of its compilation to C, starting from a natural semantics of STGL. Thus, our starting point is higher level than the descriptions found Peyton Jones (In Journal of Functional programming, 2(2), 127–202, 1992) and Marlow & Peyton Jones (In Sigplan Not., 39(9), 4–5, 2004), and our arrival point is lower level than those works. Additionally, there has been substantial changes between the so-called push/enter model of the STG machine described in Peyton Jones (In Journal of Functional programming, 2(2), 127–202, 1992), and the eval/apply model of the STG machine described in Marlow & Peyton Jones (In Sigplan Not., 39(9), 4–5, 2004). So, in fact, we derive two machines instead of one, starting from the same initial semantics. At each step we provide enough intuitions and explanations in order to understand the refinement, and then the formal definitions and statements proving that the derivation step is sound and complete. The main contribution of the paper is to show that an efficient machine such as the STG can be presented, understood, and formally reasoned about at different levels of abstraction.


title: Commercial uses: Going functional on exotic trades

authors:
Simon Frankau
Diomidis Spinellis
Nick Nassuphis
Christoph Burgard

abstract: Abstract The Functional Payout Framework ( fpf ) is a Haskell application that uses an embedded domain-specific functional language to represent and process exotic financial derivatives. Whereas scripting languages for pricing exotic derivatives are common in banking, fpf uses multiple interpretations to not only price such trades, but also to analyse the scripts to provide lifecycle support and more. This paper discusses fpf in relation to the wider trading workflow and our experiences in using a functional language in such a system as both an implementation language and a domain-specific language.


title: Peter Van Roy and Seif Haridi. Concepts, Techniques, and Models of Computer Programming. The MIT Press, 2004. ISBN: 0262220695 Price $70. 930pp


title: The essence of the Iterator pattern

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

abstract: Abstract The Iterator pattern gives a clean interface for element-by-element access to a collection, independent of the collection's shape. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating . Various existing functional models of iteration capture one or other of these aspects, but not both simultaneously. We argue that C. McBride and R. Paterson's applicative functors (Applicative programming with effects, J. Funct. Program. , 18 (1): 1–13, 2008), and in particular the corresponding traverse operator, do exactly this, and therefore capture the essence of the Iterator pattern. Moreover, they do so in a way that nicely supports modular programming. We present some axioms for traversal, discuss modularity concerns and illustrate with a simple example, the wordcount problem.


title: The worker/wrapper transformation

authors:
Andy Gill
Graham Hutton

abstract: Abstract The worker/wrapper transformation is a technique for changing the type of a computation, usually with the aim of improving its performance. It has been used by compiler writers for many years, but the technique is little known in the wider functional programming community, and has never been described precisely. In this article we explain, formalise and explore the generality of the worker/wrapper transformation. We also provide a systematic recipe for its use as an equational reasoning technique for improving the performance of programs, and illustrate the power of this recipe using a range of examples.


title: FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum

abstract: There is a minor error in Section 3 wherein it is stated that ∖acc 0_ _ k loops in_nitely, even if k succeeds on input _.” This statement is not correct, and should be replaced by ∖If k returns false on input cs, then acc 1_ cs k loops in_nitely.” The author is grateful to Derek Dreyer for pointing out this mistake, and suggesting the above-mentioned correction.


title: The Bird Tree

abstract: Sadly, Richard Bird is stepping down as the editor of the ‘Functional Pearls’ column. As a farewell present, I would like to dedicate a tree to him. A woody plant is appropriate for at least two reasons: Richard has been preoccupied with trees in many of his pearls, and where else would you find a bird's nest? Actually, there is a lot of room for nests, as the tree is infinite. Figure 1 displays the first five levels. The Bird tree, whose nodes are labelled with rational numbers, enjoys several remarkable properties.


title: Purely Functional 1-2 Brother Trees

abstract: Enter the computing arboretum and you will find a variety of well-studied trees: AVL trees (Adel'son-Vel'skiĭ & Landis 1962), symmetric binary B-trees (Bayer 1972), Hopcroft's 2-3 trees (Aho et al . 1974), the bushy finger trees (Guibas et al . 1977) and the colourful red-black trees (Guibas & Sedgewick 1978). In this pearl, we look at a more exotic species of balanced search trees, 1-2 brother trees (Ottmann et al . 1979), which deserves to be better known. Brother trees lend themselves well to a functional implementation with deletion (Section 5) as straightforward as insertion (Section 3), both running in logarithmic time. Furthermore, brother trees can be constructed from ordered lists in linear time (Section 4). With some simple optimisations in place, this implementation of search trees is one of the fastest around. So, fasten your seat belts.


title: Categorical semantics for arrows

authors:
Bart Jacobs
Chris Heunen
Ichiro Hasuo

abstract: Abstract Arrows are an extension of the well-established notion of a monad in functional-programming languages. This paper presents several examples and constructions and develops denotational semantics of arrows as monoids in categories of bifunctors C op × C → C . Observing similarities to monads – which are monoids in categories of endofunctors C → C – it then considers Eilenberg–Moore and Kleisli constructions for arrows. The latter yields Freyd categories, mathematically formulating the folklore claim ‘Arrows are Freyd categories.’


title: First-class patterns

authors:
C. Barry Jay
Delia Kesner

abstract: Abstract Pure pattern calculus supports pattern-matching functions in which patterns are first-class citizens that can be passed as parameters, evaluated and returned as results. This new expressive power supports two new forms of polymorphism. Path polymorphism allows recursive functions to traverse arbitrary data structures. Pattern polymorphism allows patterns to be treated as parameters which may be collected from various sources or generated from training data. A general framework for pattern calculi is developed. It supports a proof of confluence that is parameterised by the nature of the matching algorithm, suitable for the pure pattern calculus and all other known pattern calculi.


title: Gabriel-Ulmer duality and Lawvere theories enriched over a general base

authors:
Stephen Lack
John Power

abstract: Abstract Motivated by the search for a body of mathematical theory to support the semantics of computational effects, we first recall the relationship between Lawvere theories and monads on Set . We generalise that relationship from Set to an arbitrary locally presentable category such as Poset and ω Cpo or functor categories such as [ Inj , Set ] and [ Inj , ω Cpo ]. That involves allowing the arities of Lawvere theories to be extended to being size-restricted objects of the locally presentable category. We develop a body of theory at this level of generality, in particular explaining how the relationship between generalised Lawvere theories and monads extends Gabriel–Ulmer duality.


title: Editorial

abstract: This issue of the Journal of Functional Programming (JFP) marks a point of transition. After serving since 1991 as Editor, then since 2004 as co-Editor in Chief (along with Greg Morrisett from 2004 to 2006 and Xavier Leroy since 2007), Paul Hudak is stepping down.


title: Editorial

authors:
Xavier Leroy
Matthias Felleisen

abstract: Eighteen years ago Richard Bird joined the editorial team of the Journal of Functional Programming . As Richard mentions in his recollections (Bird, 2006), the founding editors of the Journal , Simon Peyton Jones and Philip Wadler, had asked him to contribute a regular column to be called Functional Pearls , roughly modeled on the Programming Pearls that Jon Bentley had run for the Communications of the ACM in the 1980s. Richard agreed to the suggestion, but only under the proviso that he would seek other contributors to the column.


title: An induction principle for nested datatypes in intensional type theory

abstract: Abstract Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Moreover, the argument types of the constructors refer to indices given by expressions in which the family name may occur. Especially in this case of true nesting, termination of functions that traverse these data structures is far from being obvious. A joint paper with A. Abel and T. Uustalu ( Theor. Comput. Sci ., 333 (1–2), 2005, pp. 3–66) proposed iteration schemes that guarantee termination not by structural requirements but just by polymorphic typing. They are generic in the sense that no specific syntactic form of the underlying datatype “functor” is required. However, there was no induction principle for the verification of the programs thus obtained, although they are well known in the usual model of initial algebras on endofunctor categories. The new contribution is a representation of nested datatypes in intensional type theory (more specifically, in the calculus of inductive constructions) that is still generic and covers true nesting, guarantees termination of all expressible programs, and has an induction principle that allows to prove functoriality of monotonicity witnesses (maps for nested datatypes) and naturality properties of iteratively defined polymorphic functions.


title: Preface

authors:
Conor McBride
Tarmo Uustalu

abstract: This special issue of the Journal of Functional Programming collects revised selected articles arising from the inaugural meeting of the Workshop on Mathematically Structured Functional Programming, MSFP 2006, held in Kuressaare, Estonia, on 2 July 2006, with support from the European Union's FP6 IST Coordination Action TYPES. This workshop raised the curtain for the Eighth International Conference on Mathematics of Program Construction, MPC 2006, but where MPC is concerned primarily with extrinsic mathematics supporting the programming process, MSFP has a complementary focus on the mathematics intrinsic to programs themselves. MSFP is about the extraction of functionality from structure.


title: Algebra of programming in Agda: Dependent types for relational program derivation

authors:
Shin-Cheng Mu
Hsiang-Shang Ko
Patrik Jansson

abstract: Abstract Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker. We have developed a library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.


title: Small-step and big-step semantics for call-by-need

authors:
Keiko Nakata
Masahito Hasegawa

abstract: Abstract We present natural semantics for acyclic as well as cyclic call-by-need lambda calculi, which are proved equivalent to the reduction semantics given by Ariola and Felleisen ( J. Funct. Program. , vol. 7, no. 3, 1997). The natural semantics are big-step and use global heaps, where evaluation is suspended and memorized. The reduction semantics are small-step, and evaluation is suspended and memorized locally in let-bindings. Thus two styles of formalization describe the call-by-need strategy from different angles. The natural semantics for the acyclic calculus is revised from the previous presentation by Maraist et al . ( J. Funct. Program. , vol. 8, no. 3, 1998), and its adequacy is ascribed to its correspondence with the reduction semantics, which has been proved equivalent to call-by-name by Ariola and Felleisen. The natural semantics for the cyclic calculus is inspired by that of Launchbury (1993) and Sestoft (1997), and we state its adequacy using a denotational semantics in the style of Launchbury; adequacy of the reduction semantics for the cyclic calculus is in turn ascribed to its correspondence with the natural semantics.


title: The Genuine Sieve of Eratosthenes

abstract: Abstract A much beloved and widely used example showing the elegance and simplicity of lazy functional programming represents itself as “The Sieve of Eratosthenes.” This paper shows that this example is not the sieve and presents an implementation that actually is.


title: Regular-expression derivatives re-examined

authors:
Scott Owens
John H. Reppy
Aaron Turon

abstract: Abstract Regular-expression derivatives are an old, but elegant, technique for compiling regular expressions to deterministic finite-state machines. It easily supports extending the regular-expression operators with boolean operations, such as intersection and complement. Unfortunately, this technique has been lost in the sands of time and few computer scientists are aware of it. In this paper, we reexamine regular-expression derivatives and report on our experiences in the context of two different functional-language implementations. The basic implementation is simple and we show how to extend it to handle large character sets (e.g., Unicode). We also show that the derivatives approach leads to smaller state machines than the traditional algorithm given by McNaughton and Yamada.


title: Type-safe higher-order channels with channel locality

authors:
Sungwoo Park
Hyeonseung Im

abstract: Abstract As a means of transmitting not only data but also code encapsulated within functions, higher-order channels provide an advanced form of task parallelism in parallel computations. In the presence of mutable references, however, they pose a safety problem because references may be transmitted to remote threads where they are no longer valid. This paper presents an ML-like parallel language with type-safe higher-order channels. By type safety, we mean that no value written to a channel contains references, or equivalently, that no reference escapes via a channel from the thread where it is created. The type system uses a typing judgment that is capable of deciding whether the value to which a term evaluates contains references or not. The use of such a typing judgment also makes it easy to achieve another desirable feature of channels, channel locality , that associates every channel with a unique thread for serving all values addressed to it. Our type system permits mutable references in sequential computations and also ensures that mutable references never interfere with parallel computations. Thus, it provides both flexibility in sequential programming and ease of implementing parallel computations.


title: Type-safe pattern combinators

abstract: Abstract Macros still haven't made their way into typed higher-order programming languages such as Haskell and Standard ML. Therefore, to extend the expressiveness of Haskell or Standard ML, one must express new linguistic features in terms of functions that fit within the static type systems of these languages. This is particularly challenging when introducing features that span across multiple types and that bind variables. We address this challenge by developing, in a step by step manner, mechanisms for encoding patterns and pattern matching in Haskell in a type-safe way.


title: Programming Erlang - Software for a Concurrent World by Joe Armstrong, Pragmatic Bookshelf, 2007, p. 536. ISBN-10: 193435600X


title: Monadic constraint programming

authors:
Tom Schrijvers
Peter J. Stuckey
Philip Wadler

abstract: Abstract A constraint programming system combines two essential components: a constraint solver and a search engine. The constraint solver reasons about satisfiability of conjunctions of constraints, and the search engine controls the search for solutions by iteratively exploring a disjunctive search tree defined by the constraint program. In this paper we give a monadic definition of constraint programming in which the solver is defined as a monad threaded through the monadic search tree. We are then able to define search and search strategies as first-class objects that can themselves be built or extended by composable search transformers. Search transformers give a powerful and unifying approach to viewing search in constraint programming, and the resulting constraint programming system is first class and extremely flexible.


title: Coherence of subsumption for monadic types

abstract: Abstract One approach to give semantics to languages with subtypes is by translation to target languages without subtyping: subtypings A ≤ B are interpreted via conversion functions A → B . This paper shows how to extend the method to languages with computational effects, using Moggi's computational metalanguage.


title: Software Abstractions: Logic, Language, and Analysis by Daniel Jackson, The MIT Press, 2006, 366pp, ISBN 978-0262101141


title: Algebras for combinatorial search

abstract: Abstract Combinatorial search strategies including depth-first, breadth-first and depth-bounded search are shown to be different implementations of a common algebraic specification that emphasizes the compositionality of the strategies. This specification is placed in a categorical setting that combines algebraic specifications and monads.


title: Linear, bounded, functional pretty-printing

authors:
S. Doaitse Swierstra
Olaf Chitil

abstract: Abstract We present two implementations of Oppen's pretty-printing algorithm in Haskell that meet the efficiency of Oppen's imperative solution but have a simpler and a clear structure. We start with an implementation that uses lazy evaluation to simulate two co-operating processes. Then we present an implementation that uses higher-order functions for delimited continuations to simulate co-routines with explicit scheduling.


title: Control effects as a modality

abstract: Abstract We combine ideas from types for continuations, effect systems and monads in a very simple setting by defining a version of classical propositional logic in which double-negation elimination is combined with a modality. The modality corresponds to control effects, and it includes a form of effect masking. Erasing the modality from formulas gives classical logic. On the other hand, the logic is conservative over intuitionistic logic.


title: A domain-specific language for experimental game theory

authors:
Eric Walkingshaw
Martin Erwig

abstract: Abstract Experimental game theory is increasingly important for research in many fields. Unfortunately, it is poorly supported by computer tools. We have created Hagl, a domain-specific language embedded in Haskell, to reduce the development time of game-theoretic experiments and make the definition and exploration of games and strategies simple and fun.


title: Generic programming with C++ concepts and Haskell type classes - a comparison

authors:
Jean-Philippe Bernardy
Patrik Jansson
Marcin Zalewski
Sibylle Schupp

abstract: Abstract Earlier studies have introduced a list of high-level evaluation criteria to assess how well a language supports generic programming. Languages that meet all criteria include Haskell because of its type classes and C++ with the concept feature. We refine these criteria into a taxonomy that captures commonalities and differences between type classes in Haskell and concepts in C++ and discuss which differences are incidental and which ones are due to other language features. The taxonomy allows for an improved understanding of language support for generic programming, and the comparison is useful for the ongoing discussions among language designers and users of both languages.


title: "Little language" project modules

authors:
John Clements
Kathi Fisler

abstract: Abstract Many computer science departments are debating the role of programming languages in the curriculum. These discussions often question the relevance and appeal of programming-languages content for today's students. In our experience, domain-specific, “little languages” projects provide a compelling illustration of the importance of programming-language concepts. This paper describes projects that prototype mainstream applications such as PowerPoint, TurboTax, and animation scripting. We have used these exercises as modules in non-programming languages courses, including courses for first year students. Such modules both encourage students to study linguistic topics in more depth and provide linguistic perspective to students who might not otherwise be exposed to the area.


title: NixOS: A purely functional Linux distribution

authors:
Eelco Dolstra
Andres Löh
Nicolas Pierron

abstract: Abstract Existing package and system configuration management tools suffer from an imperative model , where system administration actions such as package upgrades or changes to system configuration files are stateful: they destructively update the state of the system. This leads to many problems, such as the inability to roll back changes easily, to deploy multiple versions of a package side-by-side, to reproduce a configuration deterministically on another machine, or to reliably upgrade a system. In this paper we show that we can overcome these problems by moving to a purely functional system configuration model . This means that all static parts of a system (such as software packages, configuration files and system startup scripts) are built by pure functions and are immutable, stored in a way analogous to a heap in a purely functional language. We have implemented this model in NixOS , a non-trivial Linux distribution that uses the Nix package manager to build the entire system configuration from a modular, purely functional specification.


title: Implicitly threaded parallelism in Manticore

authors:
Matthew Fluet
Mike Rainey
John H. Reppy
Adam Shaw

abstract: Abstract The increasing availability of commodity multicore processors is making parallel computing ever more widespread. In order to exploit its potential, programmers need languages that make the benefits of parallelism accessible and understandable. Previous parallel languages have traditionally been intended for large-scale scientific computing, and they tend not to be well suited to programming the applications one typically finds on a desktop system. Thus, we need new parallel-language designs that address a broader spectrum of applications. The Manticore project is our effort to address this need. At its core is Parallel ML, a high-level functional language for programming parallel applications on commodity multicore hardware. Parallel ML provides a diverse collection of parallel constructs for different granularities of work. In this paper, we focus on the implicitly threaded parallel constructs of the language, which support fine-grained parallelism. We concentrate on those elements that distinguish our design from related ones, namely, a novel parallel binding form, a nondeterministic parallel case form, and the treatment of exceptions in the presence of data parallelism. These features differentiate the present work from related work on functional data-parallel language designs, which have focused largely on parallel problems with regular structure and the compiler transformations—most notably, flattening—that make such designs feasible. We present detailed examples utilizing various mechanisms of the language and give a formal description of our implementation.


title: Linear type theory for asynchronous session types

authors:
Simon J. Gay
Vasco Thudichum Vasconcelos

abstract: Abstract Session types support a type-theoretic formulation of structured patterns of communication, so that the communication behaviour of agents in a distributed system can be verified by static typechecking. Applications include network protocols, business processes and operating system services. In this paper we define a multithreaded functional language with session types, which unifies, simplifies and extends previous work. There are four main contributions. First is an operational semantics with buffered channels, instead of the synchronous communication of previous work. Second, we prove that the session type of a channel gives an upper bound on the necessary size of the buffer. Third, session types are manipulated by means of the standard structures of a linear type theory, rather than by means of new forms of typing judgement. Fourth, a notion of subtyping, including the standard subtyping relation for session types (imported into the functional setting), and a novel form of subtyping between standard and linear function types, which allows the typechecker to handle linear types conveniently. Our new approach significantly simplifies session types in the functional setting, clarifies their essential features and provides a secure foundation for language developments such as polymorphism and object-orientation.


title: Editorial

abstract: I have just taken over from Richard Bird as editor of the Functional Pearls column in the Journal of Functional Programming . I'm keen to receive submissions; please do get in touch if you'd like to discuss a potential paper.


title: Concrete stream calculus: An extended study

abstract: Abstract This paper shows how to reason about streams concisely and precisely. Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive datatype, operations on streams are implemented by corecursive programs, and proofs are typically concocted using coinduction. This paper offers an alternative to coinduction. Suitably restricted, stream equations possess unique solutions . This property gives rise to a simple and attractive proof technique, essentially bringing equational reasoning to the coworld. We redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators, building on the cornerstone of unique solutions. The paper contains a smörgåsbord of examples: we study recursion elimination, investigate the binary carry sequence, explore Sprague-Grundy numbers and present two proofs of Moessner's Theorem. The calculations benefit from the rich structure of streams. As the type of streams is an applicative functor we can effortlessly lift operations and their properties to streams. In combination with Haskell's facilities for overloading, this greatly contributes to conciseness of notation. The development is indeed constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use.


title: Special Issue on Generic Programming Editorial

abstract: Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast to normal programs, the parameters of a generic program are often quite rich in structure; for example, they may be other programs, types or type constructors, classes, concepts, or even programming paradigms.


title: Factorising folds for faster functions

authors:
Graham Hutton
Mauro Jaskelioff
Andy Gill

abstract: Abstract The worker/wrapper transformation is a general technique for improving the performance of recursive programs by changing their types. The previous formalisation (A. Gill & G. Hutton, J. Funct. Program. , vol. 19, 2009, pp. 227–251) was based upon a simple fixed-point semantics of recursion. In this paper, we develop a more structured approach, based upon initial-algebra semantics. In particular, we show how the worker/wrapper transformation can be applied to programs defined using the structured pattern of recursion captured by fold operators, and illustrate our new technique with a number of examples.


title: The arrow calculus

authors:
Sam Lindley
Philip Wadler
Jeremy Yallop

abstract: Abstract We introduce the arrow calculus, a metalanguage for manipulating Hughes's arrows with close relations both to Moggi's metalanguage for monads and to Paterson's arrow notation. Arrows are classically defined by extending lambda calculus with three constructs satisfying nine (somewhat idiosyncratic) laws; in contrast, the arrow calculus adds four constructs satisfying five laws (which fit two well-known patterns). The five laws were previously known to be sound; we show that they are also complete, and hence that the five laws may replace the nine.


title: A lightweight approach to datatype-generic rewriting

authors:
Thomas van Noort
Alexey Rodriguez Yakushev
Stefan Holdermans
Johan Jeuring
Bastiaan Heeren
José Pedro Magalhães

abstract: Abstract Term-rewriting systems can be expressed as generic programs parameterised over the shape of the terms being rewritten. Previous implementations of generic rewriting libraries require users to either adapt the datatypes that are used to describe these terms or to specify rewrite rules as functions. These are fundamental limitations: the former implies a lot of work for the user, while the latter makes it hard if not impossible to document, test, and analyze rewrite rules. In this article, we demonstrate how to overcome these limitations by making essential use of type-indexed datatypes. Our approach is lightweight in that it is entirely expressible in Haskell with GADTs and type families and can be readily packaged for use with contemporary Haskell distributions.


title: Scala for generic programmers

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

abstract: Abstract Datatype-generic programming (DGP) involves parametrization of programs by the shape of data, in the form of type constructors such as ‘list of’. Most approaches to DGP are developed in pure functional programming languages such as Haskell. We argue that the functional object-oriented language Scala is in many ways a better choice. Not only does Scala provide equivalents of all the necessary functional programming features (such as parametric polymorphism, higher-order functions, higher-kinded type operations, and type- and constructor-classes), but it also provides the most useful features of object-oriented languages (such as subtyping, overriding, traditional single inheritance, and multiple inheritance in the form of traits). Common Haskell techniques for DGP can be conveniently replicated in Scala, whereas the extra expressivity provides some important additional benefits in terms of extensibility and reuse. We illustrate this by comparing two simple approaches in Haskell, pointing out their limitations and showing how equivalent approaches in Scala address some of these limitations. Finally, we present three case studies on how to implement in Scala real DGP approaches from the literature: Hinze's ‘Generics for the Masses’, Lämmel and Peyton Jones's ‘Scrap your Boilerplate with Class’, and Gibbons's ‘Origami Programming’.


title: Ott: Effective tool support for the working semanticist

authors:
Peter Sewell
Francesco Zappa Nardelli
Scott Owens
Gilles Peskine
Thomas Ridge
Susmit Sarkar
Rok Strnisa

abstract: Abstract Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics – usually either for informal mathematics or the formal mathematics of a proof assistant – make it much harder than necessary to work with large definitions. We present a metalanguage specifically designed for this problem, and a tool, Ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together with code for production-quality typesetting, and OCaml boilerplate. The main innovations are (1) metalanguage design to make definitions concise, and easy to read and edit; (2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code. This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (OCaml light , 310 rules), with mechanised proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.


title: Space profiling for parallel functional programs

authors:
Daniel Spoonhower
Guy E. Blelloch
Robert Harper
Phillip B. Gibbons

abstract: Abstract We present a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to program source code. Unlike many profiling tools, our profiler is based on a cost semantics. This provides a means to reason about performance without requiring a detailed understanding of the compiler or runtime system. It also provides a specification for language implementers. This is critical in that it enables us to separate cleanly the performance of the application from that of the language implementation. Some aspects of the implementation can have significant effects on performance. Our cost semantics enables programmers to understand the impact of different scheduling policies while hiding many of the details of their implementations. We show applications where the choice of scheduling policy has asymptotic effects on space use. We explain these use patterns through a demonstration of our tools. We also validate our methodology by observing similar performance in our implementation of a parallel extension of Standard ML.


title: Special Issue Dedicated to ICFP 2008 Editorial

authors:
Peter Thiemann
Henrik Nilsson

abstract: The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP) was held in Victoria, British Columbia, Canada, in September 2008. Peter Thiemann chaired the program committee. After the conference, the authors of a selection of the presented papers were invited to submit extended versions of their work for this special issue of Journal of Functional Programming dedicated to ICFP 2008. All submitted papers were reviewed by at least three referees, including at least one expert, following the standard JFP procedures. In the end, four papers were accepted. These cover a broad range of topics and, taken together, we think they represent well the scope of ICFP 2008.


title: Formal polytypic programs and proofs

authors:
Wendy Verbruggen
Edsko de Vries
Arthur Hughes

abstract: Abstract The aim of our work is to be able to do fully formal, machine-verified proofs over Generic Haskell-style polytypic programs. In order to achieve this goal, we embed polytypic programming in the proof assistant Coq and provide an infrastructure for polytypic proofs. Polytypic functions are reified within Coq as a datatype and they can then be specialized by applying a dependently typed term specialization function. Polytypic functions are thus first-class citizens and can be passed as arguments or returned as results. Likewise, we reify polytypic proofs as a datatype and provide a lemma that a polytypic proof can be specialized to any datatype in the universe. The correspondence between polytypic functions and their polytypic proofs is very clear: programmers need to give proofs for, and only for, the same cases that they need to give instances for when they define the polytypic function itself. Finally, we discuss how to write (co)recursive functions and do (co)recursive proofs in a similar way that recursion is handled in Generic Haskell.


title: Parametricity, type equality, and higher-order polymorphism

authors:
Dimitrios Vytiniotis
Stephanie Weirich

abstract: Abstract Propositions that express type equality are a frequent ingredient of modern functional programming – they can encode generic functions, dynamic types, and GADTs. Via the Curry–Howard correspondence, these propositions are ordinary types inhabited by proof terms , computed using runtime type representations. In this paper we show that two examples of type equality propositions actually do reflect type equality; they are only inhabited when their arguments are equal and their proofs are unique (up to equivalence.) We show this result in the context of a strongly normalizing language with higher-order polymorphism and primitive recursion over runtime-type representations by proving Reynolds's abstraction theorem. We then use this theorem to derive “free” theorems about equality types.


title: Experience report: Functional programming in C-Rules

abstract: Abstract C-Rules is a business rules management system developed by Constraint Technologies International ( www.constrainttechnologies.com ) that is designed for use in transport, travel and logistics problems. Individual businesses within these industries often need to solve the same kinds of problems related to scheduling of operations, resource allocation, staff rostering and so on, but each organisation has its own rules and procedures. Furthermore, these problems tend to be combinatorially challenging: before a final solution is chosen, many potential choices need to be generated, evaluated and compared. In C-Rules, users define rules that describe various aspects of a problem. These rules can be invoked from an application, which is typically either an optimising solver or an interactive planning tool. Rules can be used to encode evaluation criteria, such as the legality or cost of a proposed solution, or values like configuration parameters that may be used by the host application to tune or direct its progress. At its core, C-Rules provides a functional expression language that affords users power and flexibility when formulating rules. In this paper we will describe our experiences of using functional programming both at the end-user level and at the implementation level. We highlight some of the benefits of basing our rule system on features such as higher-order functions, referential transparency and static, polymorphic typing. We also outline some of our experiences in using Haskell to build an efficient compiler for the core language.


title: Lightweight checkpointing for concurrent ML

authors:
Lukasz Ziarek
Suresh Jagannathan

abstract: Abstract Transient faults that arise in large-scale software systems can often be repaired by reexecuting the code in which they occur. Ascribing a meaningful semantics for safe reexecution in multithreaded code is not obvious, however. For a thread to reexecute correctly a region of code, it must ensure that all other threads that have witnessed its unwanted effects within that region are also reverted to a meaningful earlier state. If not done properly, data inconsistencies and other undesirable behavior might result. However, automatically determining what constitutes a consistent global checkpoint is not straightforward because thread interactions are a dynamic property of the program. In this paper, we present a safe and efficient checkpointing mechanism for Concurrent ML (CML) that can be used to recover from transient faults. We introduce a new linguistic abstraction, called stabilizers , that permits the specification of per-thread monitors and the restoration of globally consistent checkpoints. Safe global states are computed through lightweight monitoring of communication events among threads (e.g., message-passing operations or updates to shared variables). We present a formal characterization of its design, and provide a detailed description of its implementation within MLton, a whole-program optimizing compiler for Standard ML. Our experimental results on microbenchmarks as well as several realistic, multithreaded, server-style CML applications, including a web server and a windowing toolkit, show that the overheads to use stabilizers are small, and lead us to conclude that they are a viable mechanism for defining safe checkpoints in concurrent functional programs.


title: The Soccer-Fun project

abstract: Abstract In the Soccer-Fun , students program the brains of football players in a functional language. Soccer-Fun has been developed for an introductory course in functional programming at the Radboud University Nijmegen, The Netherlands. We have used Soccer-Fun in teaching during the past four years. We have also experience in using Soccer-Fun for pupils in secondary education. Soccer-Fun is stimulating because it is about a well-known problem domain. It engages students to problem solving with functional programming because it allows them to compete at several disciplines: the best performing football team becomes the champion of a tournament; the best written code is awarded with a prize; students are judged on the algorithms used. This enables every student to participate and perform at her favorite skill. Soccer-Fun is implemented in Clean and uses its GUI toolkit Object I/O for rendering. It can be implemented in any functional programming language that supports some kind of windowing toolkit.


title: Building a consensus: A rectangle covering problem

abstract: The other day, over a very pleasant lunch in the restaurant of Oxford's recently renovated Ashmolean Museum, Oege de Moor gave me a problem about rectangles. The problem is explained more fully later, but roughly speaking one is given a finite set of rectangles RS and a rectangle R completely covered by RS . The task is to construct a single rectangle covering R among the elements of a larger set of rectangles associated with RS , called the saturation of RS . The saturation of RS is the closure of RS under so-called consensus operations, a term coined in (Quine, 1959), in which two rectangles are combined in two distinct ways to form new rectangles. The rectangle problem is a simplified version of containment-checking, a crucial component in a type inference algorithm for Datalog programs (Schäfer & de Moor, 2010). 19 In the Schäfer-de Moor algorithm the problem is generalised to cubes in n -space rather than rectangles in two-space, the components of each cube are given by propositional formulae rather than by intervals on the real line, and certain equality and inhabitation constraints are taken into account. Oege felt that the central proof, Lemma 15 in (Schäfer & de Moor, 2010), deserved to be simplified so he posed the rectangle problem as a special case. This pearl was composed in response to the challenge.


title: Roles, stacks, histories: A triple for Hoare

authors:
Johannes Borgström
Andrew D. Gordon
Riccardo Pucella

abstract: Abstract Behavioral type and effect systems regulate properties such as adherence to object and communication protocols, dynamic security policies, avoidance of race conditions, and many others. Typically, each system is based on some specific syntax of constraints, and is checked with an ad hoc solver. Instead, we advocate types refined with first-order logic formulas as a basis for behavioral type systems, and general purpose automated theorem provers as an effective means of checking programs. To illustrate this approach, we define a triple of security-related type systems: for role-based access control, for stack inspection, and for history-based access control. The three are all instances of a refined state monad. Our semantics allows a precise comparison of the similarities and differences of these mechanisms. In our examples, the benefit of behavioral type-checking is to rule out the possibility of unexpected security exceptions, a common problem with code-based access control.


title: Handbook of Practical Logic and Automated Reasoning, by John Harrison, Cambridge University Press, 2009 ISBN 9780521899574

abstract: The steady rise in interest in formal verification of software has naturally been accompanied by increased interest in the theory and tools of verification.While there are many textbooks of logic as well as user guides for the vast array of reasoning tools (automated and otherwise), much less is written about how to bridge the two, never mind good guides to the design problems of building reasoning tools.Harrison's Handbook of Practical Logic and Automated Reasoning explores that gap with flair.Even a casual glance at this hefty 700 page book will quickly dispel any "Handbook" impression which the title disingenuously gives: not a handbook at all, but rather a proper textbook.The style, far from that of a reference book, is deeply pedagogical, complete with a significant set of well-crafted exercises.It is well written using lucid prose, with the author taking great pains to elucidate important points, pausing to illustrate some subtleties, as well as being rather erudite in its coverage of the relevant literature, both historical and contemporary.As a textbook style introduction to the theory and practice of (first order, mathematical) logic and automated reasoning, it succeeds beautifully.This textbook masterfully weaves together theory and practice, by interleaving the development of the theoretical underpinnings of each topic covered with fairly well crafted code which implements the constructive portions of each chosen topic.In other words, this textbook is also a literate program, with all code written in OCaml, available from Harrison's web site.This really forces the author to cover many topics which are often, regrettably, omitted from other "practical" introductions to logic.Readers primarily interested in the theory covered by this book may find this aspect distracting, but I rather view this aspect of the book as one of its more endearing characteristics.The prose aspects of this literate textbook could easily serve as a model for years to come.The code is written using a fairly small subset of the Objective Caml language (no objects, Functors, higher rank polymorphism, nor polymorphic variants).While higher-order functions abound, the author nevertheless does not make heavy use of a more combinator-driven style which is more prevalent in the current functional literature.Eschewing Functors also means that the higher abstractions frequently seen in modern functional programs are also not used.While such a choice does broaden the audience which can easily understand the code, it would nevertheless be quite interesting to redevelop the same code, first in idiomatic Haskell, and then in Agda.But doing this would surely result in a research-level monograph, which was clearly not the author's intent.In other words, while this text does not use the most modern functional programming idioms, this was clearly an explicit decision, which makes sense in the context of the audience for this book.The set of topics covered might seem somewhat eclectic: propositional logic, first-order logic, equality reasoning, decidable problems, interactive theorem-proving and the limitations of all these approaches.In particular, "decidable problems" and "interactive theorem-proving" have traditionally been seen as belonging in different universes by the more "pure" adherents of formal reasoning.Of course, there have always been systems which eschewed this particular balkanisition, with ACL2, IMPS and PVS immediately coming to mind, and Harrison's own HOL Light following in the tradition.But this is now changing, as traditionally very pure


title: How to think about algorithms, by Jeff Edmonds, Cambridge University Press, ISBN 0521614104


title: Purely functional lazy nondeterministic programming

authors:
Sebastian Fischer
Oleg Kiselyov
Chung-chieh Shan

abstract: Abstract Functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (nonstrict evaluation with sharing of the results) with nondeterminism. Yet these benefits are seldom enjoyed in functional programming because the existing features for nonstrictness, sharing, and nondeterminism in functional languages are tricky to combine. We present a practical way to write purely functional lazy nondeterministic programs that are efficient and perspicuous. We achieve this goal by embedding the programs into existing languages (such as Haskell, SML, and OCaml) with high-quality implementations, by making choices lazily and representing data with nondeterministic components, by working with custom monadic data types and search strategies, and by providing equational laws for the programmer to reason about their code.


title: The Hough transform

abstract: Suppose you are given a number of points in a plane and want to have those lines that each contain a large number of the given points. The Hough transform is a computerized procedure for that task. It was invented by Paul Hough (1962), originally to find the trajectories of subatomic particles in a bubble chamber, and it has even been patented. Nowadays, adaptations of the Hough transform are used, among others, for identification of transformed instances of a predefined figure, instead of just a line, in a digital picture. There are plenty of explanations on the Internet (use search key “Hough transform” and “generalized Hough transform”), some with nice applets to demonstrate the working (add search key “applet” or “demo”). Recently, Hart (2009) has looked back at the invention. We show how the original procedure could have been derived.


title: More on balanced diets

authors:
Oliver Friedmann
Martin Lange

abstract: Abstract Discrete Interval Encoding Trees are data structures for the representation of fat, i.e. densely populated sets over a discrete linear order. In this paper, we introduce algorithms for set-theoretic operations like intersection, union, etc. on sets represented as balanced diets. We empirically analyse their performance and show that these algorithms can outperform previously known algorithms on sets, such as the ones implemented in OCaml's standard library.


title: Review: Lambda-Calculus and Combinators: An Introduction, Second Edition by J. R. Hindley and J. P. Seldin


title: Short note: Strict unwraps make worker/wrapper fusion totally correct

abstract: Abstract The worker/wrapper transformation is a general way of changing the type of a recursive definition, usually applied with an eye to increasing algorithmic efficiency. This note identifies an infelicity in the program transformations presented by Gill & Hutton (The worker/wrapper transformation, J. Funct. Program ., vol. 19, 2009, pp. 227–251) and proposes a new totally correct worker/wrapper fusion rule.


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


title: Typed quote/antiquote or: Compile-time parsing

abstract: Haskell (Peyton Jones, 2003) is often used as a host language for embedding other languages. Typically, the abstract syntax of the guest language is defined by a collection of datatype declarations; parsers and pretty-printers convert between the concrete syntax and its abstract representation. A quote/antiquote mechanism permits a tighter integration of the guest language into the host language by allowing one to use phrases in the guest language's concrete syntax .


title: Balancing weight-balanced trees

authors:
Yoichi Hirai
Kazuhiko Yamamoto

abstract: Abstract A weight-balanced tree (WBT) is a binary search tree, whose balance is based on the sizes of the subtrees in each node. Although purely functional implementations on a variant WBT algorithm are widely used in functional programming languages, many existing implementations do not maintain balance after deletion in some cases. The difficulty lies in choosing a valid pair of rotation parameters: one for standard balance and the other for choosing single or double rotation. This paper identifies the exact valid range of the rotation parameters for insertion and deletion in the original WBT algorithm where one and only one integer solution exists. Soundness of the range is proved using a proof assistant Coq. Completeness is proved using effective algorithms generating counterexample trees. For two specific parameter pairs, we also proved in Coq that set operations also maintain balance. Since the difference between the original WBT and the variant WBT is small, it is easy to change the existing buggy implementations based on the variant WBT to the certified original WBT with a rational solution.


title: Foundations of F# Robert Pickering, Apress, 2007 ISBN 10: 1-59059-757-5


title: Shifting the stage - Staging with delimited control

authors:
Yukiyoshi Kameyama
Oleg Kiselyov
Chung-chieh Shan

abstract: Abstract It is often hard to write programs that are efficient yet reusable. For example, an efficient implementation of Gaussian elimination should be specialized to the structure and known static properties of the input matrix. The most profitable optimizations, such as choosing the best pivoting or memoization, cannot be expected of even an advanced compiler because they are specific to the domain, but expressing these optimizations directly makes for ungainly source code. Instead, a promising and popular way to reconcile efficiency with reusability is for a domain expert to write code generators. Two pillars of this approach are types and effects. Typed multilevel languages such as MetaOCaml ensure safety and early error reporting: a well-typed code generator neither goes wrong nor generates code that goes wrong. Side effects such as state and control ease correctness and expressivity : An effectful generator can resemble the textbook presentation of an algorithm, as is familiar to domain experts, yet insert let for memoization and if for bounds checking, as is necessary for efficiency. Together, types and effects enable structuring code generators as compositions of modules with well-defined interfaces, and hence scaling to large programs. However, blindly adding effects renders multilevel types unsound. We introduce the first multilevel calculus with control effects and a sound type system. We give small-step operational semantics as well as a one-pass continuation-passing-style translation. For soundness, our calculus restricts the code generator's effects to the scope of generated binders. Even with this restriction, we can finally write efficient code generators for dynamic programming and numerical methods in direct style, like in algorithm textbooks, rather than in continuation-passing or monadic style.


title: Causal commutative arrows

authors:
Hai Liu
Eric Cheng
Paul Hudak

abstract: Abstract Arrows are a popular form of abstract computation. Being more general than monads, they are more broadly applicable, and, in particular, are a good abstraction for signal processing and dataflow computations. Most notably, arrows form the basis for a domain-specific language called Yampa , which has been used in a variety of concrete applications, including animation, robotics, sound synthesis, control systems, and graphical user interfaces. Our primary interest is in better understanding the class of abstract computations captured by Yampa. Unfortunately, arrows are not concrete enough to do this with precision. To remedy this situation, we introduce the concept of commutative arrows that capture a noninterference property of concurrent computations. We also add an init operator that captures the causal nature of arrow effects, and identify its associated law. To study this class of computations in more detail, we define an extension to arrows called causal commutative arrows (CCA), and study its properties. Our key contribution is the identification of a normal form for CCA called causal commutative normal form (CCNF). By defining a normalization procedure, we have developed an optimization strategy that yields dramatic improvements in performance over conventional implementations of arrows. We have implemented this technique in Haskell, and conducted benchmarks that validate the effectiveness of our approach. When compiled with the Glasgow Haskell Compiler (GHC), the overall methodology can result in significant speedups.


title: Non-parametric parametricity

authors:
Georg Neis
Derek Dreyer
Andreas Rossberg

abstract: Abstract Type abstraction and intensional type analysis are features seemingly at odds—type abstraction is intended to guarantee parametricity and representation independence, while type analysis is inherently non-parametric. Recently, however, several researchers have proposed and implemented “dynamic type generation” as a way to reconcile these features. The idea is that, when one defines an abstract type, one should also be able to generate at runtime a fresh type name, which may be used as a dynamic representative of the abstract type for purposes of type analysis. The question remains: in a language with non-parametric polymorphism, does dynamic type generation provide us with the same kinds of abstraction guarantees that we get from parametric polymorphism? Our goal is to provide a rigorous answer to this question. We define a step-indexed Kripke logical relation for a language with both non-parametric polymorphism (in the form of type-safe cast) and dynamic type generation. Our logical relation enables us to establish parametricity and representation independence results, even in a non-parametric setting, by attaching arbitrary relational interpretations to dynamically generated type names. In addition, we explore how programs that are provably equivalent in a more traditional parametric logical relation may be “wrapped” systematically to produce terms that are related by our non-parametric relation, and vice versa. This leads us to develop a “polarized” variant of our logical relation, which enables us to distinguish formally between positive and negative notions of parametricity.


title: A note on the genuine Sieve of Eratosthenes

abstract: Abstract O'Neill (The genuine Sieve of Eratosthenes. J. Funct. Program . 19 (1), 2009, 95–106) has previously considered a functional implementation for the genuine Sieve of Eratosthenes, based on the well-known heap data structure. Here, we develop it further by adapting this data structure to this particular application.


title: A calculus for hardware description

authors:
Sungwoo Park
Hyeonseung Im

abstract: Abstract In efforts to overcome the complexity of the syntax and the lack of formal semantics of conventional hardware description languages, a number of functional hardware description languages have been developed. Like conventional hardware description languages, however, functional hardware description languages eventually convert all source programs into netlists, which describe wire connections in hardware circuits at the lowest level and conceal all high-level descriptions written into source programs. We develop a calculus, called l λ (linear lambda), which may serve as an intermediate functional language just above netlists in the hierarchy of hardware description languages. In order to support higher-order functions, l λ uses a linear type system, which enforces the linear use of variables of function type. The translation of l λ into structural descriptions of hardware circuits is sound and complete in the sense that it maps expressions only to realizable hardware circuits, and that every realizable hardware circuit has a corresponding expression in l λ. To illustrate the use of l λ as a practical intermediate language for hardware description, we design a simple hardware description language that extends l λ with polymorphism, and use it to implement a fast Fourier transform circuit and a bitonic sorting network.


title: Structural recursion with locally scoped names

abstract: Abstract This paper introduces a new recursion principle for inductively defined data modulo α-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. It is formulated in simply typed λ-calculus extended with names that can be restricted to a lexical scope, tested for equality, explicitly swapped and abstracted. The new recursion principle is motivated by the nominal sets notion of ‘α-structural recursion’, whose use of names and associated freshness side-conditions in recursive definitions formalizes common practice with binders. The new calculus has a simple interpretation in nominal sets equipped with name-restriction operations. It is shown to adequately represent α-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. The paper is a revised and expanded version of Pitts (Nominal System T. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 2010 (Madrid, Spain) . ACM Press, pp. 159–170, 2010).


title: Embedding an interpreted language using higher-order functions and types

abstract: Abstract Using an embedded, interpreted language to control a complicated application can have significant software-engineering benefits. But existing interpreters are designed for embedding into C code. To embed an interpreter into a different language requires an API suited to that language. This paper presents Lua-ML, a new API that is suited to languages that provide higher-order functions and types. The API exploits higher-order functions and types to reduce the amount of glue code needed to use an embedded interpreter. Where embedding in C requires a special-purpose “glue function” for every function to be embedded, embedding in Lua-ML requires only a description of each function's type. Lua-ML also makes it easy to define a Lua function whose behavior depends on the number and types of its arguments.


title: Functional and dynamic programming in the design of parallel prefix networks

abstract: Abstract A parallel prefix network of width n takes n inputs, a 1 , a 2 , . . ., a n , and computes each y i = a 1 ○ a 2 ○ ⋅ ⋅ ⋅ ○ a i for 1 ≤ i ≤ n , for an associative operator ○. This is one of the fundamental problems in computer science, because it gives insight into how parallel computation can be used to solve an apparently sequential problem. As parallel programming becomes the dominant programming paradigm, parallel prefix or scan is proving to be a very important building block of parallel algorithms and applications. There are many different parallel prefix networks, with different properties such as number of operators, depth and allowed fanout from the operators. In this paper, ideas from functional programming are combined with search to enable a deep exploration of parallel prefix network design. Networks that improve on the best known previous results are generated. It is argued that precise modelling in a functional programming language, together with simple visualization of the networks, gives a new, more experimental, approach to parallel prefix network design, improving on the manual techniques typically employed in the literature. The programming idiom that marries search with higher order functions may well have wider application than the network generation described here.


title: A combinator library for the design of railway track layouts

abstract: Abstract In the design of railway track layouts, there are only a small number of geometric configurations that are used in practice, and a number of constraints as to how those configurations can be fitted together to create a whole layout. In order to solve these problems, we construct a Haskell combinator library. The library has been used for the design of real-world track layouts.


title: Sorted - Verifying the Problem of the Dutch National Flag in Agda

abstract: The problem of the Dutch national flag was formulated by Dijkstra (1976) as follows: There is a row of buckets numbered from 1 to n. It is given that : P1 : each bucket contains one pebble P2 : each pebble is either red, white, or blue . A minicomputer is placed in front of this row of buckets and has to be programmed in such a way that it will rearrange (if necessary) the pebbles in the order of the Dutch national flag . The minicomputer in question should perform this rearrangement using two commands: • swap i j for 1≤ i ≤ n and 1≤ j ≤ n exchanges the pebbles stored in the buckets numbered i and j ; • read ( i ) for 1≤ i ≤ n returns the colour of the pebble currently lying in bucket number i . Dijkstra originally named this operation buck .


title: Special Issue Dedicated to ICFP 2009 Editorial

authors:
Andrew P. Tolmach
Xavier Leroy

abstract: The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on August 31–September 2, 2009 in Edinburgh, Scotland; Andrew Tolmach chaired the program committee. Following the conference, the authors of selected papers were invited to submit extended versions for this special issue of JFP. After review and revision, four papers were accepted for inclusion in this volume. Each paper contains substantial new material beyond the original conference version. The papers are representative of the wide range of topics and methodology that characterize ICFP.


title: OutsideIn(X) Modular type inference with local assumptions

authors:
Dimitrios Vytiniotis
Simon L. Peyton Jones
Tom Schrijvers
Martin Sulzmann

abstract: Abstract Advanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and – perhaps controversially – argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called OutsideIn(X) , is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. OutsideIn(X) extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7.