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.
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 2018