R.I.P. Robin Williams

The pejorative most often thrown Robin Williams’s way was “sentimental”. Dead Poet’s Society is sentimental; Good Will Hunting was sentimental. The Fisher King is a hugely sentimental confection (although Terry Gilliam has quite a lot to do with that).

Often what Williams was portraying was deep loneliness; and lonely people have sentimental turns. Commonplace words like “love” and “acceptance” get capitalised, become the Love and Acceptance on which entire worlds pivot. You make a big deal about these things because they’re difficult, elusive, never quite seeming to work out; redemption can happen in fantasy at least (although the fantasy itself is not redeemable).

I think his work will bear rewatching with an eye to its strangeness, its estrangement. Jumanji, already a weird and troubled film, gets considerably weirder when Williams emerges from the box, a lost child grown adult. Even the aggravated kookiness of Mork and Mindy jaunts along over an ostinato of disconnection and anxiety (Mork is an outcast from Ork, a misfit wherever he finds himself). It is not easy to live in this world.

Can it really be true, as wikipedia reports, that the landlord of Fred and Mindy’s music store was named “Arnold Wanker”?

A Moldbuggian Howler

When it comes to being whizz at programming, Moldbug fails the basic comprehension test:

“Even forgetting the macros, it’s pretty easy to see why you don’t need dynamic higher-order programming. For example, a very common operation on functions is to compose them – you have f(x) and g(x), you make h(x), defined as f(g(x)). In the right formal model, a compose operator is really no different from addition. And once you have first-class functions – which are not absolutely necessary, but certainly useful – it seems like a trivial extension.

But is it what you, the programmer, want to do? Actually, no. It is simply bad programming style. Its only effect is to make your program less comprehensible.

Because in a language with first-class functions but without dynamic higher-order programming, all you need to do is build a data structure which is the ordered pair (f(x) g(x)), and define h(x) as an operation on this structure. This may be slightly more cumbersome for the programmer. At least, if one line of code counts as ‘slightly more cumbersome.’”

No. That is not how function composition works.

I will now briefly try to describe why this is wrong, why it is elementarily wrong, and why Moldbug is both a n00b and a scrub.

Let’s say we have two functions, f : List a -> Int and g : Int -> Int. f takes a list and returns its length; g doubles the integer passed to it. We wish to compose both functions to make a new function, g . f = h : List a -> Int, which takes a list and returns double its length.

Suppose we try to do as Mr Yarvin proposes, and create an ordered pair (f(x), g(x)). f(x) will take a list, x, and return its length. g(x) will take an integer, x, and return x*2. We cannot pass the same x to both f and g, since no x can be both a list and an integer (not even in Python!). There is no therefore no way to construct this ordered pair.

The function h does not in any case take a pair of inputs. It takes a single input, a list, and returns a single output, an integer.

Function composition works by chaining functions together, so that the output of one becomes the input of another. If we wanted to apply a function h to the outputs of both f(x) and g(x), the “composition” operator would have a completely different signature, viz:

compose’ : (a -> b) -> (a -> c) -> (b -> c -> d) -> a -> d
compose’ f g h x = h (f x) (g x)

Which is also, nota bene, a damn sight easier to write and use if you’re using a sensible language that handles partial application properly. And nobody, literally nobody, calls it “dynamic higher-order programming”. Not least because it’s all worked out at compile-time anyway.

Reasons of Space

Cover of "The Production Of Space", by Henri Lefebvre
It’s mostly made in China these days

“The logical space of reasons” is a figure of speech, and a telling one. C20th philosophy is full of phase spaces and logical spaces, rhetorical spaces and epistemic spaces, from Wittgenstein’s Logische Raum and Heidegger’s Spielraum through to the smooth and striated spaces of Deleuze & Guattari. Spatialisation is one way to “go transcendental”: the movement from point to space is always a virtualising movement, a movement in the direction of overarching (rather than “underlying”) logic, higher-order organisation.

Henri Lefebvre’s argument about spatial metaphors is, more or less, a reworking of Merleau-Ponty’s phenomenological centreing of spatial intuition on the body: for “the body” as that of an individual phenomenal subject, Lefebvre substitutes the social body. For Lefebvre, the contouring of “mental space”, with all its various metaphorical deployments in philosophy and mathematics, is consequent upon the structuring and restructuring of social and geographical space, in particular the space of the city. One could always see Lefebvre’s own project of tracing shifts in the structure of social space as outlining a kind of space of spaces within which such transformations could be plotted; but that would seem somewhat against the spirit of it.

The critical question here concerns the status of the transcendental, relative to the social (and historical, geographical, physical etc) matrix of which it is the transcendental. A “logical space of reasons” might be one sort of thing in a city where argumentative cliques congregated in coffee shops and bars to debate the latest pamphlets and manifestos, and another in a remote village with a primarily oral culture, where collective decision-making and tribal identity were mediated by the same stock of stories and story-tellers. Or – and the use of “space” as metaphor predisposes us towards this alternative – we might be trying to talk about differently-situated instantiations of the same thing, transcendentally speaking.

The key notion that I draw from Zalamea’s metaphorical deployment of sheaf theory is that there is not one “space of reasons”; that the transcendental is only available on condition that one navigates from space to space, constructing “spaces of spaces” through transcendentalising operations. That is why it makes sense to me to argue that the space of reasons is not a “full body”, and is in fact incompletable. There is not an independent space of types, governing a subordinate domain of values: type and value are inextricably entwined.

Two rationalist subjectivities

Reason is not the already-accomplished apparatus of rationality, and the space of reasons can never be laid out in its totality under a single gaze. In short, it is not a “full body”, sufficient and all-comprehending.

The Pigtronix “philosopher king” guitar effects pedal.

Neither can a “rationalist project” be oriented by the thought of one day completing rationality, or take the measure of its accomplishments based on their perceived proximity to such a goal. Rationality is locally perfectible – there exist problems to which there are solutions, and even classes of problems to which there are general solutions – but not globally: there is no universal procedure which will render every circumstance as a problem to which there is a solution.

There is no end of phrases, and no end to the task of linking phrases together.

The obscure subject of a rationalist politics will be that which, in the name of a “full body” of accomplished (or to-be-accomplished) rationality, calls for everything to be restored to order. Society organised according to geometric principles! Its speech purged of fallacies, its politics free of antagonism…

We know that such an obscure subject must devote itself increasingly to destruction, culminating in a frenzy against the real. Only the destruction of error can restore the integrity of the full body; and there is no end of error.

The faithful subject of a rationalist politics will be that which proceeds by proofs, which is to say by logical invention. To trust in reason is to trust in a generic capacity, without any guarantee drawn from the particularity of this or that person or community. It is to trust in the next step of the proof, without the certain knowledge of the world’s approval (reason can still scandalise the world).

The obscure subject has no need of fidelity, since there is literally nothing left for it to prove. All that remains is the identification – and consignment to perdition – of the infidel.

It is by no means the rationalist orientation in politics that has generated the most ferociously indiscriminate instances of this subjective figure.

Idris homework: tabulate

When Conor McBride sets you homework

The problem given is to write (in Idris) a function satisfying this signature:

That is, given a function that will provide a value of type a for every value of type Fin n, construct a vector of all the possible outputs of this function.

We might think that in order to do this we have to generate all possible inputs to the function – the range of possible values of Fin n. It is of course possible to do this, but the approach I’ve taken here is slightly different.

Let’s start with the “zero” case. A function (Fin Z -> a) can accept no input, as Fin Z has no elements. The tabulated vector of its outputs will therefore be empty:

What about a function (Fin 1 -> a)? There exists only one value of type Fin 1, fZ {k=1}. We can therefore construct our vector like this:

Ideally we would like to generate the right-hand side through a recursive call to tabulate, but that means we need a way to convert Fin (S Z) -> a into Fin Z -> a. Let’s write that function in its general form:

weaken is defined in Prelude.Fin, as follows:

So we can now rewrite the case where n = S Z like this:

Nearly there! Let’s try the more general case:

We can’t just use fZ every time – what we need instead is to pick a value of type Fin n for each value of n. The obvious thing to do is to take the “last” element, rather than the “first”. Again, this is defined for us in Prelude.Fin:

So that gives us:

My only hesitation here is that Conor said this was an easy exercise. Is the above really the simplest way to do it?

(edit: see the comments!)

Finally, here’s elements rewritten to use tabulate:

Again, I’m not sure whether this explicit definition of fins is necessary, or whether it could be expressed more concisely.

Idris notes: Fin

I’m trying to get fluent with Idris. It’s hard – but really interesting – but really hard. As often happens with these things, you gain a little ground in understanding only to find that just beyond the perimeter of your knowledge is a steep cliff face. Every so often you look down, and realise the ground isn’t there…

Picture of Idris Elba
No, not that Idris.

My first stumbling block has been that the signature and constructors for Fin are pretty weird.

The concept is not all that hard. Fin n is an abstract finite set of cardinality n. It’s not a container type, like Set a. The set “is” the type; values of the type are elements of the set, which as far as we’re concerned aren’t anything in particular – think of the “dots inside a circle” notation used by Lawvere to denote abstract sets. We’re not interested in what’s “in” a finite set, we’re just interested in its being of a bounded size.

A value of type Fin n is one of n elements – but which? This is where the constructors come into play, by introducing an ordering on these elements like that of Nat, the type of the natural numbers. There’s a Peano-like encoding on the naturals: Z = 0, S Z = 1, S (S Z) = 2 and so on. Similarly, here, fZ is the “zeroth” element of a finite set of size k+1 (it has to be k+1 so that we don’t try to construct an element of an empty set). fS Fin k is then the “successor” element of an element of Fin k, and has the type Fin (S k).

This is a bit odd. Suppose we have fZ {k=4} – the zeroth element of a finite set of five (4 + 1) elements, which has the type Fin 5. fS (fZ {k=4}) is then the successor-to-zeroth element of a finite set of six elements, having the type Fin 6 – in order to obtain the “next” element, we’ve also had to grow the type. On the one hand, this means that we can never obtain a “next” element outside the bounds of a finite set; but on the other, it means that a successor is always “added” to a finite set, rather than simply located within it.

Suppose we wanted, given a bound n : Nat, to generate a vector of size n containing all the values of Fin n. What would that look like?

%d bloggers like this: