Compiling untyped lambda calculus to lower-level code by game semantics and partial evaluation (invited paper)

AbstractThis article describes theoretical and practical aspects of an implemented self-applicable partial evaluator for the untyped lambda-calculus with constants and a fixed point operator. To the best of our knowledge, it is the first partial evaluator that is simultaneously higher-order, non-trivial, and self-applicable.Partial evaluation produces aresidual programfrom a source program and some of its input data. When given the remaining input data the residual program yields the same result that the source program would when given all its input data. Our partial evaluator produces a residual lambda-expression given a source lambda-expression and the values of some of its free variables. By self-application, the partial evaluator can be used to compile and to generate stand-alone compilers from a denotational or interpretive specification of a programming language.An essential component in our self-applicable partial evaluator is the use of explicitbinding time information.We use this to annotate the source program, marking asresidualthe parts for which residual code is to be generated and marking aseliminablethe parts that can be evaluated using only the data that is known during partial evaluation. We give a simple criterion,well-annotatedness,that can be used to check that the partial evaluator can handle the annotated higher-order programs without committing errors.Our partial evaluator is simple, is implemented in a side-effect free subset of Scheme, and has been used to compile and to generate compilers and a compiler generator. In this article we examine two machine-generated compilers and find that their structures are surprisingly natural.

Download Full-text

Normalization by Evaluation with Typed Abstract Syntax

BRICS Report Series ◽

10.7146/brics.v8i16.20473 ◽

2001 ◽

Vol 8 (16) ◽

Author(s):

Olivier Danvy ◽

Morten Rhiger ◽

Kristoffer H. Rose

Keyword(s):

Normal Forms ◽

Partial Evaluation ◽

Lambda Calculus ◽

Abstract Syntax ◽

Type Checking

We present a simple way to implement typed abstract syntax for the lambda calculus in Haskell, using phantom types, and we specify normalization by evaluation (i.e., type-directed partial evaluation) to yield this typed abstract syntax. Proving that normalization by evaluation preserves types and yields normal forms then reduces to type-checking the specification.

Download Full-text

A Symmetric Approach to Compilation and Decompilation

BRICS Report Series ◽

10.7146/brics.v9i37.21752 ◽

2002 ◽

Vol 9 (37) ◽

Cited By ~ 1

Author(s):

Mads Sig Ager ◽

Olivier Danvy ◽

Mayer Goldberg

Keyword(s):

Partial Evaluation ◽

Lambda Calculus ◽

Target Language ◽

Machine Language ◽

Left Inverse ◽

Source Language ◽

Secd Machine ◽

Arithmetic Expressions

Just as specializing a source interpreter can achieve compilation from a source language to a target language, we observe that specializing a target interpreter can achieve compilation from the target language to the source language. In both cases, the key issue is the choice of whether to perform an evaluation or to emit code that represents this evaluation. We substantiate this observation by specializing two source interpreters and two target interpreters. We first consider a source language of arithmetic expressions and a target language for a stack machine, and then the lambda-calculus and the SECD-machine language. In each case, we prove that the target-to-source compiler is a left inverse of the source-to-target compiler, i.e., it is a decompiler. In the context of partial evaluation, compilation by source-interpreter specialization is classically referred to as a Futamura projection. By symmetry, it seems logical to refer to decompilation by target-interpreter specialization as a Futamura embedding.

Download Full-text

A Temporal-Logic Approach to Binding-Time Analysis

BRICS Report Series ◽

10.7146/brics.v2i51.19952 ◽

1995 ◽

Vol 2 (51) ◽

Author(s):

Rowan Davies

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Partial Evaluation ◽

Lambda Calculus ◽

Time Analysis ◽

Typed Lambda Calculus ◽

Binding Time ◽

Logic Approach ◽

Multi Level ◽

Binding Time Analysis

The Curry-Howard isomorphism identifies proofs with typed lambda- calculus terms, and correspondingly identifies propositions with types. We show how this isomorphism can be extended to relate constructive temporal logic with binding-time analysis. In particular, we show how to extend the Curry-Howard isomorphism to include the ("next") operator from linear-time temporal logic. This yields the simply typed lambda-calculus which we prove to be equivalent to a multi-level binding-time analysis like those used in partial evaluation. Keywords: Curry-Howard isomorphism, partial evaluation, binding-time analysis, temporal logic.

Download Full-text

Eta-Expansion Does The Trick

BRICS Report Series ◽

10.7146/brics.v2i41.21673 ◽

1995 ◽

Vol 2 (41) ◽

Cited By ~ 1

Author(s):

Olivier Danvy ◽

Karoline Malmkjær ◽

Jens Palsberg

Keyword(s):

Partial Evaluation ◽

Lambda Calculus ◽

Product Type ◽

Proper Treatment ◽

Time Analysis ◽

Function Type ◽

Dynamic Case ◽

Unified View ◽

Binding Time ◽

Binding Time Analysis

Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such "binding-time improvements'': non-standard use of continuation-passing style, eta-expansion, and a popular transformation called "The Trick''. We provide a unified view of these binding-time improvements, from a typing perspective. Just as a proper treatment of product values in partial evaluation requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the non-standard use of continuation-passing style encountered in partial evaluation. In this setting, eta-expansion acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it achieves "The Trick''. In this paper, we extend Gomard and Jones's partial evaluator for the lambda-calculus, lambda-Mix, with products and disjoint sums; we point out how eta-expansion for disjoint sums does The Trick; we generalize our earlier work by identifying that eta-expansion can be obtained in the binding-time analysis simply by adding two coercion rules; and we specify and prove the correctness of our extension to lambda-Mix. See revised version BRICS-RS-96-17.

Download Full-text

Type-Directed Partial Evaluation

DAIMI Report Series ◽

10.7146/dpb.v24i494.7022 ◽

1995 ◽

Vol 24 (494) ◽

Author(s):

Olivier Danvy

Keyword(s):

Programming Languages ◽

Code Generation ◽

Compiler Optimization ◽

Partial Evaluation ◽

Lambda Calculus ◽

Denotational Semantics ◽

Compiler Generation ◽

Environment Type ◽

Symbolic Evaluation ◽

Specialized Program

We present a strikingly simple partial evaluator, that is type-directed and reifies a compiled program into the text of a residual, specialized program. Our partial evaluator is concise (a few lines) and it handles the flagship examples of offline monovariant partial evaluation. Its source programs are constrained in two ways: they must be closed and monomorphically typable. Thus dynamic free variables need to be factored out in a ``dynamic initial environment´´. Type-directed partial evaluation uses no symbolic evaluation for specialization, and naturally processes static computational effects.Our partial evaluator is the part of an offline partial evaluator that residualizes static values in dynamic contexts. Its restriction to the simply typed lambda-calculus coincides with Berger and Schwichtenberg's ``inverse of the evaluation functional´´ (LICS'91), which is an instance of normalization in a logical setting. As such, type-directed partial evaluation essentially achieves lambda-calculus normalization. We extend it to produce specialized programs that are recursive and that use disjoint sums and computational effects. We also analyze its limitations: foremost, it does not handle inductive types.This paper therefore bridges partial evaluation and lambda-calculus normalization through higher-order abstract syntax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler optimization, and run-time code generation (including decompilation). It also offers a simple solution to denotational semantics-based compilation and compiler generation.Proceedings of POPL96, the 1996 ACM Symposium on Principles of Programming Languages (to appear).

Download Full-text

Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

ACM SIGPLAN Notices ◽

10.1145/982962.964007 ◽

2004 ◽

Vol 39 (1) ◽

pp. 64-76 ◽

Cited By ~ 4

Author(s):

Vincent Balat ◽

Roberto Di Cosmo ◽

Marcelo Fiore

Keyword(s):

Partial Evaluation ◽

Lambda Calculus ◽

Typed Lambda Calculus

Download Full-text

A Simple Take on Typed Abstract Syntax in Haskell-like Languages

BRICS Report Series ◽

10.7146/brics.v7i34.20169 ◽

2000 ◽

Vol 7 (34) ◽

Author(s):

Olivier Danvy ◽

Morten Rhiger

Keyword(s):

Normal Forms ◽

Partial Evaluation ◽

Lambda Calculus ◽

Higher Order ◽

Abstract Syntax ◽

Typed Lambda Calculus

We present a simple way to program typed abstract syntax in a language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms.Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.

Download Full-text