FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell

2005 ◽  
Vol 16 (1) ◽  
pp. 21-34 ◽  
Author(s):  
MARTIN ERWIG ◽  
STEVE KOLLMANSBERGER
Keyword(s):  
Functional Programming ◽  
Data Type ◽  
A Value ◽  
Probabilistic Values

At the heart of functional programming rests the principle of referential transparency, which in particular means that a function f applied to a value x always yields one and the same value y=f(x). This principle seems to be violated when contemplating the use of functions to describe probabilistic events, such as rolling a die: It is not clear at all what exactly the outcome will be, and neither is it guaranteed that the same value will be produced repeatedly. However, these two seemingly incompatible notions can be reconciled if probabilistic values are encapsulated in a data type.

Encapsulating non-determinacy in an abstract data type with determinate semantics

1991 ◽  
Vol 1 (1) ◽  
pp. 3-20 ◽  
Author(s):  
F. Warren Burton
Keyword(s):  
Parallel Algorithms ◽  
Programming Language ◽  
Functional Programming ◽  
Data Type ◽  
Parallel Program ◽  
Abstract Data Type ◽  
Functional Programming Language ◽  
Abstract Data

AbstractA parallel program may be indeterminate so that it can adapt its behavior to the number of processors available.Indeterminate programs are hard to write, understand, modify or verify. They are impossible to debug, since they may not behave the same from one run to the next.We propose a new construct, a polymorphic abstract data type called an improving value, with operations that have indeterminate behavior but simple determinate semantics. These operations allow the type of indeterminate behavior required by many parallel algorithms.We define improving values in the context of a functional programming language, but the technique can be used in procedural programs as well.

scholarly journals Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins

2013 ◽  
Vol 23 (5) ◽  
pp. 515-551 ◽  
Author(s):  
JANIS VOIGTLÄNDER ◽  
ZHENJIANG HU ◽  
KAZUTAKA MATSUDA ◽  
MENG WANG
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Data Type ◽  
Good Effect ◽  
Original Source ◽  
International Conference ◽  
Consistency Conditions ◽  
Update Propagation ◽  
Propagation Function ◽  
Function Mapping

AbstractMatsuda et al. (Matsuda, K., Hu, Z., Nakano, K., Hamana, M. & Takeichi, M. (2007) Bidirectionalization transformation based on automatic derivation of view complement functions. In Proceedings of the International Conference on Functional Programming. ACM Press, pp. 47–58) and Voigtländer (Voigtländer, J. (2009) Bidirectionalization for free! In Proceedings of Principles of Programming Languages. ACM Press, pp. 165–176) have introduced two techniques that given a source-to-view function provide an update propagation function mapping an original source and an updated view back to an updated source, subject to standard consistency conditions. Previously, we developed a synthesis of the two techniques, based on a separation of shape and content aspects (Voigtländer, J., Hu, Z., Matsuda, K. & Wang, M. (2010) Combining syntactic and semantic bidirectionalization. In Proceedings of the International Conference on Functional Programming. ACM Press, pp. 181–192). Here we carry that idea further, reworking the technique of Voigtländer such that any shape bidirectionalizer (based on the work of Matsuda et al. (2007) or not) can be used as a plug-in, to good effect. We also provide a data-type-generic account, enabling wider reuse, including the use of pluggable bidirectionalization itself as a plug-in.

scholarly journals GhostCell: separating permissions from data in Rust

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Joshua Yanovski ◽  
Hoang-Hai Dang ◽  
Ralf Jung ◽  
Derek Dreyer
Keyword(s):  
Data Structures ◽  
Functional Programming ◽  
Dependent Types ◽  
A Value ◽  
State Dependent ◽  
Representative Subset ◽  
Rank 2 ◽  
Systems Programming ◽  
Linked Lists

The Rust language offers a promising approach to safe systems programming based on the principle of aliasing XOR mutability : a value may be either aliased or mutable, but not both at the same time. However, to implement pointer-based data structures with internal sharing, such as graphs or doubly-linked lists, we need to be able to mutate aliased state. To support such data structures, Rust provides a number of APIs that offer so-called interior mutability : the ability to mutate data via method calls on a shared reference. Unfortunately, the existing APIs sacrifice flexibility, concurrent access, and/or performance, in exchange for safety. In this paper, we propose a new Rust API called GhostCell which avoids such sacrifices by separating permissions from data : it enables the user to safely synchronize access to a collection of data via a single permission. GhostCell repurposes an old trick from typed functional programming: branded types (as exemplified by Haskell’s ST monad), which combine phantom types and rank-2 polymorphism to simulate a lightweight form of state-dependent types. We have formally proven the soundness of GhostCell by adapting and extending RustBelt, a semantic soundness proof for a representative subset of Rust, mechanized in Coq.

Improving intervals

1993 ◽  
Vol 3 (2) ◽  
pp. 153-169
Author(s):  
W. Ken Jackson ◽  
F. Warren Burton
Keyword(s):  
Lower Bounds ◽  
Branch And Bound ◽  
Data Type ◽  
Parallel Program ◽  
Upper And Lower Bounds ◽  
A Value ◽  
Parallel Branch And Bound ◽  
Simple Implementation ◽  
Alpha Beta

AbstractWe show how improving values (Burton, 1991) can be extended to handle both upper and lower bounds. The result is a new data type, called improving intervals. We give a simple implementation of improving intervals that uses a list of successively tighter bounds to represent a value. A program using improving intervals can be evaluated as a parallel program using speculative evaluation. The utility of improving intervals is demonstrated through two programs: parallel alpha-beta and parallel branch-and-bound

Containers, monads and induction recursion

2014 ◽  
Vol 26 (1) ◽  
pp. 89-113 ◽  
Author(s):  
NEIL GHANI ◽  
PETER HANCOCK
Keyword(s):  
Programming Language ◽  
Algebraic Structure ◽  
Functional Programming ◽  
Type System ◽  
Pivotal Role ◽  
A Value ◽  
Structural Recursion ◽  
Definition Of ◽  
High Level ◽  
Original Type

Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a setUofcodesand a decoding functionT : U → Dwhich assigns to every codeu : U, a valueT, uof some typeD, e.g.the large type Set of small types or sets. The name induction recursion refers to the build-up of codes inUusing inductive clauses, simultaneously with the definition of the functionT, by structural recursion on codes.Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation – in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.

Observations of the Thermal Decomposition of Brucite

1968 ◽  
Vol 26 ◽  
pp. 446-447
Author(s):  
P. L. Burnett ◽  
W. R. Mitchell ◽  
C. L. Houck
Keyword(s):  
Thermal Decomposition ◽  
Magnesium Oxide ◽  
Basal Plane ◽  
Magnesium Ions ◽  
A Value ◽  
Reaction Proceeds

Natural Brucite (Mg(OH)2) decomposes on heating to form magnesium oxide (MgO) having its cubic ﹛110﹜ and ﹛111﹜ planes respectively parallel to the prism and basal planes of the hexagonal brucite lattice. Although the crystal-lographic relation between the parent brucite crystal and the resulting mag-nesium oxide crystallites is well known, the exact mechanism by which the reaction proceeds is still a matter of controversy. Goodman described the decomposition as an initial shrinkage in the brucite basal plane allowing magnesium ions to shift their original sites to the required magnesium oxide positions followed by a collapse of the planes along the original <0001> direction of the brucite crystal. He noted that the (110) diffraction spots of brucite immediately shifted to the positions required for the (220) reflections of magnesium oxide. Gordon observed separate diffraction spots for the (110) brucite and (220) magnesium oxide planes. The positions of the (110) and (100) brucite never changed but only diminished in intensity while the (220) planes of magnesium shifted from a value larger than the listed ASTM d spacing to the predicted value as the decomposition progressed.

Field-assisted ionization theory for microscopists

1994 ◽  
Vol 52 ◽  
pp. 820-821
Author(s):  
Patrick P. Camus
Keyword(s):  
Electric Field ◽  
Electron Tunneling ◽  
Ionization Probability ◽  
Critical Distance ◽  
Tunneling Probability ◽  
Field Ionization ◽  
Radius Of Curvature ◽  
Field Evaporation ◽  
A Value ◽  
Ion Emission

The theory of field ion emission is the study of electron tunneling probability enhanced by the application of a high electric field. At subnanometer distances and kilovolt potentials, the probability of tunneling of electrons increases markedly. Field ionization of gas atoms produce atomic resolution images of the surface of the specimen, while field evaporation of surface atoms sections the specimen. Details of emission theory may be found in monographs.Field ionization (FI) is the phenomena whereby an electric field assists in the ionization of gas atoms via tunneling. The tunneling probability is a maximum at a critical distance above the surface,xc, Fig. 1. Energy is required to ionize the gas atom at xc, I, but at a value reduced by the appliedelectric field, xcFe, while energy is recovered by placing the electron in the specimen, φ. The highest ionization probability occurs for those regions on the specimen that have the highest local electric field. Those atoms which protrude from the average surfacehave the smallest radius of curvature, the highest field and therefore produce the highest ionizationprobability and brightest spots on the imaging screen, Fig. 2. This technique is called field ion microscopy (FIM).

Vitamin A Value of Plant Food Provitamin A - Evaluated by the Stable Isotope Technologies

2014 ◽  
Vol 84 (Supplement 1) ◽  
pp. 25-29 ◽  
Author(s):  
Guangwen Tang
Keyword(s):  
Stable Isotope ◽  
Vitamin A ◽  
Provitamin A ◽  
Animal Origin ◽  
Plant Food ◽  
Plant Foods ◽  
A Value ◽  
Provitamin A Carotenoids ◽  
Β Carotene

Humans need vitamin A and obtain essential vitamin A by conversion of plant foods rich in provitamin A and/or absorption of preformed vitamin A from foods of animal origin. The determination of the vitamin A value of plant foods rich in provitamin A is important but has challenges. The aim of this paper is to review the progress over last 80 years following the discovery on the conversion of β-carotene to vitamin A and the various techniques including stable isotope technologies that have been developed to determine vitamin A values of plant provitamin A (mainly β-carotene). These include applications from using radioactive β-carotene and vitamin A, depletion-repletion with vitamin A and β-carotene, and measuring postprandial chylomicron fractions after feeding a β-carotene rich diet, to using stable isotopes as tracers to follow the absorption and conversion of plant food provitamin A carotenoids (mainly β-carotene) in humans. These approaches have greatly promoted our understanding of the absorption and conversion of β-carotene to vitamin A. Stable isotope labeled plant foods are useful for determining the overall bioavailability of provitamin A carotenoids from specific foods. Locally obtained plant foods can provide vitamin A and prevent deficiency of vitamin A, a remaining worldwide concern.

Sign in / Sign up

Export Citation Format

Share Document