Automatic type inference via partial evaluation. Aaron Tomb, Cormac Flanagan. PPDPâ€™05.
Type checking and type inference are fundamentally similar problems. However, the algorithms for performing the two operations, on the same type system, often differ significantly. The type checker is typically a straightforward encoding of the original type rules. For many systems, type inference is performed using a two-phase, constraint-based algorithm.We present an approach that, given the original type rules written as clauses in a logic programming language, automatically generates an efficient, two-phase, constraint-based type inference algorithm. Our approach works by partially evaluating the type checking rules with respect to the target program to yield a set of constraints suitable for input to an external constraint solver. This approach avoids the need to manually develop and verify a separate type inference algorithm, and is ideal for experimentation with and rapid prototyping of novel type systems.
Also somewhat relevant to the discussions here about type checking as abstract interpretation.
The terms pattern matching, and declartive programming come mind.
You can also think about it as an embedded DSL.
I came across Behaviour via this simple example which shows the style of programming the library leads to.
Backtracking, Interleaving, and Terminating Monad Transformers. Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman and Amr Sabry.
We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair conjunctions, conditionals, pruning, and an expressive top-level interface. Implementing these additional constructs is well-known in models of backtracking based on streams, but not known to be possible in continuation-based models. We show that all these additional constructs can be generically and monadically realized using a single primitive which we call msplit. We present two implementations of the library: one using success and failure continuations; and the other using control operators for manipulating delimited continuations.
As you can expect from the author list, this is cool stuff. Enjoy!
A type discipline for authorization policies. Cedric Fournet; Andrew D. Gordon; Sergio Maffeis
Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner. For a given authorization policy, we consider the problem of checking whether a cryptographic implementation complies with the policy. We formalize authorization policies by embedding logical predicates and queries within a spi-calculus. This embedding is new, simple, and general; it allows us to treat logic programs as specifications of code using secure channels, cryptography, or a combination. Moreover, we propose a new dependent type system for verifying such implementations against their policies. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.
I guess it's dependent types day around here...
We present a framework called Semantic Streams that allows users to pose declarative queries over semantic interpretations of sensor data. For example, instead of querying raw sensor data, the user can query vehicle speeds; the system decides which sensor data and which operations to use to infer the vehicle speeds. The user can also place constraints on values such as the confidence with which the speed was measured or the amount of energy consumed to measure the speeds. This framework is designed to work in a shared sensor infrastructure, where multiple queries may coexist for extended periods of time, instead of a hand-designed, single purpose sensor network. We propose a semantic service programming model and describe a service description language and a query processor that support the programming model. We demonstrate how this system can be used with a network of video, magnetometer, and infrared break beam sensors deployed in a parking garage.
The declarative framework is based on Prolog and CLP(R) and implemented using SICStus Prolog.
Starlog is a pure-logic programming language designed to overcome some of the problems inherient in traditional approaches to logic programming.
Starlog was designed as an alternative approach to programming in pure logic. Many of the failings of other logic programming languages can be overcome using the bottom-up evaluation technique. Bottom-up evaluation avoids problems associated with cyclic relations, and allows side-effects to be performed without compromising the declarative semantics of a program.
Using Starlog we advocate a data structure free programming style. That is, predicates in Starlog programs do not contain compound terms for their arguments. This greatly simplifies logic programs and their implementations, lowers the learning curve for new programmers, and forces the programmer to think of all program constructs as relations.
A Tutorial on Proof Theoretic Foundations of Logic Programming. Paola Bruscoli and Alessio Guglielmi. ICLP'03.
I just glanced through this tutorial, but since I know quite a few LtU readers are into proof theory, I thought I'd share the link.
More from Michael Rys.
Rys lists several advantages of declarative languages, some of which apply to functional languages in general.
It seems I've become the editor responsible for XML related links around here lately, even though we have on board editors who are much more qualified for this than I am ;-).
Peter linked to the MOZ 2004 papers earlier.
This presentation by Raphael Collet provides a nice example of constraint programming, a paradigm we don't discuss often enough.
Experiments from Graham Klyne:
Active forum topics
New forum topics