Thoughts about types

Types in programming languages define logical properties of a program in that language.

N.B. I am not talking about type annotations, i.e. the programmer may explicitly specifiy types or they may be inferred.

When a program successfully type checks, the execution of the type checker constitutes a proof of those logical properties w.r.t the program (assuming correct, consistent behaviour of the type checker itself).

If a program fails the type checker it implies that (as far as the type checker is concerned) there is ambiguity or logical inconsistency w.r.t to the program (again assuming no bugs in the type checker itself).

Partial functions subvert the type system and therefore undermine the value of the logical proof provided by the type checker. Apparently there is a relationship between this, Turing completeness and the Halting problem, although I don't understand that yet.

One of my goals over the summer is to work through Types and Programming Languages by Benjamin Pierce.

Zermelo and set theory

I am currently studying axiomatic set theory. In the process I came across Zermelo and Set Theory, which gives details about his work and interactions with other significant mathematicians.

While interesting, it unfortunately didn't help me when working out his proof for the Schroder-Bernstein Theorem in an assignment. :-)

Digital Camera

Given the shortlist from my requirements, I bought the Fujifilm FinePix F100fd. Tried it out at the Amberley Air Show on the weekend and am happy with the results so far. Some of the photos are here on Flickr.

On a side note, I also shot some video from our digital video camera and tried uploading that to Flickr as well, but after the Flickr processing the videos looked terrible (mind you my original footage was a bit dodgy to start with :-)). I guess I need to find a decent private/public video sharing site. Vimeo and Viddler look interesting.

Digital Camera Requirements

My wife and I have used an old digital camera (generously passed on from a friend when they upgraded) for some years now and the time has finally come to upgrade. So this is what I think we need in a camera:

1. Neither of us know much about photography so we need to be able to point-and-click and still get reasonably good quality images in different light conditions.


2. 5x optical zoom or greater.


3. Low response time between pressing the button and taking the photo.


4. Wider angle would be handy for those landscape or family photos.


5. Prefer AA batteries over lithium.


6. Viewfinder might be nice for outdoor shots when it is difficult to view the LCD.

I would like to spend no more than AUD $400. From reading reviews, I arrived at the following shortlist:

• Fujifilm FinePix F100fd
  Image quality scored well in reviews: DigitalCameraReview, Digital Camera Resource Page, cnet. Has a 5x optical zoom and and 28mm wide angle lens. No viewfinder and uses a lithium-ion battery. DigitalCameraReview thought this was a great camera for the point-and-click user.


• Panasonic Lumix DMC-FS20
  Image quality scored well in reviews: DigitalCameraReview, cnet, Steve's Digicams. Auto mode got a good rap. 4x optical zoom and 30mm wide angle lens. No viewfinder, although screen did well outside and has a lithium-ion battery. Cnet thought this was a great camera for the point-and-click user, but it would be a bit over budget.


• Sony Cyber-shot DSC-W150
  Image quality didn't seem to score quite as well as the previous cameras, although still good: DigitalCameraReview, Steve's Digicams. 5x optical zoom and 30mm wide angle lens. Small viewfinder and lithium-ion battery.

Worlds: Controlling the Scope of Side Effects

The state of an imperative program—e.g., the values stored in global and local variables, objects’ instance variables, and arrays—changes as its statements are executed. These changes, or side effects, are visible globally: when one part of the program modifies an object, every other part that holds a reference to the same object (either directly or indirectly) is also affected. This paper introduces worlds, a language construct that reifies the notion of program state, and enables programmers to control the scope of side effects.

This paper is from the Inventing Fundamental New Computing Technologies project at the Viewpoints Research Institute (founded by Alan Kay).

Seems like it is intended to be quite a coarse-grained approach to program state. A little like a developer checking out a copy of a project from a version control system, making changes and either committing or reverting back.

State in Clojure

Many people come to Clojure from an imperative language and find themselves out of their element when faced with Clojure's approach to doing things, while others are coming from a more functional background and assume that once they leave Clojure's functional subset, they will be faced with the same story re: state as is found in Java. This essay intends to illuminate Clojure's approach to the problems faced by imperative and functional programs in modeling the world.

From: Values and Change - Clojure's approach to Identity and State.

Farewell Marion

A brave 10 year old boy shed a tear and said goodbye to his mother at her burial site today.

Cancer claims another victim and now her husband and two boys start a new journey together.