scholarly journals Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages

2009 ◽  
Vol 19 (5) ◽  
pp. 509-543 ◽  
Author(s):  
JACQUES CARETTE ◽  
OLEG KISELYOV ◽  
CHUNG-CHIEH SHAN
Keyword(s):  
Partial Evaluation ◽  
Higher Order ◽  
Dependent Types ◽  
Abstract Syntax ◽  
Object Language ◽  
Data Types ◽  
Initial Algebra ◽  
The Family ◽  
De Bruijn ◽  
Algebraic Data Types

AbstractWe 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-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.

Normalization by evaluation with typed abstract syntax

2001 ◽  
Vol 11 (6) ◽  
pp. 673-680 ◽  
Author(s):  
OLIVIER DANVY ◽  
MORTEN RHIGER ◽  
KRISTOFFER H. ROSE
Keyword(s):  
Higher Order ◽  
Abstract Syntax ◽  
Object Language

In higher-order abstract syntax, the variables and bindings of an object language are represented by variables and bindings of a meta-language. Let us consider the simply typed λ-calculus as object language and Haskell as meta-language. For concreteness, we also throw in integers and addition, but only in this section.

scholarly journals Sharing analysis in the Pawns compiler

2015 ◽  
Author(s):  
Lee Naish
Keyword(s):  
Programming Language ◽  
Data Structures ◽  
Source Code ◽  
Higher Order ◽  
Declarative Programming ◽  
Data Types ◽  
Shared Data ◽  
Algebraic Data Types ◽  
Higher Order Functions

Pawns is a programming language under development which supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures which are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and postconditions concerning sharing for functions.

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

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

<p>We present a simple way to program typed abstract syntax in a <br />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.</p><p>Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.</p>

scholarly journals RS-2 Tagging, Encoding, and Jones Optimality

2003 ◽  
Vol 10 (2) ◽  
Author(s):  
Olivier Danvy ◽  
Pablo E. Martínez López
Keyword(s):  
Partial Evaluation ◽  
Higher Order ◽  
The Self ◽  
Abstract Syntax ◽  
Original Source ◽  
Simple Representation ◽  
Residual Program ◽  
Source Program

A partial evaluator is said to be Jones-optimal if the result of specializing a self-interpreter with respect to a source program is textually identical to the source program, modulo renaming. Jones optimality has already been obtained if the self-interpreter is untyped. If the self-interpreter is typed, however, residual programs are cluttered with type tags. To obtain the original source program, these tags must be removed.<br /> <br />A number of sophisticated solutions have already been proposed. We observe, however, that with a simple representation shift, ordinary partial evaluation is already Jones-optimal, modulo an encoding. The representation shift amounts to reading the type tags as constructors for higher-order abstract syntax. We substantiate our observation by considering a typed self-interpreter whose input syntax is higher-order. Specializing this interpreter with respect to a source program yields a residual program that is textually identical to the source program, modulo renaming.

scholarly journals Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing

2020 ◽  
pp. 319-338 ◽  
Author(s):  
Mathieu Huot ◽  
Sam Staton ◽  
Matthijs Vákár
Keyword(s):  
Automatic Differentiation ◽  
Higher Order ◽  
Data Types ◽  
Structure Preserving ◽  
Correctness Proofs ◽  
Unique Structure ◽  
Order Language ◽  
Algebraic Data Types ◽  
Semantic Correctness

AbstractWe present semantic correctness proofs of Automatic Differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Finally, we sketch how the analysis extends to other AD methods by considering a continuation-based method.

scholarly journals Sharing analysis in the Pawns compiler

2015 ◽  
Author(s):  
Lee Naish
Keyword(s):  
Programming Language ◽  
Data Structures ◽  
Source Code ◽  
Higher Order ◽  
Declarative Programming ◽  
Data Types ◽  
Shared Data ◽  
Algebraic Data Types ◽  
Higher Order Functions

Pawns is a programming language under development that supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures that are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and post-conditions concerning sharing for functions.

scholarly journals Sharing analysis in the Pawns compiler

2015 ◽  
Author(s):  
Lee Naish
Keyword(s):  
Programming Language ◽  
Data Structures ◽  
Source Code ◽  
Higher Order ◽  
Declarative Programming ◽  
Data Types ◽  
Shared Data ◽  
Algebraic Data Types ◽  
Higher Order Functions

Pawns is a programming language under development that supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures that are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and post-conditions concerning sharing for functions.

Sign in / Sign up

Export Citation Format

Share Document