Lambda the Ultimate

This blog post about Idris led me to Edwin C. Brady's 2005 PhD thesis, Practical Implementation of a Dependently Typed Functional Programming Language.

This thesis considers the practical implementation of a dependently typed programming language, using the Epigram notation defined by McBride and McKinna. Epigram is a high level notation for dependently typed functional programming elaborating to a core type theory based on Luo's UTT, using Dybjer's inductive families and elimination rules to implement pattern matching. This gives us a rich framework for reasoning about programs. However, a naive implementation introduces several run-time overheads since the type system blurs the distinction between types and values; these overheads include the duplication of values, and the storage of redundant information and explicit proofs.

A practical implementation of any programming language should be as efficient as possible; in this thesis we see how the apparent efficiency problems of dependently typed programming can be overcome and that in many cases the richer type information allows us to apply optimisations which are not directly available in traditional languages. I introduce three storage optimisations on inductive families; forcing, detagging and collapsing. I further introduce a compilation scheme from the core type theory to G-machine code, including a pattern matching compiler for elimination rules and a compilation scheme for efficient runtime implementation of Peano's natural numbers. We also see some low level optimisations for removal of identity functions, unused arguments and impossible case branches. As a result, we see that a dependent type theory is an effective base on which to build a feasible programming language.

What's the current state of the art in optimization of dependently typed languages?

Ensuring Correct-by-Construction Resource Usage by using Full-Spectrum Dependent Types

Where it has been done at all, formally demonstrating the correctness of functional programs has historically focused on proving essential properties derived from the functional specification of the software. In this paper, we show that correct-by-construction software development can also handle the equally important class of extra-functional properties, namely the correct usage of resources. We do this using a novel embedded domain-specific language approach that exploits the capabilities of full-spectrum dependent types. Our approach provides significant benefits over previous approaches based on less powerful type systems in reducing notational overhead, and in simplifying the process of formal proof.

More ammunition for the importance of embedded domain-specific languages, dependent types, and correctness-by-construction.

Denotational design with type class morphisms. Conal Elliott.

Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of types but also of properties (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of the remaining freedom is in how the implementation works, and some is in what it accomplishes.

To give additional guidance to the what, without impinging on the how, this paper proposes a principle of type class morphisms (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that the instance’s meaning is the meaning’s instance. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback.

The paper is illustrated with several examples of type, meanings, and morphisms.

To continue in our new all-Conal format... This paper brings together a bunch of things that Conal's been talking about lately, and "algebra of programming" fans will probably like his approach.

(I have a hunch that what he calls a "type class morphism" could be described using standard categorical jargon, but I haven't given it much thought. Suggestions?)

Luke Palmer and Nick Szabo can shoot me for this if they want, but I think this is warranted, and I want to connect a couple of dots as well. Luke is one of a number of computer scientists, with Conal Elliott probably being the best known, who have devoted quite a bit of attention to Functional Reactive Programming, or FRP. FRP has been discussed on LtU off and on over the years, but, unusually for LtU IMHO, does not seem to have gotten the traction that some other similarly abstruse subjects have.

In parallel, LtU has had a couple of interesting threads about Second Life's economy, smart contracts, usage control, denial of service, technical vs. legal remedies, and the like. I would particularly like to call attention to this post by Nick Szabo, in which he discusses a contract language that he designed:

Designing the contract language radically changed my idea of what program flow and instruction pointers can be. Its successor, a general-purpose programming language, may thereby make event-oriented programming and concurrency far easier. The language is targeted at GUI programming as well as smart contracts, real-time, and workflow programming. My answer to the problems of concurrency and event handling is to make the ordering of instructions the syntactic and semantic core of the language. The order of execution and event handlers are the easiest things to express in the language rather than kludged add-ons to a procedural or functional language.

In recent private correspondence, Nick commented that he'd determined that he was reinventing synchronous programming à la Esterel, and mentioned "Reactive" programming.

Ding!

To make a potentially long entry somewhat shorter, Luke is working on a new language, Dana, which appears to have grown out of some frustration with existing FRP systems, including Conal Elliot's Reactive, currently perhaps the lynchpin of FRP research. Luke's motivating kickoff post for the Dana project can be found here, and there are several follow-up posts, including links to experimental source code repositories. Of particularly motivating interest, IMHO, is this post, where Luke discusses FRP's interaction with garbage collection succinctly but nevertheless in some depth. Luke's most recent post makes the connection from Dana, which Luke has determined needs to have a dependently-typed core, to Illative Combinatory Logic, explicit, and offers a ~100 line type checker for the core.

I find this very exciting, as I believe strongly in the project of being able to express computation centered on time, in the sense of Nick's contract language, in easy and safe ways extremely compelling. I've intuited for some time now that FRP represents a real breakthrough in moving us past the Von Neumann runtime paradigm in fundamental ways, and between Conal Elliott's and Luke's work (and no doubt that of others), it seems to me that my sense of this may be borne out, with Nick's contract language, or something like it, as an initial application realm.

So I wanted to call attention to Luke's work, and by extension recapitulate Conal's and Nick's, both for the PLT aspects that Luke's clearly represents, but also as a challenge to the community to assist in the realization of Nick's design efforts, if at all possible.

Functional Pearl: Type-safe pattern combinators, by Morten Rhiger:

Macros still have not made their way into typed higher-order programming languages such as Haskell and Standard ML. Therefore, to extend the expressiveness of Haskell or Standard ML gradually, one must express new linguistic features in terms of functions that fit within the static type systems of these languages. This is particularly challenging when introducing features that span across multiple types and that bind variables. We address this challenge by developing, in a step-by-step manner, mechanisms for encoding patterns and pattern matching in Haskell in a type-safe way.

This approach relies on continuation-passing style for a full encoding of pattern matching. Tullsen's First-Class Patterns relies on a monadic encoding of pattern matching to achieve abstraction over patterns. Given the relationship between CPS and monads, the two approaches likely share an underlying structure.

Abstracting over patterns yields a whole new level of abstraction, which could significantly improve code reuse. The only concern is compiling these more flexible structures to the same efficient pattern matching code we get when the language natively supports patterns. Section 4.9 discusses the efficiency concerns, and suggests that partial evaluation can completely eliminate the overhead.

Books on two of the languages that get a lot of airplay on LtU have made the finalist list for this year's Jolt awards.

Books Technical
* High Performance MySQL by Baron Schwartz, Peter Zaitsev, Vadim Tkachenko, Jeremy Zawodny, Arjen Lentz, Derek J. Balling (O'Reilly Media)
* Java Power Tools by John Ferguson Smart (O'Reilly Media)
* Programming in Scala by Martin Odersky, Lex Spoon, and Bill Venners (Artima Press)
* Real World Haskell by John Goerzen, Bryan O'Sullivan, Donald Bruce Stewart (O'Reilly Media)
* The iPhone Developer's Cookbook: Building Applications with the iPhone SDK by Erica Sadun (Addison-Wesley Professional)

Congratulations to Martin, Lex, Bill, John, Bryan, and Don!

Whether or not either book wins, it's quite a sea change that two sophisticated, statically typed functional programming languages with research origins are getting so much mainstream attention.

From the FAQ

How are the winners selected?

Our judges not only examine the standard criteria of audience suitability, productivity, innovation, quality, ROI, risk and flexibility, but also seek to honor products that are ahead of the curve. Jolt-winning products are universally useful; are simple, yet rich in functionality; redefine their product space; and/or solve a nagging problem that has consistently eluded other products and books.

Programmable Concurrency in a Pure and Lazy Language, Peng Li's 2008 PhD dissertation, is a bit more implementation focused than is common on LtU. The paper does touch on a wide range of concurrency mechanisms so it might have value to any language designer considering ways to tackle the concurrency beast.

First, this dissertation presents a Haskell solution based on concurrency monads. Unlike most previous work in the field, this approach provides clean interfaces to both multithreaded programming and event-driven programming in the same application, but it also does not require native support of continuations from compilers or runtime systems. Then, this dissertation investigates for a generic solution to support lightweight concurrency in Haskell, compares several possible concurrency configurations and summarizes the lessons learned.

The paper's summary explains what I like most about it:

the project ... solves a systems problem using a language-based approach. Systems programmers, Haskell implementors and programming language designers may each find their own interests in this dissertation.

Even if concurrency isn't your thing, section 6.3 describes the author's findings on the pros and cons of both purity and laziness in a systems programming context.

A much beloved and widely used example showing the elegance and simplicity of lazy functional programming represents itself as "The Sieve of Eratosthenes." This paper shows that this example is not the sieve and presents an implementation that actually is.

Starting with the classic one-liner sieve (p : xs) = p : sieve [x | x <- xs, x ‘mod‘ p > 0] O'Neill proceeds to show why this standard rendition of the Sieve of Eratosthenes does not in fact "cross-off" the multiples of each prime in the same way the "real" Sieve does.

She notes that "Some readers may feel that despite all of these concerns, the earlier algorithm is somehow “morally” the Sieve of Eratosthenes. I would argue, however, that they are confusing a mathematical abstraction drawn from the Sieve of Eratosthenes with the actual algorithm. The algorithmic details, such as how you remove all the multiples of 17, matter."

A fun read.

Type inference for correspondence types

We present a type and effect system for proving correspondence assertions in a π-calculus with polarized channels, dependent pair types and effect terms. Given a process P and a type environment E, we describe how to generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. A reasonable model of the generated constraints yields a type and effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type and effect inference in our system is polynomial-time decidable.

That's a mouthful. The part of the paper that perked my virtual ears up:

Most importantly, our approach is general in nature; the encoding of types and terms does not depend on the rules of the type system. For this reason, our approach appears a natural candidate for obtaining similar type inference results for type systems such as [9], where correspondences concern formulas in an arbitrary authorization logic and the underlying process calculus includes cryptographic operations, and type systems for secrecy properties such as [12]. The possibility of such ramifications is currently under investigation.

[9] is A type discipline for authorization policies, which is followed up by Type-checking zero knowledge. The upshot is that it might be possible to have reasonable type inference support for a dependent type- and effect system with cryptographic operations supporting some of the most powerful privacy and security primitives and protocols currently known. I find this very exciting!

Qi II has been released. Qi is a functional programming language built on top of Common Lisp. It has an optional static type system based on sequent calculus and a general focus on logic based programming. For version II, see the what's new page. Rule closures in particular look very interesting.

Unlike Qi I, Qi II allows you to embed sequent rules within functions, evaluating them to closures. These rule closures are type checked and are permeable to having their variables lexically bound from outside the scope of the rule itself. These devices enable the student of computational logic to effortlessly code complex logical systems of all descriptions. Thus the rule

let PTerm/X (replace-by X Term P)
PTerm/X, (all X P) >> Q;
____________________
(all X P) >> Q;

allows universally quantified assumptions to be instantiated to new premises. This rule can be embedded into a Qi II function called all-left which does precisely this job. The rule is turned into a closure by the rule function which is then applied to the problem (list of sequents).

(define all-left
{term --> [sequent] --> [sequent]}
Term S -> ((rule let PTerm/X (replace-by X Term P)
PTerm/X, (all X P) >> Q;
____________________
(all X P) >> Q;) S))

FPQi devotes a hundred pages to the exploration of this powerful construction.

Also with this release is a new book: Funcitonal Programming in Qi.

Earlier versions of Qi have been mentioned on LtU here and here.