Towards more natural functional programming languages
Programming languages are the way for a person to express a mental plan in a way that the computer can understand. Therefore, it is appropriate to consider properties of people when designing new programming languages. In our research, we are ...
Bootstrapping one-sided flexible arrays
The abstract data type one-sided flexible array, also called random-access list, supports look-up and update of elements and can grow and shrink at one end. We describe a purely functional implementation based on weight-balanced multiway trees that is ...
Concatenate, reverse and map vanish for free
We introduce a new transformation method to eliminate intermediate data structures occurring in functional programs due to repeated list concatenations and other data manipulations (additionally exemplified with list reversal and mapping of functions ...
Monads for incremental computing
This paper presents a monadic approach to incremental computation, suitable for purely functional languages such as Haskell. A program that uses incremental computation is able to perform an incremental amount of computation to accommodate for changes ...
Packrat parsing:: simple, powerful, lazy, linear time, functional pearl
Packrat parsing is a novel technique for implementing parsers in a lazy functional programming language. A packrat parser provides the power and flexibility of top-down parsing with backtracking and unlimited lookahead, but nevertheless guarantees ...
Contracts for higher-order functions
Assertions play an important role in the construction of robust software. Their use in programming languages dates back to the 1970s. Eiffel, an object-oriented programming language, wholeheartedly adopted assertions and developed the "Design by ...
An interoperable calculus for external object access
By extending an ML-style type system with record polymorphism, recursive type definition, and an ordering relation induced by field inclusion, it is possible to achieve seamless and type safe interoperability with an object-oriented language. Based on ...
Composable and compilable macros:: you want it when?
Many macro systems, especially for Lisp and Scheme, allow macro transformers to perform general computation. Moreover, the language for implementing compile-time macro transformers is usually the same as the language for implementing run-time functions. ...
A demand-driven adaptive type analysis
Compilers for dynamically and statically typed languages ensure safe execution by verifying that all operations are performed on appropriate values. An operation as simple as car in Scheme and hd in SML will include a run time check unless the compiler ...
Exception analysis for non-strict languages
In this paper we present the first exception analysis for a non-strict language. We augment a simply-typed functional language with exceptions, and show that we can define a type-based inference system to detect uncaught exceptions. We have implemented ...
Modular typechecking for hierarchically extensible datatypes and functions
One promising approach for adding object-oriented (OO) facilities to functional languages like ML is to generalize the existing datatype and function constructs to be hierarchical and extensible, so that datatype variants simulate classes and function ...
Functional formal methods
Some functional programming languages are also mathematical logics. One can reason formally, traditionally, and directly about programs in such languages. This is driving a new application area for functional programming: modeling microarchitectures, ...
Shortcut fusion for accumulating parameters & zip-like functions
We present an alternative approach to shortcut fusion based on the function unfoldr,. Despite its simplicity the technique can remove intermediate lists in examples which are known to be difficult. We show that it can remove all lists from definitions ...
Composing monads using coproducts
Monads are a useful abstraction of computation, as they model diverse computational effects such as stateful computations, exceptions and I/O in a uniform manner. Their potential to provide both a modular semantics and a modular programming style was ...
Interactive visual functional programming
An interactive graphical environment for supporting the development and use of Haskell applications programs is described. The environment, named Vital, is particularly intended for supporting the open-ended, incremental development style often ...
Typing dynamic typing
Even when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include ...
A theory of overloading
We present a minimal extension of the Hindley/Milner system to allow for overloading of identifiers. Our approach relies on a combination of the HM(X) type system framework with Constraint Handling Rules (CHRs). CHRs are a declarative language for ...
Type classes with more higher-order polymorphism
We propose an extension of Haskell's type class system with lambda abstractions in the type language. Type inference for our extension relies on a novel constrained unification procedure called guided higher-order unification. This unification procedure ...
An expressive, scalable type theory for certified code
We present the type theory LTT, intended to form a basis for typed target languages, providing an internal notion of logical proposition and proof. The inclusion of explicit proofs allows the type system to guarantee properties that would otherwise be ...
Meta-programming with names and necessity
Meta-programming languages provide infrastructure to generate and execute object programs at run-time. In a typed setting, they contain a modal type constructor which classifies object code. These code types generally come in two flavors: closed and ...
Tagless staged interpreters for typed languages
Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an ...
There and back again
We present a programming pattern where a recursive function traverses a data structure---typically a list---at return time. The idea is that the recursive calls get us there (typically to a base case) and the returns get us back again while traversing ...
A compiled implementation of strong reduction
Motivated by applications to proof assistants based on dependent types, we develop and prove correct a strong reducer and ß-equivalence checker for the λ-calculus with products, sums, and guarded fixpoints. Our approach is based on compilation to the ...
An experimental study of renewal-older-first garbage collection
Generational collection has improved the efficiency of garbage collection in fast-allocating programs by focusing on collecting young garbage, but has done little to reduce the cost of collecting a heap containing large amounts of older data. A new ...
Compiling scheme to JVM bytecode:: a performance study
We have added a Java virtual machine (henceforth JVM) bytecode generator to the optimizing Scheme-to-C compiler Bigloo. We named this new compiler BiglooJVM. We have used this new compiler to evaluate how suitable the JVM bytecode is as a target for ...
Final shift for call/cc:: direct implementation of shift and reset
We present a direct implementation of the shift and reset control operators in the SFE system. The new implementation improves upon the traditional technique of simulating shift and reset via callcc. Typical applications of these operators exhibit space ...
Program generation, termination, and binding-time analysis
Recent research suggests that the goal of fully automatic and reliable program generation for a broad range of applications is coming nearer to feasibility. However, several interesting and challenging problems remain to be solved before it becomes a ...