We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is instantiated in a precise fashion that permits decidable verification. We show how reflection allows the user to write equational proofs of programs just by writing other programs, e.g. using pattern-matching and recursion to perform case-splitting and induction. Thus, via, the propositions-as-types principle we show that reflection permits the specification of arbitrary functional correctness properties. While equational proofs are elegant, writing them out can be exhausting. % Our third contribution is a new We introduce a proof-search algorithm called Proof by Logical Evaluation that uses techniques from model checking & abstract interpretation, to completely automate equational reasoning. We have implemented reflection in Liquid Haskell and used it to verify that the widely used instances of the Monoid, Applicative, Functor, and Monad typeclasses actually satisfy key algebraic laws required to make the clients safe, and to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.
There are two styles of lazy evaluation, one (called `odd') that is easy to encode in the traditional `delay' and `force' syntax, but forces too much evaluation, and another (called `even') that delays evaluation as in traditional lazy languages, but is harder to encode. This note presents a new `lazy' syntax, and shows how the even style is easy to encode in this syntax, while the odd style is harder to encode. The new `lazy' syntax is defined by translation into the `delay-force' syntax. Comparisons are drawn with two other syntaxes, one used in CAML and one proposed by Chris Okasaki.
John Hughes has made pretty-printers one of the prime demonstrations of using combinators to develop a library, and algebra to implement it. This note presents a new design for pretty printers which improves on Hughes's classic design. The new design is based on a single concatenation operator which is associative and has a left and right unit. Hughes's design requires two separate operators for concatenation, where horizontal concatenation has a right unit but no left unit, and vertical concatenation has neither unit.
Pattern matching and data abstraction are important concepts in designing programs, but they do not fit well together. Pattern matching depends on making public a free data type representation, while data abstraction depends on hiding the representation. This paper proposes the views mechanism as a means of reconciling this conflict. A view allows any type to be viewed as a free data type, thus combining the clarity of pattern matching with the efficiency of data abstraction.
Providing efficient operations on arrays in a functional language is problematic. No completely satisfactory solution has yet been found. This paper proposes a new solution, which is a variant on the ``monolothic'' approach to array operations. The new solution is also not completely satisfactory, but does have advantages complementary to other proposals. It makes a class of programs easy to express, notably those involving the construction of histograms. It also allows for parallel implementations without the need to introduce non-determinism.
This note presents a trivial transformation that can eliminate many calls of the concatenate (or append) operator from a program. The general form of the transformation is well known, and one of the examples, transforming the reverse function, is a classic. However, so far as I am aware, this style of transformation has not previously been systematised in the way done here. The transformation is suitable for incorporation in a compiler, and improves the asymptotic time complexity of some programs from quadratic to linear. There is a syntactic test that determines when the transformation will succeed in eliminating a concatenate operation.
This paper presents the derivation of an efficient compiler for pattern-matching in a functional language. The algorithm was published, independently, by Augustsson and Wadler, and is used in the LML compiler. The derivation is based on that given in Barrett's M.Sc. dissertation The algorithm relates to functional languages in two ways: a functional language is used as the medium of the derivation, and the algorithm is useful for compiling functional languages.
Orwell, later called OL, was one of the predecessors to Haskell. It was designed by Philip Wadler when a postdoc at Oxford, and maintained by Quentin Miller and Martin Raskovsky.
Philip Wadler, An Introduction to Orwell, 1985.
pdf
Philip Wadler and Quentin Miller, Orwell Manual.
pdf
Philip Wadler, Quentin Miller, and Martin Raskovsky. OL Manual.
pdf
