Peter G. Hancock

Writings

This webpage leads to various writings that I wanted to collect together and make available. There is also a mausoleum of more elderly things, currently in a random state. Some links might eventually work.

The main topic is programming and type theory, but there might some recreational things:

Some musical things that amuse me.
Some sayings and phrases that amuse me.

As for programming:

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.

I am interested in the interplay between arithmetic and logic, particularly in type-systems. By arithmetic I mean anything that smells like arithmetic, including the arithmetic of transfinite ordinals.

2018: The predecessor function of elementary arithmetic and related stuff

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.

May 2016: arithmetic combinators and logarithms(pdf)

I put this on a github page. AMEN However I seem to have lost update access due to recent changes at github.

Here is some Haskell : code for running the evaluator mentioned.

Here is a May 2016 talk on this topic. (This was an exercise in playing the fool.)

Aug 2015: church numerals and lenses (html)

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.

Oct 2015: substitution calculus (pdf)

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

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.

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.

PGP