Lambda the Ultimate

The Functional Payout Framework (fpf) is a Haskell application that uses an embedded domain-specific functional language to represent and process exotic financial derivatives. Whereas scripting languages for pricing exotic derivatives are common in banking, fpf uses multiple interpretations to not only price such trades, but also to analyse the scripts to provide lifecycle support and more. This paper discusses fpf in relation to the wider trading workflow and our experiences in using a functional language in such a system as both an implementation language and a domain-specific language.

Section 3 is a nice discussion of why Haskell was chosen. Section 4 illustrates one of the major benefits of using DSLs, namely that different backends can be applied to programs written in the DSL, allowing various types of runtime behavior and analysis without the need to re-code each program for each purpose (thus n+m, rather than n*m programs).

Another topic that may be worth discussing is the authors' dislike of point free style.

What we really need, of course, are DSLs for financial regulation (and possibly for specifying various definitions of honesty), but that's a separate issue...

If optimization and intermediate languages for lazy functional languages are your things, take a look at Types are Calling Conventions by Max Bolingbroke and Simon Peyton Jones.

It is common for compilers to derive the calling convention of a function from its type. Doing so is simple and modular but misses many optimisation opportunities, particularly in lazy, higher-order functional languages with extensive use of currying. We restore the lost opportunities by defining Strict Core, a new intermediate language whose type system makes the missing distinctions: laziness is explicit, and functions take multiple arguments and return multiple results.

Polymorphic Delimited Contiunations by Kenichi Asai and Yukiyoshi Kameyama, in the 5^th ASIAN Symposium on Programming Languages and Systems (2007).

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations.

Now, the real reason that I post this is because of Oleg's ShiftResetGenuine, which implements polymorphic delimited continuations in Haskell, and primarily cites this paper as well as Robert Atkey's Parameterized Notions of Computation. So if you find this paper challenging to read, Oleg provides you with a concrete playground in which to experiment.

It's also notable that Matthieu Sozeau has GenuineShiftReset available, which is a Coq version of Oleg's code.

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.