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 topic is 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.
- type theory for me concerns 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.
- 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 predicatively seems to require a universe, or better, a universe operator that can be iterated. This is all in a state of flux.

I put this on a github page. AMEN

Here is a May 2016 talk on this topic. (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 a nice solution. I'm very interested by IR. I hope to improve my understanding of it, enough to express 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.

Last modified: Mon Apr 2 12:12:58 BST 2018PGP