|
This is our 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 = Y*D(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.
Newton's FingerThis is our 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 = Y*D(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.
Conor McBrideUniversity of Strathclyde Conor is a previous alumnus of Cambridge who went on to complete a PhD in dependent type theory at Edinburgh University. He now works at the University of Strathclyde where he continues to work on functional programming and type theory. Some examples of the work he has done include finding links between calculus and types, and the development of the dependently typed language Epigram. His well known papers include ‘Clowns to the left of me, jokers to the right’ and ‘Do Be Do Be Do’.
|
