Lambda the Ultimate

2005 is nearly over, and as everyone knows, December is the time for compiling hugely subjective Top 5 (10, 20, 100) lists for everything under the sun. I think it would be fun to see everybody's favorite papers... Here's mine, totally off the top of my head (I'm sure I'm forgetting something essential):

• Scalable Component Abstractions - Martin Odersky and Matthias Zenger
• Generic implementation of all four *F* operators: from control0 to shift - Oleg Kiselyov
• Composable Memory Transactions - Tim Harris, Simon Marlow, Simon Peyton Jones, and Maurice Herlihy
• Putting Curry-Howard to Work - Tim Sheard
• Extensible Records With Scoped Labels - Daan Leijen

(Don't worry about trying to post the "best" papers in some objective sense, just whatever excited you... Show me what I missed this year!)

Hi,

I don't know if any of you are interested in this but, the weekly BBC Radio 4 program "In Our Time" last installment divoted the whole program to the development and history of Artifical Intelligence (AI).

As you are probably aware, BBC Radio 4 offers a "listen again" service where past programs are streamed to you via Real Player so that you can enjoy missed programmes at your leisure. However, "IOT" is one of the few programs where you can actually download the programme as an MP3 as well.

"IOT"'s webiste is here: http://www.bbc.co.uk/radio4/history/inourtime/inourtime.shtml.
Looks for the links on the left hand side of the page to either listen again via RealPlayer or download the MP3 if your interested in listening to this programme. (The MP3 is DRM free, BTW)

The next episode (about the Peterloo Massacre) is on Thursday morning and this new episode will replace this current edition about AI, so you may need to "digitus extractus" if you want to catch the programme and listen to it.

Enjoy
Cheers
Barry Carr
Scotland

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.