This paper explores the use monads to structure functional programs. No prior knowledge of monads or category theory is required. Monads increase the ease with which programs may be modified. They can mimic the effect...
详细信息
ISBN:
(纸本)0897914538
This paper explores the use monads to structure functional programs. No prior knowledge of monads or category theory is required. Monads increase the ease with which programs may be modified. They can mimic the effect of impure features such as exceptions, state, and continuations;and also provide effects not easily achieved with such features. The types of a program reflect which effects occur. The first section is an extended example of the use of monads. A simple interpreter is modified to support various extra features: error messages, state, output, and non-deterministic choice. The second section describes the relation between monads and continuation-passing style. The third section sketches how monads are used in a compiler for Haskell that is written in Haskell.
This paper presents program analyses and transformations that discover a general class of auxiliary information for any incremental computation problem. Combining these techniques with previous techniques for caching ...
详细信息
ISBN:
(纸本)9780897917698
This paper presents program analyses and transformations that discover a general class of auxiliary information for any incremental computation problem. Combining these techniques with previous techniques for caching intermediate results, we obtain a systematic approach that transforms non-incremental programs into efficient incremental programs that use and maintain useful auxiliary information as well as useful intermediate results. The use of auxiliary information allows us to achieve a greater degree of incrementality than otherwise possible. Applications of the approach include strength reduction in optimizing compilers and finite differencing in transformational programming.
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 th...
详细信息
ISBN:
(纸本)9780897917698
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 *** 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 *** paper therefore bridges partial evaluation and ¿-calculus normalization through higher-order abstract syntax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler optimization, and rut-time code generation (including decompilation). It also offers a simple solution to denotational semantics-based compilation and compiler generation.
We present a new framework for transforming data representations in a strongly typed intermediate language. Our method allows both value producers (sources) and value consumers (sinks) to support multiple representati...
详细信息
We present a new framework for transforming data representations in a strongly typed intermediate language. Our method allows both value producers (sources) and value consumers (sinks) to support multiple representations, automatically inserting any required code. Specialized representations can be easily chosen for particular source/sink pairs. The framework is based on these techniques: 1. Flow annotated types encode the `flows-from' (source) and `flows-to' (sink) information of a flow graph. 2. Intersection and union types support (a) encoding precise flow information, (b) separating flow information so that transformations can be well typed, (c) automatically reorganizing flow paths to enable multiple representations. As an instance of our framework, we provide a function representation transformation that encompasses both closure conversion and inlining. Our framework is adaptable to data other than functions.
The algorithms for synthesis onto programmable gate arrays (PGAs) have so far addressed only the combinational logic problem. We present two algorithms for mapping a sequential circuit onto a specific table look up ar...
详细信息
ISBN:
(纸本)0818628456
The algorithms for synthesis onto programmable gate arrays (PGAs) have so far addressed only the combinational logic problem. We present two algorithms for mapping a sequential circuit onto a specific table look up architecture, namely the Xilinx 3090 architecture. In the first algorithm, we map combinational and sequential elements simultaneously. In the second, combinational elements are mapped first, followed by the sequential elements. We heavily use the combinational synthesis techniques to solve the sequential synthesis problem.
In this paper, we present a new transformation algorithm called distillation which can automatically transform higher-order functional programs into equivalent tail-recursive programs. Using this algorithm, it is poss...
详细信息
We revisit the work of Paterson and of Meijer & Hutton, which describes how to construct catamorphisms for recursive datatype definitions that embed contravariant occurrences of the type being defined. Their const...
详细信息
We revisit the work of Paterson and of Meijer & Hutton, which describes how to construct catamorphisms for recursive datatype definitions that embed contravariant occurrences of the type being defined. Their construction requires, for each catamorphism, the definition of an anamorphism that has an inverse-like relationship to that catamorphism. We present an alternative construction, which replaces the stringent requirement that an inverse anamorphism be defined for each catamorphism with a more lenient restriction. The resulting construction has a more efficient implementation than that of Paterson, Meijer, and Hutton and the relevant restriction can be enforced by a Hindley-Milner type inference algorithm. We provide numerous examples illustrating our method.
Starting from a denotational semantics of the eager untyped lambda-calculus with explicit runtime errors, the standard collecting semantics is defined as specifying the strongest program properties. By a first abstrac...
详细信息
ISBN:
(纸本)9780897918534
Starting from a denotational semantics of the eager untyped lambda-calculus with explicit runtime errors, the standard collecting semantics is defined as specifying the strongest program properties. By a first abstraction, a new sound type collecting semantics is derived in compositional fix-point form. Then by successive (semi-dual) Galois connection based abstractions, type systems and/or type inference algorithms are designed as abstract semantics or abstract interpreters approximating the type collecting semantics. This leads to a hierarchy of type systems, which is part of the lattice of abstract interpretations of the untyped lambda-calculus. This hierarchy includes two new a la Church/Curry polytype systems. Abstractions of this polytype semantics lead to classical Milner/Mycroft and Damas/-Milner polymorphic type schemes, Church/Curry monotypes and Hindley principal typing algorithm. This shows that types are abstract interpretations.
F≤ is a typed λ-calculus with subtyping and bounded second-order polymorphism. First proposed by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping. Curien and Ghelli ...
详细信息
ISBN:
(纸本)0897914538
F≤ is a typed λ-calculus with subtyping and bounded second-order polymorphism. First proposed by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping. Curien and Ghelli proved the partial correctness of a recursive procedure for computing minimal types of F≤ terms and showed that the termination of this procedure is equivalent to the termination of its major component, a procedure for checking the subtype relation between F≤ types. This procedure was thought to terminate on all inputs, but the discovery of a subtle bug in a purported proof of this claim recently reopened the question of the decidability of subtyping, and hence of typechecking. This question is settled here in the negative, using a reduction from the halting problem for two-counter Turing machines to show that the subtype relation of F≤ is undecidable.
Under a species-level abstraction of classical evolutionary programming, the standard tournament selection model is not appropriate. When viewed in this manner, it is more appropriate to consider two modes of life his...
详细信息
ISBN:
(纸本)0780363752
Under a species-level abstraction of classical evolutionary programming, the standard tournament selection model is not appropriate. When viewed in this manner, it is more appropriate to consider two modes of life histories: background evolution and extinction. The utility of this approach as an optimization procedure is evaluated on a series of test functions relative to the performance of classical evolutionary programming and fast evolutionary programming. The results indicate that on some smooth, convex landscapes and over noisy, highly multimodal landscapes, extinction evolutionary programming can outperform classical and fast evolutionary programming. On other landscapes, however, extinction evolutionary programming performs considerably worse than classical and fast evolutionary programming. Potential reasons for this variability in performance are indicated.
暂无评论