Edward spent most of his adult life trying to build reusable code in imperative languages before realizing he was building castles in sand. He converted to Haskell in 2006 while searching for better building materials. He now chairs the Haskell core libraries committee, collaborates with hundreds of other developers on over 150 projects on github, builds tools for quants and traders using the purely-functional programming-language Ermine for S&P Capital IQ, and is obsessed with finding better tools so that seven years from now he won’t be stuck solving the same problems with the same tools he was stuck using seven years ago.
YOW! West 2016 Perth
There are a lot of algorithms that revolve around iterating a form of information propagation until it attains a deterministic fixed point. CRDTs, Datalog, SAT solving, functional reactive programming, and constraint programming all fit into this mold.
One framework for these sorts of algorithms is the notion of a “propagator” due to Sussman and Radul, but until now little rigor has applied to know how such algorithms terminate with consistent results.
Another framework is Lindsey Kuper’s work on the notion of “lattice variables” (LVars), which addresses termination, parallelism and eventual consistency well, but not iteration.
By blending these frameworks, I’ll build up a series of sufficient conditions for propagators to terminate with consistent results and proceed to show how we can use this common framework to steal insights and quirks from each individual domain to try to optimize the rest.