916 papers · page 20 of 46
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 structu…
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…
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…
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 inpu…
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-preservi…
Book review
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 effi…
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 mu…
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 iter…
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 communit…
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 …
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 els…
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 t…
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 sim…
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 …
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 categor…
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.
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 …