Abstract

This is CUCaTS’ first talk of the year, presented by Dr Conor McBride! The talk title is ‘Newton’s Finger’ and will explore the relationship between Newton and Leibniz derivatives and computer data types, it should be a very interesting talk regardless of background knowledge! As always, we will be heading to the pub after for free drinks, so don’t miss out :)

Newton’s notion of “divided difference”, D(F)(X,Y) = (F(Y) – F(X))/(Y-X) makes perfect sense for container-like data structures, F(-), even in the absence of “subtraction” or “division”. We may rather consider solutions to the equation (or type isomorphism)

F(Y) D(F)(X,Y)X = YD(F)(X,Y) F(X)

which witnesses how to travel “left-to-right” through an F()-structure, gradually turning Ys into Xs. D(F)(X,Y) represents a snapshot in the process, where there is a finger over a place where a Y has been removed but an X has yet to be inserted, but there are Xs “left of the finger”, and Ys “right of the finger”. Just as various limits of the divided differnce play a useful role in mathematics, so the same limits have computational meaning. Leibniz’s derivative F’(X) = D(F)(X,X) gives the type of “one-hole contexts” for an X in an F(X). Meanwhile, D(F)(0,Y) (i.e., nothing left of the finger) gives a formal notion of “division by Y with remainder F(0)”, but also plays a vital role in Brzozowski’s differential analysis of regular expressions. Lastly, D(F)(X,1), also known as “Fox’s free deriviative”, captures F() structures under construction, with stubs right of the finger, in place of values not yet computed.

In any functional programming language that treats datatype descriptions as first-class notions, we can just do the mathematics and extract the functionality in general, once for all.