1,066 papers · page 40 of 54
We describe a monadic interface to low-level hardware features that is a suitable basis for building operating systems in Haskell. The interface includes primitives for controlling memory management hardware, user-mode process execution, and low-level device I/O. The interface en…
What does it mean for a programming language to exist? Usually languages are defined by an informal description augmented by a reference compiler whose behavior is regarded as normative. This approach works well so long as the one true implementation suffices, but as soon as we w…
We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair conjunctions, conditionals, …
The 'Scrap your boilerplate' approach to generic programming allows the programmer to write generic functions that can traverse arbitrary data structures, and yet have type-specific cases. However, the original approach required all the type-specific cases to be supplied at once,…
MLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that can accommodate a wide rang…
A mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or developed type inference for first…
We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. This paper describes the design and implementation issues of those AOP mechani…
A limited form of dependent types, called Generalized Algebraic Data Types (GADTs), has recently been added to the list of Haskell extensions supported by the Glasgow Haskell Compiler. Despite not being full-fledged dependent types, GADTs still offer considerably enlarged scope f…
Implementing first-class continuations can pose a challenge if the target machine makes no provisions for accessing and re-installing the run-time stack. In this paper, we present a novel translation that overcomes this problem. In the first half of the paper, we introduce a theo…
Hindley and Milner's type system, in its purest form, allows what one might call full type inference. Even when a program contains no explicit type information, its very structure gives rise to a conjunction of type equations (or, more generally, to a constraint) whose resolution…
Narrowing-driven partial evaluation is a powerful technique for the specialization of (first-order) functional and functional logic programs. However, although it gives good results on small programs, it does not scale up well to realistic problems (e.g., interpreter specializati…
Current languages allow a programmer to describe an interface only by enumerating its parts, possibly including other interfaces wholesale. Such languages cannot express relationships between interfaces, yet when independently developed software components are combined into a lar…
We explore partial type-inference for System F based on type-containment. We consider both cases of a purely functional semantics and a call-by-value stateful semantics. To enable type-inference, we require higher-rank polymorphism to be user-specified via type annotations on sou…
We have designed, implemented, and evaluated AtomCaml, an extension to Objective Caml that provides a synchronization primitive for atomic (transactional) execution of code. A first-class primitive function of type (unit->'a)->'a evaluates its argument (which may call other funct…
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some…
Writing loops with tail-recursive function calls is the equivalent of writing them with goto's. Given that loop packages for Lisp-family languages have been around for over 20 years, it is striking that none have had much success in the Scheme world. I suggest the reason is that …
We present a new approach to the old problem of adding side effects to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and …
In this paper a language-based approach to functionally correct imperative programming is proposed. The approach is based on a programming language called RSP1, which combines dependent types, general recursion, and imperative features in a type-safe way, while preserving decidab…
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more expressive. We formalise that the …
Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. If we postulate soundness (in the sense that whenever a term is accused…