The Semicolon Wars

The Semicolon Wars
Brian Hayes

A laypeople's introduction to the world of programming languages from American Scientist. Includes some history, a high-level overview of different programming paradigms, some guesses at which differences make a difference, some Dijkstra, and some cheap shots at zealots.

Regular LtU readers won't find anything new here, but it's a good article, and it's always nice to see something like this for the general reading public.

This Is the Title of This Story, Which Is Also Found Several Times in the Story Itself

This is the first sentence of this story. This is the second sentence. This is the title of this story, which is also found several times in the story itself. This sentence is questioning the intrinsic value of the first two sentences. This sentence is to inform you, in case you haven't already realized it, that this is a self-referential story, that is, a story containing sentences that refer to their own structure and function. This is a sentence that provides an ending to the first paragraph.

This is the link to the story

foldl and foldr and are two fun websites that may just help you wrap your head around left and right folds. They are the product of Oliver Steele, designer of (Open)Laszlo.

Google Magic

I have characterized myself recently as a recovering typoholic and a convert to Visual Basic and in my various talks I use the paper on type-indexed rows that I wrote together with Mark Shields as the prime example of how deep you can fall as an addict to static typing.

As many of us undoubtedly do every once in a while, I was egosurfing for “typoholic”; vague hoping it would be a Google wack. However, much to my astonishment the first hit is actually our paper on type-indexed rows (alternatively type in typoholic on the Google homepage and hit “I’m feeling lucky”). That page does not contain the word "typoholic" and until now there were no links pointing to it!

If you ask me, this is pure voodoo. Perhaps I should start wrapping myself in aluminum foil to protect me against the Google mind control waves.

Inverse typechecker and theorem proving in intuitionistic and classical logics

Another cool demonstration from Oleg:

I'd like to point out a different take on Djinn:

The first defines the Hindley-Milner typechecking relation for a
language with polymorphic let, sums and products. We use the Scheme
notation for the source language (as explained at the beginning of the
first file); ML or Haskell-like notations are straightforward. The
notation for type terms is infix, with the right-associative arrow.

The typechecking relation relates a term and its type: given a term we
obtain its type. The relation is pure and so it can work in reverse: given a type, we can obtain terms that have this type. Or, we can give a term with blanks and a type with blanks, and ask the relation to fill in the blanks.

As an example, the end of the file type-inference.scm shows the derivation for the terms call/cc, shift and reset from their types in the continuation monad. Given the type

(((a -> . ,(cont 'b 'r)) -> . ,(cont 'b 'b)) -> . ,(cont 'a 'b))

we get the expression for shift:

   (lambda (_.0) (lambda (_.1)
	((_.0 (lambda (_.2) (lambda (_.3) (_.3 (_.1 _.2)))))
	 (lambda (_.4) _.4))))

It took only 2 milli-seconds.

More interesting is using the typechecker for proving theorems in
intuitionistic logic: see logic.scm. We formulate the proposition in types, for example:

  (,(neg '(a * b)) -> . ,(neg (neg `(,(neg 'a) + ,(neg 'b)))))

This is one direction of the deMorgan law. In intuitionistic logic,
deMorgan law is more involved:

	NOT (A & B) == NOTNOT (NOT A | NOT B)

The system gives us the corresponding term, the proof:

(lambda (_.0)
      (lambda (_.1) 
	(_.1 (inl (lambda (_.2) 
		    (_.1 (inr (lambda (_.3) (_.0 (cons _.2 _.3))))))))))

The de-typechecker can also prove theorems in classical logic,
via double-negation (aka CPS) translation. The second part of
logic.scm demonstrates that. We can formulate a proposition:

(neg (neg `(,(neg 'a) + ,(neg (neg 'a)))))

and get a (non-trivial) term

	(lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1))))))

It took only 403 ms. The proposition is the statement of the Law of
Excluded Middle, in the double-negative translation.

So, programming languages can help in the study of logic.

Lego Mindstorms NXT Robotics Announced

(via Lemonodor)

This looks cool.

I am not sure about the details of how these bricks are to be programmed, but from the Slashdot dicussion is seems that there is some kind of dataflow language. Even more interesting is the claim that the VM is going to be documented, so third party language developers can target this low end robotics platform.

G-Men Called on W-Hats for WMVD

One of the cool things about Second Life is that players can create new kinds of objects, by writing small programs in a special scripting language to describe how the objects should behave, and then launching objects into the world.

Things got really out of hand when the W-Hats created a doomsday device. It looked like a harmless little orb, but it was programmed to make copies of itself, repeatedly. The single object split into two. Then each of those split, and there were four. Then eight, and sixteen, and so on to infinity.

A highly amusing story this is.

I guess the correct term for this kind of thing is The law of unintended DSL consequences.

Please share similar stories, if you got them.

Djinn, a theorem prover in Haskell, for Haskell.

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

To play with Djinn do a
darcs get
or get
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.

Top N Papers 2005

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):

(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!)

Code Reading

LtU readers know that I am long time advocate of code reading. As I've argued here in the past, reading great code is the best way to acquire good programming skills. It's also a pleasure to read good code. Yes - reading code can be fun.

It turns out that I am not alone (though my conception of a code reading workshop is perhaps somewhat different than the things discussed there).

Anyway, this is a chance to continue one of my pet memes. Many of the pieces of great code I've read over the years come from language processing tools (e.g., compilers, meta-programming systems etc.) I don't think this is a coincidence.

Now's your chance to tell us your favorite examples.

The rules: The code must be beautiful and it must be programming language related (and no, being written in a programming language isn't enough).

XML feed