Sunday, 26 June 2016

GEB

Douglas Hofstadter's Godel, Escher, Bach is one of my favourite books. Commonly referred to as GEB, this book is a mesmerising meditation on consciousness, mathematics and creativity. The central idea is that of a "strange loop", in which the same message is interpreted on multiple semantic levels.

GEB was the first place I came across the idea of a musical canon. A canon is a beautifully austere form of composition that was popular in the Baroque period. A canon consists of a dux part which sets out the base melody accompanied by a comes part which is some kind of transformation of the dux.

Here is the structure of a canon described using the programming language Clojure. f stands for the transformation selected by the composer.

(defn canon [f notes]
  (->> notes
       (with (f notes))))

For example, the comes might be formed by delaying the dux by a bar and raising every note by a third. In my talk Functional Composition I show how computer code can be used to explain music theory, focussing on JS Bach's Canone alla Quarta from the Goldberg Variations. Canone alla Quarta is an unusually complex and beautiful canon where the transformation is composed of a delay of three beats (a simple canon), a reflection (a mirror canon) and a pitch transposition down a fourth (an interval canon).

Here is the transformation from Canone alla Quarta written in Clojure. comp is a Clojure function for composing multiple transformations together.

(defn canone-alla-quarta [notes]
  (->> notes
       (canon
         (comp (interval -3) mirror (simple 3)))))

I was working on a talk for last year's Strange Loop programming conference (itself a reference to Hofstadter's work) and I decided that I wanted to create my own canon as a tribute to GEB as a finale. Rather than use an ordinary musical transformation for my comes, I wanted to pick something that spoke to the idea of composing music with computer code. I also wanted to incorporate GEB's theme of interpreting messages on multiple levels.

I took the letters G, E and B, and used the ASCII codes that represent these letters as though they were MIDI pitch codes. This gave me my dux. I then took the same three letters and interpreted them as the musical notes G, E and B. This gave me my comes. I had obtained a canon based not on musical concepts like delay or transposition, but on encoding schemes used in computer programming.

(defn canone-alla-geb [notes]
  (->> notes
       (canon
         #(where :pitch ascii->midi %))))

I elaborated the harmonies provided by this canon into a complete track, composed via computer code. The dux and the comes are joined by various other parts, some using polyrhythms to generate apparent complexity from underlying simplicity.

Eventually, the dux and the comes are accompanied by a third canonic voice, in which the names of Godel, Escher and Bach are read out by a text-to-speech program. So the theme of three notes G, E and B becomes a canon of three voices musical, technical and allusive to the three great creative spirits Godel, Escher and Bach.

Listen to the recording.

Read the code.

Watch the talk.

Sunday, 17 May 2015

Lanham on explicit data dependencies

Who's kicking who?

- Richard Lanham, Revising Prose

Tuesday, 20 January 2015

Korzybski on story points

The map is not the territory.

- Alfred Korzybski

Sunday, 19 October 2014

Types don't substitute for tests

When reading discussions about the benefits of types in software construction, I've come across the following claim:
When I use types, I don't need as many unit tests.
This statement is not consistent with my understanding of either types or test-driven design. When I've inquired into reasoning behind the claim, it often boils down to the following:
Types provide assurance over all possible arguments (universal quantification). Unit tests provide assurance only for specific examples (existential quantification). Therefore, when I have a good type system I don't need to rely on unit tests.
This argument does not hold in my experience, because I use types and unit tests to establish different kinds of properties about a program.

Types prove that functions within a program will terminate successfully for all possible inputs (I'm ignoring questions of totality for the sake of simplifying the discussion).

Unit tests demonstrate that functions yield the correct result for a set of curated inputs. The practice of test-driven design aims to provide confidence that the inputs are representative of the function's behaviour through the discipline of expanding a function's definition only in response to an example that doesn't yet hold.

All of the examples that I use in my practice of test-driven design are well-typed, whether or not I use a type system. I do not write unit tests that exercise the behaviour of the system in the presence of badly-typed input, because in an untyped programming language it would be a futile exercise and in a typed programming language such tests would be impossible to write.

If I write a program using a type system, I still require just as many positive examples to drive my design and establish that the generalisations I've created are faithful to the examples that drove them. Simply put, I can't think of a unit test that I would write in the absence of a type system that I would not have to write in the presence of one.

I don't use a type system to prove that my functions return the output I intend for all possible inputs. I use a type system to prove that there does not exist an input, such that my functions will not successfully terminate (again, sidestepping the issue of non-total functions). In other words, a type checker proves the absence of certain undesirable behaviours, but it does not prove the presence of the specific desirable behaviours that I require.

Type systems are becoming more sophisticated and are capable of proving increasingly interesting properties about programs. In particular, dependently typed programming languages like Idris can be used to establish that lists are always non-empty or the parity of addition.

But unless the type system proves that there is exactly one inhabitant of a particular type, I still require a positive example to check that I've implemented the right well-typed solution. And even if the type provably has only one inhabitant, I would still likely write a unit test to help explain to myself how the abstract property enforced by the type system manifests itself.

A type system is complementary to unit tests produced by test-driven design. The presence of a type system provides additional confidence as to the correctness of a program, but as I write software it does not reduce the need for examples in the form of unit tests.

Sunday, 12 October 2014

Hiding the REPL

I depend heavily on Clojure's REPL, because it's where I write music. Over time, however, I've become less focused on directly interacting with the REPL, and pushed it more and more into the background.

I use Vim Fireplace, which gives me the ability to evaluate forms in a buffer by sending them to an nREPL instance. There's also a REPL available within Fireplace, but I find I only use it for simple commands like stopping a piece of music or printing a data structure.

Speaking to Aidy Lewis on Twitter today, I've come to realise that there may be two different models for REPL-driven development.

Aidy described a model where the REPL is ever-present in a split-window. This brings the REPL to the foreground, and makes it conveniently available for experimentation. I would describe this as a side-by-side model.

On the other hand, I treat the buffer itself as my REPL. I write and refine forms, evaluating them as I go. If I want to experiment, I do so by writing code in my buffer and either evolving it or discarding it. My navigation and interaction are as they would be in any other Vim session, punctuated by occasional re-evaluation of something I've changed. This seems to me more like a layered model, with my buffer on the surface and the REPL below.

The reason I value this mode of interaction is it makes me feel more like I'm directly interacting with my code. When I make a change and re-evaluate the form, I have the sense that I'm somehow touching the code. I don't have a mental separation between my code-as-text and the state of my REPL session. Rather they're two ways of perceiving the same thing.

Saturday, 7 June 2014

Pragmatic people

She came from Greece. She had a thirst for knowledge.
She studied Haskell at Imperial College -
that's where I caught her eye.
She told me monads are burritos too.
I said, "In that case Maybe I have a beef with you."
She said, "Fine",
and then in thirty metaphors time she said,

"I wanna live like pragmatic people.
I wanna do whatever pragmatic people do.
Wanna sleep with pragmatic people,
I wanna sleep with pragmatic people like you."
Oh, what else could I do?
I said, "I'll see what I can do."

I showed her some JavaScript.
I don't know why,
but I had to start it somewhere,
so it started there.

I said, "Pretend undefined == null"
And she just laughed and said, "Oh you're so droll!"
I said, "Yeah?
I can't see anyone else smiling in here."

"Are you sure you want to live like pragmatic people?
You wanna see whatever pragmatic people see?
Wanna sleep with pragmatic people,
You wanna sleep with pragmatic people like me?"
But she didn't understand.
And she just smiled and held my hand.

Rent a flat above a shop,
Cut your hair and get a job.
Write a language in 10 days
and you're stuck with it always.

But still you'll never get it right,
'cos when you're debugging late at night,
watching errors climb the wall,
if you just used types you could stop it all, yeah.

You'll never live like pragmatic people.
You'll never do whatever pragmatic people do.
You'll never fail like pragmatic people.
You'll never watch Curry-Howard slide out of view.
Time flies like a Kleisli arrow
because your perspective is so narrow.

Sing along with the pragmatic people.
Sing along and it might just get you through.
Laugh along with the pragmatic people.
Laugh along even though they're laughing at you.
And the stupid things that you do,
because you think that proof is cool.

Like a dog lying in a corner,
faults will bite you and never warn you.
Look out they'll tear your insides out.
Pragmatists hate a tourist,
especially one who thinks it's all such laffs.
Yeah and the stains of faulty reasoning
will come out in the maths.

You will never understand
how it feels to live your life
with no meaning or control.
And I'm with nowhere left to go.
You are amazed untyped languages exist
and they burn so bright
while you can only wonder.

Why rent a flat above a shop,
cut your hair and get a job?
Dynamic languages are cool.
Pretend you never went to school.

Still you'll never get it right,
'cos when you're debugging late at night,
watching stacktraces 10 screens tall,
if you had types you could stop it all, yeah.

Never live like pragmatic people.
Never do what pragmatic people do.
Never fail like pragmatic people.
Never watch Curry-Howard slide out of view,
and on error resume,
because there's nothing else to do.

With apologies to Jarvis Cocker.

Sunday, 27 April 2014

Microservices relax

Recently I blogged explaining that I view microservice architectures as a collection of strategies to independently vary system characteristics. I suggested that these strategies could be framed in terms of a generic architectural constraint:
X can be varied independently of the rest of the system.
Mark Baker pointed out that while I employed the language of architectural constraints, my one "isn't upon components, connectors, and data." He referred me to Roy Fielding's excellent thesis, famous for defining the REST architectural style, for a rigorous description of how architectural constraints can be described.

Thinking about the problem further, I considered what kind of data flows through the microservice systems I've worked with. I realised that many of the qualities that characterise a microservice architecture are not visible during a single system run. Microservice architecture can only be explained in terms of components, connectors and data if the constituent services are themselves regarded as data, and the processes that evolve them as components and connectors.

I don't think that's too much of a stretch. For systems that are deployed via continuous delivery pipelines, the automated deployment infrastructure is part of the system itself. If the build is red, or otherwise unavailable, then the production system loses one of its most important capabilities - to evolve. The manner in which the code/data that specifies the behaviour of the system evolves can be subject to similar constraints to the introduction of novelty into conventional system data.

Viewed that way, it becomes apparent that the constraint I proposed was the inverse of what it should have been, namely:
X's variation must be synchronised with the rest of the system.
Monolithic architectures are subject to this constraint for various values of 'X'. Microservice architectures are produced via the relaxation of this constraint along different axes.

The process of starting with a highly constrained system and gradually relaxing constraints that it is subject to is the opposite of the approach Fielding advocates in his thesis. When deriving REST, Fielding starts with the null style and layers on six constraints to cumulatively define the style.

However, the microservice style is a reaction against highly-constrained monolithic architectures, so it has taken the opposite approach, which is to peel away constraints layer by layer in order to introduce new flexibility into the system.

For example, a monolithic system might consist of five functional areas, all integrated within a single codebase. For a functional change to make its away to production, the data describing the system's behaviour (its source code) is modified, checked-in and moves through the deployment pipeline into production. This must happen for all five functional areas as one, because the transaction of deployment encompasses all five pieces of data.

This system is devolved into a system of five microservices, each living in an independent source control root. A change to any one of those services can be checked in and move through its pipeline to production independently of the others. The deployment transactions are now smaller in scope, encompassing only a single service at a time.

The change in the scope of a single deployment generates options for the maintainers of the system. They can now release changes to one of the five functional areas without downtime to any of the other four.

But, as is the case with real options, this comes at a price. If the five areas interact, their APIs need to be versioned and kept backwards compatible. Changes that crosscut multiple services need to be carefully orchestrated to avoid breaking changes, whereas in the original monolithic system such refactorings might have been made with impunity.

Generally speaking, for each constraint that is relaxed in a microservice architecture, there is a corresponding real option generated and a corresponding coordination cost incurred. For good explanations on real options and how they apply to software development, see the various works of Chris Matts, including the book he wrote with Olav MaassenCommitment.

I think that it's a productive approach to describe microservice architectures in terms of the the relaxation of architectural constraints relative to a monolithic architecture. This provides us with a model not only to analyse the runtime properties of the system, but also its evolution and the options it affords its maintainers.