Archive for October, 2007

Archimedes, Gentzen and lenses

Saturday, October 20th, 2007 by Hancock

At Neil’s request, I talked on the topic of “lenses”, a name I use for a structure underlying many well-ordering proofs. (The same name is used by some people for funny-bracket notation for anamorphisms, catamorphisms, and the like. The notions have nothing to do with each other, except insofar as initial algebras are involved.)

I started by explaining “Archimedes trick”, involved in his work the “Sand Reckoner”. See http://en.wikipedia.org/wiki/The_Sand_Reckoner. (more…)

Back from ICFP

Friday, October 12th, 2007 by Wouter

As I should be working hard to meet an upcoming deadline, I’ve spent a fair share of last week faffing about with various ways to generate pictures from Haskell. This was directly inspired by an exercise on Andres Loeh’s course on Functional programming at Utrecht University. I’ve written a few small Haskell programs to generate .ppm images, together with some shell scripts to turn .ppm images into .gifs, and subsequently build an animated .gif from the resulting files. The results can be fairly hypnotic, to say the least.

Hypnotic All we need to do now is bundle this code as an exercise, add subliminal messages about how great functional programming is, and ship it to our first-years. A lot of the code I wrote is directly inspired by Conal Elliott’s terrific article about functional images in The fun of programming.

To wind down, Graham suggested we watch Don Stewart’s XMonad talk from the Haskell Workshop.

The internal workings of GHC

Friday, October 5th, 2007 by Graham

Andy Gill from Galois visited today, and talked about two of the key ideas in the Glasgow Haskell Compiler: the simple data type that is used to represent expressions (copied below), and the manner in which unboxed values are handled.


data Expr b = — “b” for the type of binders,
Var Id
| Lit Literal
| App (Expr b) (Arg b)
| Lam b (Expr b)
| Let (Bind b) (Expr b)
| Case (Expr b) b Type [Alt b]
| Cast (Expr b) Coercion
| Note Note (Expr b)
| Type Type

type Arg b = Expr b

type Alt b = (AltCon, [b], Expr b)

data AltCon =
DataAlt DataCon
| LitAlt Literal
| DEFAULT
deriving (Eq, Ord)

data Bind b =
NonRec b (Expr b)
| Rec [(b, (Expr b))]