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