Lambda the Ultimate

The goal of my project was to be able to thoroughly test a poker server using poker bots. Each poker bot was to to excercise different parts of the server by talking the poker protocol consisting of 150+ binary messages. The poker server itself is written in C++ and runs on Windows....

This app is all about binary IO, thousands of threads/processes and easy serialization. All I ever wanted to do was send packets back and forth, analyze them and have thousands of poker bots running on my machine doing same. Lofty but simple goal :-). Little did I know!

Erlang and Haskell compared... Want to know the conclusion?

I was able to finish the Erlang version 10 times faster and with 1/2 the code. Even if I cut the 10-11 weeks spent on the Haskell version in half to account for the learning curve, I would still come out way ahead with Erlang.

I am sure you'll find a lot to disagree with in this article...

LtU readers will recognize the names of the lecturers, if not the specific presentation titles. Among the lecturers are Jeremy Gibbons, Ralf Hinze, Ralf Lämmel and Tim Sheard (who will talk about putting Curry-Howard to work).

GPUs are difficult to program for general-purpose uses. Programmers must learn graphics APIs and convert their applications to use graphics pipeline operations. We describe Accelerator, a system that simplifies the programming of GPUs for general-purpose uses. Accelerator provides a high-level data-parallel programming model as a library that is available from a conventional imperative programming language. The library translates the data-parallel operations on-the-fly to optimized GPU pixel shader code and API calls.

A library provides programmers with a new type of array, a data-parallel array. Data-parallel arrays differ from conventional arrays in two ways. First, the only operations available on them are aggregate operations over entire input arrays. The operations are a subset of those found in languages like APL. They include element-wise arithmetic and comparison operators, reductions to compute min, max, product, and sum, and transformations on entire arrays. Second, the data-parallel arrays are functional: each operation produces an entirely new data-parallel array.

Nick Benton and Andrew Kennedy. 2001. Exceptional syntax. Journal of Functional Programming 11(4): 395-410.

From the points of view of programming pragmatics, rewriting and operational semantics, the syntactic construct used for exception handling in ML-like programming languages, and in much theoretical work on exceptions, has subtly undesirable features. We propose and discuss a more well-behaved construct.

Why do I need a monad for IO in Haskell? The standard explanation is, that the IO monad hides the non-functional IO actions ---which do have side effects--- from the functional world of Haskell. But how does this "hiding" work, apart from having IO actions disappearing beyond the borders of my knowledge?

This report scratches the surface of category theory, an abstract branch of algebra, just deep enough to find the monad structure. On the way we discuss the relations to the purely functional programming language Haskell. Finally it should become clear how the IO monad keeps Haskell pure.

It's hard for me to judge how successful this tutorial is going to be with beginners, but it seems well written.

The target audience isn't porgrammers trying to learn about monads as a programming construct, but rather programmers that want to get a taste of theory.

by Jérôme Vouillon

We propose a type system based on regular tree grammars, where algebraic datatypes are interpreted in a structural way. Thus, the same constructors can be reused for different types and a flexible subtyping relation can be defined between types, corresponding to the inclusion of their semantics. For instance, one can define a type for lists and a subtype of this type corresponding to lists of even length. Patterns are simply types annotated with binders. This provides a generalization of algebraic patterns with the ability of matching arbitrarily deep in a value. Our main contribution, compared to languages such as XDuce and CDuce, is that we are able to deal with both polymorphism and function types.

It will appear in POPL '06.

Lennart Augustsson announced Djinn on the Haskell mailing list recently.

He included this demonstration:

I've written a small program that takes a (Haskell) type
and gives you back a function of that type if one exists.
It's kind of fun, so I thought I'd share it.

It's probably best explained with a sample session.

   calvin% djinn
   Welcome to Djinn version 2005-12-11.
   Type :h to get help.
# Djinn is interactive if not given any arguments.
# Let's see if it can find the identity function.
   Djinn> f ? a->a
   f :: a -> a
   f x1 = x1
# Yes, that was easy.  Let's try some tuple munging.
   Djinn> sel ? ((a,b),(c,d)) -> (b,c)
   sel :: ((a, b), (c, d)) -> (b, c)
   sel ((_, v5), (v6, _)) = (v5, v6)

# We can ask for the impossible, but then we get what we
# deserve.
   Djinn> cast ? a->b
   -- cast cannot be realized.

# OK, let's be bold and try some functions that are tricky to write:
# return, bind, and callCC in the continuation monad
   Djinn> type C a = (a -> r) -> r
   Djinn> returnC ? a -> C a
   returnC :: a -> C a
   returnC x1 x2 = x2 x1

   Djinn> bindC ? C a -> (a -> C b) -> C b
   bindC :: C a -> (a -> C b) -> C b
   bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17))

   Djinn> callCC ? ((a -> C b) -> C a) -> C a
   callCC :: ((a -> C b) -> C a) -> C a
   callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11)
# Well, poor Djinn has a sweaty brow after deducing the code
# for callCC so we had better quit.
   Djinn> :q
   Bye.

To play with Djinn do a
darcs get http://darcs.augustsson.net/Darcs/Djinn
or get
http://darcs.augustsson.net/Darcs/Djinn/Djinn.tar.gz
Then just type make. (You need a Haskell 98 implementation and
some libraries.) And then start djinn.

For the curious, Djinn uses a decision procedure for intuitionistic
propositional calculus due to Roy Dyckhoff. It's a variation of
Gentzen's LJ system. This means that (in theory) Djinn will always
find a function if one exists, and if one doesn't exist Djinn will
terminate telling you so.

This is the very first version, so expect bugs. :)

Don Stewart wrote a lambdabot plugin for Djinn a few hours later.

15:39:01  @djinn a -> b -> a
15:39:02  x :: a -> b -> a
15:39:02  x x1 _ = x1
15:39:11  @djinn (a -> b -> c) -> ((a,b) -> c)
15:39:11  x :: (a -> b -> c) -> (a, b) -> c
15:39:11  x x1 (v3, v4) = x1 v3 v4
15:39:27  @djinn (a -> b) -> (c -> b) -> Either a c -> b
15:39:27  x :: (a -> b) -> (c -> b) -> Either a c -> b
15:39:27  x x1 x2 x3 = case x3 of
15:39:27       Left l4 -> x1 l4
15:39:27       Right r5 -> x2 r5
15:40:06  @djinn a -> [a] -> [a]
15:40:07  x :: a -> [a] -> [a]
15:40:07  x _ x2 = x2
15:40:08  @help djinn
15:40:09   @djinn 
15:40:09  Generates Haskell code from a type.

Djinn has proven to be much fun on #haskell.

Stefan Holdermans. Master's thesis, Utrecht University, 2005.
An extension of Wadler's views.

In the conclusion, in a comparison to SYB, this paper notes:

Even when they target the same types of applications, it is often hard to transfer ideas and techniques between two different [generic programming] approaches. Therefore, frameworks for generic programming are typically studied in rather isolated environments. When proposals are compared to one another, the focus usually is on issues like which programs can and which programs cannot be written within the context of a specific paradigm: attention is drawn to the surface area of a generic-programming model, rather than to the underlying theory and techniques.

Generic views on data types may allow us to break with this tradition and incorporate different approaches within a single framework. The idea is to define a view that captures the way in which a given approach treates data types and to consequently transfer the building blocks of that approach to Generic Haskell idioms.

Before noting the impossibility of even this approach to encode generic fold.

Module Mania: A Type-Safe, Separately Compiled, Extensible Interpreter

To illustrate the utility of a powerful modules language, this paper presents the embedded interpreter Lua-ML. The interpreter combines extensibility and separate compilation without compromising type safety. Its types are extended by applying a sum constructor to built-in types and to extensions, then tying a recursive knot using a two-level type; the sum constructor is written using an ML functor. The initial basis is extended by composing initialization functions from individual extensions, also using ML functors.

This is an excellent example of how the ML module language doesn't merely provide encapsulation but also strictly adds expressive power. It also demonstrates how a dynamic language (Lua) can be embedded in the statically-typed context of ML. Finally, it demonstrates that none of this need come at the expense of separate compilation or extensibility. Norman Ramsey's work is always highly recommended.

In functional programming, programs are often written in a compositional style. There are many advantages to this, such as clarity and modularity, but the resulting programs can be inefficient in terms of space, due to the use of intermediate data structures. These structures may be removed using deforestation techniques, but whether the space performance is actually improved depends on the structures being consumed in the same order that they are produced. In this paper we explore this problem and suggest a solution, in particular for lists and then generalising to trees.

Since the paper discusses many examples, it is quite enjoyable to read and can even serve as an introduction to folds.