This document formally specifies the semantics of local modules and packages - dynamically typed modules that are first-class values - as an extension to the functional programming language Standard ML. The language thus defined is a substantial subset of a larger extension of Standard ML, a language known as Alice ML. Packages are the central feature of Alice ML that enables support for typed open programming.
In many problems that require extensive searching, the solution can be described as satisfying two competing constraints, where satisfying each independently does not pose a challenge. As an alternative to tree-based and stochastic searching, for these problems we propose using an iterated map built from the projections to the two constraint sets. Algorithms of this kind have been the method of choice in a large variety of signal-processing applications; we show here that the scope of these algorithms is surprisingly broad, with applications as diverse as protein folding and Sudoku.Our survey of applications shows the difference map algorithm often achieves results comparable to much more sophisticated, special purpose algorithms. Efficient implementations of constraint projections usually are easier than designing the linear program solver at the heart of many optimization algorithms.
Tim Sheard, Zine-el-abidine Benaissa, and Emir Pasalic * Introduction * Staging in MetaML * Monads in Langauge Design * Monads in METAML * Illustrating our compiler development method o The while-language o The structure of the solution o Step 1: monadic interpreter o Step 2: staged interpreter + Interpreter for Commands. + An example. * Step 3: Back-end translation and intermediate code optimization o Intensional analysis of code fragments
we develop an approach for reconciling open programming -- the development of programs that support dynamic exchange of higher-order values with strong static typing. conventional functional language extended with a set of orthogonal features like higher-order modules, dynamic type checking, higher-order serialisation, and concurrency. On top of these a flexible system of dynamic components and a simple but expressive notion of distribution is realised. The central concept in this design is the packag}, a first-class value embedding a module along with its interface type. formal model for abstract types that is not invalidated by the presence of primitives for dynamic type inspection, as is the case for the standard model based on existential quantification. For that we present an idealised language in form of an extended lambda-calculus, which can express dynamic generation of types.
Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence.
The need for flexible forms of serialisation arises under many circumstances, e.g. for doing high-level inter-process communication or to achieve persistence. Many languages, including variants of ML, thus offer pickling as a system service, but usually in a both unsafe and inexpressive manner, so that its use is discouraged. In contrast, safe generic pickling plays a central role in the design and implementation of Alice ML: components are defined as pickles, and modules can be exchanged between processes using pickling. For that purpose, pickling has to be higher-order and typed (HOT), i.e. embrace code mobility and involve runtime type checks for safety. We show how HOT pickling can be realised with a modular architecture consisting of multiple abstraction layers for separating concerns, and how both language and implementation benefit from a design consistently based on pickling.
We introduce a new lambda calculus with futures, Lambda(fut), that models the operational semantics of concurrent statically typed functional programming languages with mixed eager and lazy threads such as Alice ML, a concurrent extension of Standard ML. Lambda(fut) is a minimalist extension of the call-by-value lambda-calculus that is sufficiently expressive to define and combine a variety of standard concurrency abstractions, such as channels, semaphores, and ports. Despite its minimality, the basic machinery of Lambda(fut) is sufficiently powerful to support explicit recursion and call-by-need evaluation. We present a static type system for Lambda(fut) and distinguish a fragment of Lambda(fut) that we prove to be uniformly confluent. This result confirms our intuition that reference cells are the sole source of indeterminism.
Despite its powerful module system, ML has not yet evolved for the modern world of dynamic and open modular programming, to which more primitive languages have adapted better so far. We present the design and semantics of a simple yet expressive first-class component system for ML. It provides dynamic linking in a type-safe and type-flexible manner, and allows selective execution in sandboxes. The system is defined solely by reduction to higher-order modules plus an extension with simple module-level dynamics, which we call packages. To represent components outside processes we employ generic pickling. We give a module calculus formalising the semantics of packages and pickling.
ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into separately compilable, mutually recursive components. Mixin modules facilitate recursive linking of separately compiled components, but they are not hierarchically composable and typically do not support type abstraction. We synthesize the complementary advantages of these two mechanisms in MixML. A MixML module is like an ML structure with some components specified but not defined unifing the ML structure and signature languages into one. MixML seamlessly integrates hierarchical composition, translucent MLstyle data abstraction, and mixin-style recursive linking.Tthe design of MixML is minimalist emphasizing how all the interesting features of the ML module system can be understood simply as stylized uses of a small set of orthogonal underlying constructs, with mixin composition playing a central role.
A Tutorial Implementation of a Dependently Typed Lambda Calculus Andres Löh, Conor McBride and Wouter Swierstra We present the type rules for a dependently-typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently-typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The paper is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe. Download Draft Paper (submitted to FI) Haskell source code (executable Haskell file containing all the code from the paper plus the interpreter; automatically generated from the paper sources) prelude.lp (prelude for the LambdaPi interpreter, containing several example programs) Instructions (how to get started with the LambdaPi interpreter)
Daniel Fridlender Mia Indrika March 2001 Inspired by Danvy, we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general definition of zipWith for which the Haskell library provides a family of functions, each member of the family having a different type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in lambda-calculus
Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without manual annotation. We have implemented liquid type inference in Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the Ocaml program.We describe experiments using Dsolve to statically verify the safety of array accesses on a set of Ocaml benchmarks that were previously annotated as part of the DML project. When used with a simple set of bounds checking qualifiers, Dsolve reduces manual annotation required from 31% of program text to under 1%.
Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system. Code accompanying the paper has been developed into an Agda library AoPA.
Dependent type systems, in which types can depend on values, admit detailed specifications of function behavior and data invariants. Programming languages based on System F do not have dependent types, and are therefore more limited in what structure or function invariants can be encoded in the type system. In this paper, we show how guarded algebraic datatypes can simulate dependent types. We formalize additions to a guarded-datatypes-enhanced System F that allow types to depend on values and discuss the programming style that results, which is similar to theorem proving. Our technique can be applied to multiple existing programming languages, including Haskell and C#. We also introduce an idiom for eliminating any execution cost from programming with simulated dependent types. We have developed a tool to automatically produce the boilerplate necessary for the simulation, and we have used it to enforce data structure invariants and to allow elision of run-time bounds checks.
S Peyton Jones, D Vytiniotis, S Weirich, and G Washburn, ICFP 2006, pp50-61 Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. Our contribution is to show how to exploit programmer-supplied type annotations to make the type inference task almost embarrassingly easy. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms. [This is a version of Wobbly types: type inference for generalised algebraic data types. Relative to ICFP 2006, the PDF above also describes a simplification to the type system, at the cost of extra annotation burden. This simpler system is the one actually implemented in GHC 6.8]
popl2008 ** 1. GADTs are syntactic sugar. The real structures at work are existentially quantified types and the equality GADT. 2. Indexing by a set, rather than a category, as GADTs do means that really this is dependently typed programming faked in Haskell by using kind level proxies for types 3. As a result, Haskell ends up with a curious "logic programming" feel to its type level computation and functional programming feel to its term-level computation. PJohann and NGhani ** his main point (which worked with me) is that we should pay more attention Kan extensions. We already know and love (strong) functors, (co)monads, adjunctions and the Yoneda lemma.
One of the key goals of rewriting logic from its beginning has been to provide a semantic and logical framework in which many models of computation and languages can be naturally represented. There is by now very extensive evidence supporting the claim that rewriting logic is indeed a very flexible and simple logical and semantic framework. From a language design point of view the obvious question to ask is: how can a rewriting logic language best support logical and semantic framework applications, so that it becomes a metalanguage in which a very wide variety of logics and languages can be both semantically defined, and implemented? Our answer is: by being reflective. This paper discusses our latest language design and implementation work on Maude as a reflective metalanguage in which entire environments---including syntax definition, parsing, pretty printing, execution, and input/output---can be defined for a language or logic L of choice.
Keeping two or more copies of the same document synchronized with each other in real-time is a complex challenge. This paper describes the differential synchronization algorithm. Differential synchronization offers scalability, fault-tolerance, and responsive collaborative editing across an unreliable network. 1 Conventional Strategies The three most common approaches to synchronization are ownership, event passing and three-way merges. These methods are conceptually simple, but all have drawbacks. link to googletalk video and mobWrite sw
Review of Modern Physics 1986 The interpretational problems of quantum mechanics are considered. The way in which the standard Copenhagen Interpretation (CI) of quantum mechanics deals with these problems is reviewed. A new interpretation of the formalism of quantum mechanics, the Transactional Interpretation (TI), is presented. The basic element of TI is the transaction describing a quantum event as an exchange of advanced and retarded waves, as implied by the work of Wheeler and Feynman, Dirac, and others. The TI is explicitly nonlocal and thereby consistent with recent tests of the Bell Inequality, yet is relativistically invariant and fully causal. A detailed comparison of the TI and CI is made in the context of well known quantum mechanical gedanken experiments and "paradoxes". The TI permits quantum mechanical wave functions to be interpreted as real waves physically present in space rather than as "mathematical representations of knowledge" as in the CI.