Previous work on semantics-based multi-stage programming (MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designs simply add a hygienic quasi-quotation and evaluation mechanism to a base language. An apparent disadvantage of this approach is that the programmer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means to avoid this by providing specialized translations from subsets of the base language to different target languages. This approach preserves the homogeneous “look” of multi-stage programs, and, more importantly, the static guarantees about the generated code. In addition, compared to an explicitly heterogeneous approach, it promotes reuse of generator source code and systematic exploration of the performance characteristics of the target languages. To illustrate the proposed approach, we design and implement a translation to a subset of C suitable for numerical computation, and show that it preserves static typing. The translation is implemented, and evaluated with several benchmarks. The implementation is available in the online distribution of MetaOCaml.

Writing (meta-)programs that manipulate other (object-) programs poses significant technical problems when the objectlanguage itself has a notion of binders and variable occurrences. Higher-order abstract syntax is a representation of object programs that has recently been the focus of several studies. This paper points out a number of limitations of using higher order syntax in a functional context, and argues that DALI, a language based on a simple and elegant proposal made by Dale Miller ten years ago can provide superior support for manipulating such object-languages. Miller's original proposal, however, did not provide any formal treatment. To fill this gap, we present both a big-step and a reduction semantics for DALI, and summarize the results of our extensive study of the semantics, including the rather involved proof of the soundness of the reduction semantics with respect to the big-step semantics. Because our formal development is carried out for the untyped version of the language, we hope it will serve as a solid basis for investigating type system(s) for DALI.

Previous work on semantics-based multi-stage programming (MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designs simply add a hygienic quasi-quotation and evaluation mechanism to a base language. An apparent disadvantage of this approach is that the programmer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means to avoid this by providing specialized translations from subsets of the base language to different target languages. This approach preserves the homogeneous “look” of multi-stage programs, and, more importantly, the static guarantees about the generated code. In addition, compared to an explicitly heterogeneous approach, it promotes reuse of generator source code and systematic exploration of the performance characteristics of the target languages. To illustrate the proposed approach, we design and implement a translation to a subset of C suitable for numerical computation, and show that it preserves static typing. The translation is implemented, and evaluated with several benchmarks. The implementation is available in the online distribution of MetaOCaml.

Previous work on semantics-based multi-stage programming (MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designs simply add a hygienic quasi-quotation and evaluation mechanism to a base language. An apparent disadvantage of this approach is that the programmer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means to avoid this by providing specialized translations from subsets of the base language to different target languages. This approach preserves the homogeneous " look " of multi-stage programs, and, more importantly, the static guarantees about the generated code. In addition, compared to an explicitly heterogeneous approach, it promotes reuse of generator source code and systematic exploration of the performance characteristics of the target languages. This is a revised version based on a conference paper of the same title 4). To illustrate the proposed approach, we design and implement a translation to a subset of C suitable for numerical computation, and show that it preserves static typing. The translation is implemented, and evaluated with several benchmarks. The implementation is available in the online distribution of MetaOCaml. Multi-stage programming (MSP) languages allow the programmer to use abstraction mechanisms such as functions, objects, and modules, without having to pay a runtime overhead for them due to the generation of specialized code. Operationally, these languages provide quasi-quotation and eval mechanisms similar to those of LISP and Scheme. In addition, to avoid accidental capture, bound variables are always renamed, and values produced by quasi-quotes can only be de-constructed by eval. This makes reasoning about quoted terms as programs sound 18) , even in the untyped setting. Several type systems have been developed that statically ensure that all programs generated using these constructs are well-typed (see for example 19, 1)). Currently, the main examples of MSP languages include MetaScheme 7) , MetaML 20) , MetaOCaml 10) , and Metaphor 11). They are based, respectively, on Scheme, Standard ML, OCaml, and Java/C#. In all these cases, the language design is homogeneous, in that quoted values are fragments of the base language. Homogeneity has three distinct advantages. First, it is convenient for the language designer, as it often reduces the size of the definitions needed to model a language, and makes extensions to arbitrary stages feasible at little cost. Second, it is convenient for the language implementor, as it allows the implementation …

In this paper, we describe two techniques for the efficient, modularized implementation of a large class of algorithms. We illustrate these techniques using several examples, including efficient generic unification algorithms that use reference cells to encode substitutions, and highly modular language implementations. We chose these examples to illustrate the following important techniques that we believe many functional programmers would find useful. First, defining recursive data types by splitting them into two levels: a structure defining level, and a recursive knot-tying level. Second, the use of rank-2 polymorphism inside Haskell's record types to implement a kind of type-parameterized modules. Finally, we explore techniques that allow us to combine already existing recursive Haskell data-types with the highly modular style of programming proposed here.

Meta-programming, writing programs that write other programs, involves two kinds of languages. The meta-language is the language in which meta-programs, which construct or manipulate other programs, are written. The object-language is the language of programs being manipulated. We study a class of meta-language features that are used to write meta-programs that are statically guaranteed to maintain semantic invariants of object-language programs, such as typing and scoping. We use type equality in the type system of the meta-language to check and enforce these invariants. Our main contribution is the illustration of the utility of type equality in typed functional meta-programming. In particular, we encode and capture judgments about many important language features using type equality. Finally, we show how type equality is incorporated as a feature of the type system of a practical functional meta-programming language. The core of this thesis is divided into three parts. First, we design a meta-programming language with dependent types. We use dependent types to ensure that well-typed meta-programs manipulate only well-typed object-language programs. Using this meta-language, we then construct highly efficient and safe interpreters for a strongly typed object language. We also prove the type safety of the meta-language. Second, we demonstrate how the full power of dependent types is not necessary to encode typing properties of object-languages. We explore a meta-language consisting of the programming language Haskell and a set of techniques for encoding type equality. In this setting we are able to carry out essentially the same meta-programming examples. We also expand the range of object-language features in our examples (e.g., pattern matching). Third, we design a meta-language (called Omega) with built-in equality proofs. This language is a significant improvement for meta-programming over Haskell: Omega's type system automatically manipulates proofs of type equalities in meta-programs. We further demonstrate our encoding and meta-programming techniques by providing representations and interpreters for object-languages with explicit substitutions and modal type systems.

We report our experience with exploring a new point in the design space for formal reasoning systems: the development of the programming language mega. mega is intended as both a practical programming language and a logic. The main goal of mega is to allow programmers to describe and reason about semantic properties of programs from within the programming language itself, mainly by using a powerful type system. We illustrate the main features of mega by developing an interesting meta-programming example. First, we show how to encode a set of well-typed simply typed �-calculus terms as an mega data-type. Then, we show how to implement a substitution operation on these terms that is guaranteed by the mega type system to preserve their well-typedness.

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 untyped setting, staging an interpreter "removes a complete layer of interpretive overhead", just like partial evaluation. In a typed setting however, Hindley-Milner type systems do not allow us to exploit typing information in the language being interpreted. In practice, this can mean a slowdown cost by a factor of three or mor.Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experience with the issues that arise in writing such an interpreter and in designing such a language. .To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (called Meta-D) and prove its type safety. To formalize Meta-D, we extend Shao, Saha, Trifonov and Papaspyrou's λH language to a multi-level setting. Building on λH allows us to demonstrate type safety in a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work needed for establishing the soundness of that system.

When an Automated Testing Equipment (ATE) company designs a new system, the issue of backward compatibility is always a major concern, both for the company and its customers. If backward compatibility is maintained, the ATE application engineers face the difficult task of trying to support new features on an aging system. The alternative is to face the problem of converting old test programs to the new environment. Translation of legacy code involves an automatic translation tool, and some application effort applied to those problems the translatorcouldn't resolve. To minimize the amount of work required from the application engineers, the tool need to be semantically-aware; that is, the tool must contain domain-specific knowledge and use that knowledge when translating. The more knowledge a tool has at its disposal, the less code an application engineer is forced to translate by hand.Until recently, it has been difficult to perform automatic translation satisfactorily because it was not cost effective to write a translator that possessed such semantic understanding of the test programs. By making good use of Functional Programming techniques and tools, we were able to construct a cost-effective, semantically-aware translation tool in a fraction of the time needed by traditional methods. Based upon its performance during testing, we believe the toolto correctly translate the majority of test programs, thereby greatly easing the applications engineers' burden.

Abstract : The impact of Domain Specific Languages (DSLs) on software design is considerable. They allow programs to be more concise than equivalent programs written in a high-level programming languages. They relieve programmers from making decisions about data-structure and algorithm design, and thus allows solutions to be constructed quickly. Because DSL's are at a higher level of abstraction they are easier to maintain and reason about than equivalent programs written in a high-level language, and perhaps most importantly they can be written by domain experts rather than programmers. The problem is that DSL implementation is costly and prone to errors, and that high level approaches to DSL implementation often produce inefficient systems. By using two new programming language mechanisms, program staging and monadic abstraction, we can lower the cost of DSL implementations by allowing reuse at many levels. These mechanisms provide the expressive power that allows the construction of many compiler components as reusable libraries, provide a direct link between the semantics and the low-level implementation, and provide the structure necessary to reason about the implementation.

Abstract : Writing (meta-)programs that manipulate other (object-) programs poses significant technical problems when the object language itself has a notion of binders and variable occurrences. Higher-order abstract syntax is a representation of object programs that has recently been the focus of several studies. This paper points out a number of limitations of using higher order syntax in a functional context, and argues that DALI, a language based on a simple and elegant proposal made by Dale Miller ten years ago can provide superior support for manipulating such object-languages. Miller's original proposal, however, did not provide any formal treatment. To fill this gap, we present both a big-step and a reduction semantics for DALI, and summarize the results of our extensive study of the semantics, including the rather involved proof of the soundness of the reduction semantics with respect to the big-step semantics. Because our formal development is carried out for the untyped version of the language, we hope it will serve as a solid basis for investigating type system(s) for DALI.

The impact of Domain Specific Languages (DSLs) on software design is considerable. They allow programs to be more concise than equivalent programs written in a high-level programming languages. They relieve programmers from making decisions about data-structure and algorithm design, and thus allows solutions to be constructed quickly. Because DSL's are at a higher level of abstraction they are easier to maintain and reason about than equivalent programs written in a high-level language, and perhaps most importantly they can be written by domain experts rather than programmers. The problem is that DSL implementation is costly and prone to errors, and that high level approaches to DSL implementation often produce inefficient systems. By using two new programming language mechanisms, program staging and monadic abstraction, we can lower the cost of DSL implementations by allowing reuse at many levels. These mechanisms provide the expressive power that allows the construction of many compiler components as reusable libraries, provide a direct link between the semantics and the low-level implementation, and provide the structure necessary to reason about the implementation.

Molecular biology applications, like those of other scientific domains, need to store and view large amounts of specialized quantitative information. With the advent of high speed sequencing technology and considerable funding to "map" the genomes of key biological organisms, public databases such as GenBank, PDB, EMBL, JIPID, and SwissProt make millions of genetic sequences available to molecular biologists, and industry and university laboratories maintain large databases. The need for common interfaces and query languages to exploit these heterogeneous databases is well documented, and several such systems now exist or are under development. The authors' own work on database and program interoperability in this domain has shown, however, that providing an interface is but a first step towards making these databases fully useful. The system they are developing integrates and trades inputs and results from numerous computational biology programs. It helps researchers organize result items from sequence comparisons into "clusters" that can be marked, named, annotated, and manipulated. An alpha version is implemented in Smalltalk. The paper describes the scientific problem the system aims to solve, as well as current barriers to development and research opportunities suggested by those barriers. They present its conceptual data model, the current prototype, and future implementation plans.