That’s for sure

Certified Programming with Dependent Types: A pragmatic introduction to the COQ proof assistant by Adam Chlipala

I really loved this introduction to COQ, a formal proof management system which can be used to formalise and prove mathematical theorems. COQ is based on a constructive type theory which allows you to also write dependently typed programs in its formal language, which can be executed by the COQ system itself. COQ’s most famous moment was probably when it was used to formalise the four colour theorem.

This text is available online here, as a series of COQ script files which can be executed and which contain the text of the book as embedded comments. The book itself is really practical, starting quickly with a definition of the semantics of a simple language of expressions over the natural numbers (including times, plus and later comparison), and then proves a the correctness of a compiler that compiles an expression to run on top of a simple stack machine.

coq

The book then rapidly moves on to give an overview of the whole COQ system. It starts with a description of very basic programming and proving, all the while working through a set of examples. It covers infinite data types and the equivalence of streams. It then moves on to issues around programming with dependent types and more general forms of recursion, covering the tricky constructive concepts of equality and universes.

The final section of the book discusses more proof engineering concepts such as using reflection in proofs, and one chapter covers the Ltac language, allowing a user to invent new proof methods (whilst keeping the core logic consistent).

A brilliant book that covers both the theoretical concepts and also explains them with a stream of useful practical examples. Loved it!

Posted in Computers and Internet | Leave a comment

It’s off to war we go

DogFight: How Apple and Google went to war and started a revolution by Fred Vogelstein

A fairly lightweight book which gives details about the development of the iPhone and the Android platform, telling the story from the perspective of both the Apple and Google teams. For some of the book we do a chapter in turn from each company, though the stories start to intertwine for the most part. Few technical details, but some coverage of the patent battles between the various players including Samsung, and if you haven’t followed the story from the beginning, this book is a fairly good way to catch up.

Posted in Books | Leave a comment

Where next?

In Pursuit of the Travelling Salesman: Mathematics at the Limits of Computation by William J Cook

This is one of those maths books that describes the problem, and then tells the story of the various historical approaches to solving it. The story is fascinating, and in the pre-computer days involved massive amounts of hand calculation using clever tricks to prove lower bounds for various instances of the problem.

Along the way we learn about the P!=NP conjecture, and also learn about the simplex method and integer programming which can be used as a way to get strong lower bounds for various for travelling salesman problems (using so called control zones).

A good interesting read.

Posted in Books | Leave a comment

To infinity from far away

The Man Who new Infinity: Life of the genius Ramanujan by Robert Kanigel

Very little technical detail about his various theorems and contributions, but a great biography of the man and his life, with loads of historical information about India and the British Raj at the end of the 19th century. As a resident of Cambridge, it was great to hear the interlinking story of G.H Hardy, his time at Trinity College, Cambridge and his reforms of the mathematical Tripos.

The author gets into Ramanujan’s character, seeking to explain his motivations and frustrations at not being able to do full time mathematical research, and also seeks to explain Ramanujan’s bodily breakdown when he eventually reached Cambridge. In many ways a sad story, but a very interesting read.

Posted in Books | Leave a comment

Should I do them concurrently or in parallel?

Parallel and Concurrent Programming in Haskell: Techniques for Multicore and Multithreaded Programming by Simon Marlow

This was a fascinating read. Haskell itself has a reputation for being very high level and abstract, and, of course, this book uses some very high level concepts to achieve multithreaded execution and deterministic parallelism. However the author was one of the main implementers for the runtime system of GHC, and this comes across in the writing – from the use of ThreadScope to see exactly where the threads and runtime are spending their time to the brilliant explanation of weak-head normal form, deepseq and the execution semantics using sparks.

GHC has a great number of ways of using multiple threads. The book starts with parallel Haskell, covering rpar, rseq and the Eval monad which allows an algorithm to be parameterised with different evaluation strategies. All the time, the author demonstrates the facility using an example, and often demonstrates how well things are working by measuring the speedup with number of cores that the runtime is allowed to use. Sometimes these measurements point to bottlenecks in the runtime itself and he isn’t afraid to point this out.

We move on to dataflow parallelism using the Par monad and then array style parallelism using Repa and Accelerate, a means for converting some Haskell code into CUDA which will run on the GPU.

Next the book moves on to concurrent Haskell.

The author starts by covering threads communicating via MVars (which are like data values protected by a semaphore). He then moves on to discussing Exceptions, a facility of Haskell that I had largely ignored in the past. At this point, things starts getting  little dirty as we need to start thinking about asynchronous exceptions, and that means that we need to be able to guard regions in order to prevent asynchronous exceptions happening in things like finally blocks which would make it impossible to preserve invariants.

This is the thing that I always found distasteful in C# where thread abort exceptions, which are asynchronously delivered as a result of the Thread.Abort, can be caught but require special code to prevent them propagating after the catch handler has finished.

abort

There’s also the need to prevent the delivery inside finally blocks.

finally

The GHC runtime requires the programmer to duplicate these semantics themself by exposing primitives for controlling asynchronous delivery.

The book then moves on to software transactional memory. It shows how beautiful code can become using this feature. Using retry, for example, allows the STM system to wait until the global state changes before restarting failed computations. Better still, the author points out the possible problems with STM for large transactions where the transaction log access and multiple potential retries can make performance really bad.

The rest of the book is filled with some examples, including a chat server. These examples demonstrate a number of techniques, including a function which can be used as a combinator that races two threads and returns the answer from the first to complete, aborting the other.

The book is a great read, and I think everyone will learn something from it.

Posted in Books | Leave a comment

Plug table into light

We have a regular Clojure meetup one lunchtime a week at work, and for the last couple of weeks we’ve been looking at LightTable. LightTable is a programming language IDE written entirely in ClojureScript, a variant of Clojure that can be compiled down to JavaScript. It is written as a hybrid application – the node webkit browser is embedded into a simple native application which simple displays the browser pane and then runs the packaged JavaScript. There are lots of companies using this technology as listed on the wiki here.

The ClojureScript code implements a BOT model – behaviour-object-tag, which is a kind of prototype based object system, though in this system the central focus isn’t the objects but is rather the behaviours and the objects to which they are attached. The code for the BOT system is contained in object.cljs file which is included in the LightTable source.

Using this code, we can easily create objects and behaviours and attach the behaviours to the objects. We can attach and remove behaviours dynamically. When an event is raised, the appropriate reaction is called with the passed arguments, though if no reaction is available then things just silently fail.

ObjectAndBehaviours

What are these objects? Well, an object is just an atom containing a map that records the information about the behaviour mapping. For example, one of the objects we made above prints as follows in the REPL.

#<Atom: {:lt.object/id 65, :lt.object/type :my-object, :tags #{:object}, :content nil, :triggers [], :args nil, :children {}, :listeners {:event1 [:play/behavior1], :destroy [:lt.objs.clients/on-destroy-remove-cb]}, :behaviors #{:play/behavior1}, :name Foo}>

One thing to be aware of is that the object system is dynamic only to a limited degree. If you make changes you need to refresh! objects for the current definitions to take effect.

For example, here we redefine the behaviour, to trigger it with a new event. The change doesn’t take effect until the object is refreshed.

RefreshNeeded

It’s a very clever system through. Behaviours can encapsulate functionality which can be used across multiple unrelated object types.

This tutorial shows how you can define a simple plugin. It uses the defui macro, which can be used to generate HTML elements for fairly complicated UI elements, and shows how you can use the tab manager to add these elements into the existing GUI.

We were more interested in modifying the behaviour of the existing GUI than adding new separated GUI elements, and the documentation points to the DeClassifier plugin as a demonstration of how to go about this. DeClassifier defines come commands for checking the current editor buffer and uses a behaviour definition to hook them into the existing system.

  {:+ {:app [(:lt.objs.plugins/load-js "declassifier_compiled.js" true)]
          :editor [(:lt.objs.editor/on-change :declassify-behind-cursor)]}

The :+ adds new behaviours, and there’s a :- for removing them. The name (like :editor) finds the relevant objects using the lt.object/by-tag function.

  (lt.object/by-tag :app)  -> a sequence containing the single app instance in the system. This is the top level control object.

  (lt.object/by-tag :editor) –> a sequence of the existing editors, one per loaded file

Looking at the listeners of one of the editor instances using

  (println (:listeners (deref (first (lt.object/by-tag :editor)))))

we can see the triggers and their subscriptions.

  {:editor.eval.cljs.result.replace [:lt.plugins.clojure/cljs-result.replace],
    :editor.exception [:lt.objs.eval/inline-exceptions],
    :watch [:lt.plugins.watches/eval-on-watch-or-unwatch],
    :editor.eval.clj.no-op [:lt.plugins.clojure/no-op],
    :keymap.diffs.user+ [:lt.objs.settings/user-keymap-diffs],
    :editor.eval.clj.print [:lt.plugins.clojure/eval-print],
    :deactivated [:lt.objs.style/remove-theme],
    :change [:lt.objs.editor.file/dirty-on-change
                     (:lt.objs.editor/on-change :declassify-behind-cursor)
                   :lt.plugins.auto-complete/intra-buffer-string-hints],
…}

Hence the change trigger on the editor will react using the in-change behaviour in this file. This fires the command that is passed in as an argument as expected.

The more interesting behaviour is the first one, which seems to be responsible for loading the JavaScript file that is passed as the parameter. You might expect this to happen at the time that the plugin is loaded, but how does it get triggered.

It took a while to find the answer. There is a special trigger object.instant-load, which causes the reaction to happen when an object associated with it changes – for example, a behaviour is added or freed. In the following example we can add this tag on one of our own behaviours, and then see that the reaction fires when a behaviour is added. Contrast this with the ::not-special behaviour which is not specially tagged, and hence executes only when the trigger event happens.

SpecialTriggers

This is used by the load-js behaviour on the app which is defined as part of the plugin definition file (as the last line).

LoadJs

It’s really clever that the editor is customised by adding and removing behaviours, which is in turn by reading and executing the configuration files (like the standard one). This data driven configuration looks very powerful and seems to work well inside LightTable. I guess the question is, how easy is it to use this mechanism if order starts being important when we are executing a number of reactions?

Posted in Computers and Internet | Leave a comment

Cast the fun

Another podcast has recently come to my attention – the HaskellCast podcast. The first four episodes are really good, and include discussion with Don Stewart on the practical application of Haskell, Simon Peyton Jones on GHC, the main Haskell implementation, and Simon Marlow on the work he is doing at Facebook.

In the first episode, with Edward Kmett, there was plenty of discussion about lenses, a pattern for making copies of immutable potentially deeply nested data structures while at the same time modifying some of the contents. This reminded me a lot of a generalised kind of Zipper. There is a tutorial here and an associated slide presentation here.

Haskell is full of interesting ideas, and it is fascinating to see all of the practical uses of what once seemed a more research kind of language. Sometimes, you don’t use the full set of facilities in the language – Don Stewart points out that often in practice, the laziness needs to be removed from the program by using strictness annotations, but that the language is great of implementing internal DSLs for the financial world. They’ve found it quick to train non-programmers for using Haskell to define mathematical models. The purity of the language seems to offer a lot of benefits – deterministic parallelism and “efficient” software transactional memory being two obvious benefits.

I’m looking forward to future editions of the podcast!

Posted in Computers and Internet | Leave a comment