This webpage leads to various things I have written, that I wanted to collect together. The end of this page has recent things. There is also a mausoleum of more elderly things, currently in a random state. Some links might eventually work.

The main topics are in type theory and programming, but there might be something about music.

- programming = devising programs that communicate in a specified way with their environment. For example, via streams, or a command response interface.
- the topics in type theory concern mostly dependently typed systems in Martin-Lof's style, and the mathematical theory of such things.
- Some musical things that amuse me.
- Some sayings and phrases that amuse me.
- The gas is the pdf just mentioned.
- The code is here:.lhs. It is essentially a rewriting calculator, and the main thing it does is display a reduction sequence for a given term (by typing in to ghci something like "test $ ... :^: vy :^: vx :^: some-expression"). A number of useful combinators (like "cS" for the S combinator are defined in the file -- sadly, you have to browse around looking for them). I often use the calculator to check equalities: just apply the terms of interest to sufficiently many fresh variables, and observe the reduction sequences. There is a pdf presentation here: .pdf, but things are not very polished yet.
- a notion of type-family indexed over a given type, besides the usual notion of object of a type.
- named variables in contexts, substitutions, and context thinning.
- dependent function-/pair-types Pair-types can be generalised to record-types, with named projectors, perhaps. With pair types there are just the 2 names "0" and "1". The idea is that an ordered pair should be defined by its successive projections, where the type of the second projection may depend on the value of the first one. Pair-types should be thought of as limits
- A ground type family, that may be empty or something more interesting, like a `hosted' type-theory. (o,i).
- There is also some discussion of `self-hosting' logical frameworks.

Some recreational things:

In connection with "lenses" (in my sense below), I have been looking at the predecessor function. There is some ongoing work in this (Haskell) file , as well as an (Agda) file mentioned below as well.

My interest is that the predecessor is mildly tricky to define with Church numerals, and very tricky to explain. "The less said about this, the better", to quote John Hughes. (To be convinced, one can look at this Wikipedia page, and see the notes of notes of Oleg Kiselyov.) The predecessor seems to share some of the mystery of the exponentiation function, in that it involves a certain change-of-carrier (a non-trivial lens). To treat tetration and cut-off subtraction seems to require a universe of pure types got by iterating an set-of-endomaps operator. (It is easy if one uses impredicative Church numerals, as in system F: the point is to accomplish the encoding predicatively.)

Yet another angle of interest is that the trick used to encode the predecessor really supports the definition of related operators, like the one that pushes a given number "on the front" of a given function. That is to say, it supports the "cons" operator of the type of (countably) infinite streams (at least, of numbers). Some interesting things lurk in the arithmetic of such streams.

10ish .pdf pages. I have extracted the executable code from the source of this file, and am in the process of polishing up the two parts: gas and code.

What is odd is that besides 0, there are special "numbers" ((^),(*),(+)) that represent the arithmetic operations they indicate, via exponentiation. Together, these "numbers" suffice to support variable abstraction: amazingly, this turns out to extend the ordinary laws of logarithms.

Here is a May 2016 talk on this topic. (It is desperately difficult to be funny about mathematics, or indeed anything. This was an exercise in `playing the fool'.)

Some Agda code exploring "lenses" in my sense. This sense has nothing to do with Benjamin C. Pierce's bidirectional programming, as far as I know. It is more to do with lens (banana)-brackets and is an Archimedean metaphor for (visual) magnification. I might change the metaphor to levers or pulleys, if the words can be found to fit.

The notion I call a lens implements a function (eg `(2^)`) on the natural numbers (or `(omega^)` on the countable ordinals) using an operation (eg `endo X = X -> X`) on algebra carriers, with accompanying structural operations on algebras. For example `(0,(+1))` is altered to `((+1),twice)` -- where `twice` composes a given operation with itself; then values in the original carrier are recovered from values in the higher type carrier using `(f |-> f 0)`.

Sometimes I try to find a way to encode Michael Rathjen's notations for the provable ordinals of KPM in a form of type-theory based on inductive-recursive (IR) definitions. This is essentially a solved problem, due to Anton Setzer, but I want an elegant solution, where elegance means in the eyes of a programmer: simple, short, fitting together like unfussy, beautiful clockwork. I'm very interested by IR. I hope to stress-test and improve my understanding of IR, by expressing the various ingredients of "Mahloness" as respectable dependently typed IR-based code.

A few pages making completely explicit all judgement forms and rules for a type theory with

Something so large always has bugs. I am not 100% sure I have all the rules, and whether they are in the right order, or even exactly how to tell.

There are 10 judgement forms and depending on details of the formalism roughly 100 rules, modulo some smallish factor. The first version of Martin-Lof's theory of types I saw was astoundingly beautiful and simple. The essence of the whole thing could be summarised in perhaps 4 or 5 rules (most beautifully, V : V). Nowadays his theory of types is still astounding, but for its intricacy. It doesn't compare at all badly though with other programming languages in this respect.

Last modified: Sun Aug 20 12:35:22 BST 2017PGP