Erlang Factory SF 2016 - Keynote - John Hughes - Why Functional Programming Matters

okay so thank you very much for the invitation in the introduction Francesco it's a great pleasure to be here today and actually my my paper that Francesco talk so nicely about that was published a little over 25 years ago so it's been a long time but when Francesco asked me to come and give this keynote he actually invited both me and my wife Mary Sheeran so Mary is also a researcher in functional programming there are no side effects in our household and our son is a haskell enthusiast believe it or not so the first time the first version of this talk we gave together in London and there is not able to be here today but nevertheless quite a lot of what I'll be presenting has to do with her experiences as well so what I'm going to do is I'm going to give a kind of whirlwind tour of some of the important ideas in functional programming pick out some of the landmark papers but also point to some of the work that has inspired myself and Mary over the years so it's a kind of personal retrospective on functional programming so of course my paper 25 years ago is not the start of the subject not at all functional programming dates back to the 1940s but back then it was rather different back then functional programming was very minimalist for example early UNS who Needham what can you do with a boolean all you can do really is make a choice well we can define functions to do that so let's define true and false to be functions that make choices if you're going to make a choice you have to have two things to choose between so let's give them two arguments and now we'll just say that true is the function that chooses its first argument and false is the function that chooses its second I'm going to use Haskell notation here a lot of the talk so this is just function with two arguments X and returnee X I hope that it's familiar enough that there won't be any problem understanding it so if we define billions like this then we can define if-then-else as a function here it is what does it do it takes a boolean and are then branch and an else branch and it just calls the boolean and uses it to make a choice between the then and else branches so that's great we don't need boolean how about that well what else might you want in a programming language maybe numbers integers but who needs those really I mean what is an integer for I'm going to talk about positive integers here but what is an integer for if not counting loop iterations so why don't we define integers just to iterate a loop so many times let's define to to be a function that takes a loop body F and a starting value X and just calls F twice so we execute the loop body twice and then one of course will execute it once 0 will execute at 0 times and so on and there we are we don't need numbers we have functions instead and if we want to recover a normal integer from a function it's easy to do so if these are defined in Haskell then I can turn the function 2 into the Haskell integer 2 just by iterating a loop body that adds 1 starting from the integer 0 so you can see that all of the information is in these functions I'm going to be able to extract integer values from them again and if I make that call I'll get the Haskell integer 2 as the result ok so I can represent integers as functions but can't I do things with them what do you want to do with it's just add them together for example how will I add two integers well I need to execute my loop body n plus n times and I can do that by first executing it n times and then executing it M times on the result so ad NN is a function that takes a loop body F and a starting value X and it iterates the loop n plus n times I wonder if I can do multiplication how could I execute a loop body n times n times how about nested loops if I have an inner loop that calls F n times and an outer loop that calls all of that M times that in total I'm going to execute F M times n times so that's great this gives me a way of adding and multiplying these functions that represent numbers does it really work well we can just type into the haskell repple add one multiply two by two that should give us five right and if i use that to iterate the increment function start from zero sure enough I get five so we don't need integers either in our programming language so here's the factorial function I'm sure you've all been waiting for it the factorial function Allen 1940 so what does it say well factorial of n if then else if n is zero we get one otherwise we multiply n by factorial of decrement n does it work here's factorial of 5 so we can construct that function which should iterate the increment function 120 times and yes it works now there's a couple of auxiliaries that still need to be defined here like is 0 how can I tell whether a number is 0 well what I do is iterate a loop body that returns false n times starting from true so if there are 0 iterations I'll get true if there's more than 0 iterations I'll get false so that's my is 0 function and the other one I had was decrement the less said about that the better but you can do it so there we are we see that boolean z' integers and actually I have not shown you this but also any other data structure can be represented entirely by functions and the man who discovered this was Alonzo Church these things are called Church encodings so why did it church want to do that well excuse me Church wanted to show that functional programming could be a foundation for mathematics but you didn't need anything else to build up you know all the rest of mathematics in particular you could create billions numbers and so on so he had a theoretical interest in this but actually early versions the Haskell compiler represented data structures this way not integers of course that would be silly but data structures were represented by Church encodings and there was a man called Yann Fairburn who tried this out first he wrote his own functional language compiler he had some new ideas generate very good code but he didn't have an implementation of data structures so he just used the church encodings and then he could write programs on lists and so on and they all ran fine at one day he decided that pyro was getting sufficiently good that he should really do the work and implement data structures properly he did that and the code went slower so this this used to be the fastest way to implement data structures that's why the Haskell compiler used to do it it's not true anymore because when you run these programs you're calling dynamically constructed functions the whole time so it wreaks crews totally with branch prediction but back in around about 1990 branch prediction wasn't so important and so this was the fastest way to implement data structures if you want to try this at home I should warn you I've shown you Haskell code and it all works but if you just type in exactly what I've typed you get a type error the type checker says there's a curse check we can't construct an infinite type okay that sounds bad but it's not entirely clear is it why it's trying to construct an infinite type luckily the type checker tells it gives us a lot more helpful information so it tells us the type it was expecting and the type that it got and this is actually the first time I've had a chance to use a three-point font on a slide now I realize that this information may be a little bit daunting but don't worry there's more these are the types of all the local variables so you can't just type this stuff straight into a Haskell compiler you have to give the type checker a little bit of help and what you have to do is tell it the type of the factorial function you can do it like this now here the black stuff that's all stuff that the type checker would be able to figure out for itself the bit in red the for all it can't so you have to tell it that if you want to try this otherwise everything just works okay so this was functional programming in the 40s so Alonzo Church could have a lot of fun writing functional programs but he couldn't actually run them it's a bit of a bummer and that wasn't possible until 1960 when John McCarthy implemented the first version of Lisp so here's the factorial function in Lisp and it looks jolly similar label means it's a recursive function and we got a lambda n then cond as if then else in Lisp and so on looks quite familiar apart from all the lovely parentheses and this was really very advanced it also had higher-order functions so a function called mapless that nowadays we call map and you could map the factorial function down the list one two three four five and get the list of factorials so you could start doing some real functional programming around about 1960 and at that time functional programming among and theoretical computer scientists began to become very very popular so church had already shown that you can implement numbers by functions McCarthy show that you could implement Lisp by functions and Christopher Strachey actually began a whole program of work to show that you could implement any programming language by functions so what he was doing basically he was writing an interpreter for any programming language in the lambda calculus and using that as a way to define what programs meant and that started a whole branch of programming language theory that continues to this day but I want to skip ahead a little bit to 1965 when a landmark paper was published called the next 700 programming languages by Peter Landon univac and I'm just going to read you the abstract of the paper which says today 1,700 special programming languages are used to communicate in over 700 application areas Landon thought this was rubbish he thought that it would be much better to have 700 instead of 700 programming languages just one programming language with 700 libraries for the different application areas so quite a modern idea and of course he thought that one programming language should be his programming language which he called I swim it sends what if you see what I mean and I swim has been a great influence on many functional programming languages that followed here's the factorial function in I swim but what I really want to emphasize about this paper it's not just a language it's the emphasis that Peter Landon put on laws what do I mean by a law well I mean an equivalence between two different programs that tells us that you can replace one by the other here's a law about Lisp programs okay if you take a list and you reverse it and then you map a function over that that's the same as first mapping the function over the list and then reversing the result well it's kind of the same it's the same provided F doesn't have any side effects which list functions can have so you often this will be true but not always Landon believed that laws are there to be followed and that it's important for programs satisfy laws like this without exception so he actually discusses in the paper that you might think what's the point of having two different ways of doing the same thing wouldn't it be better if these two programs did something different because then you could choose which one you wanted land in thunders no expressive power should be bid by design rather than by accident yes mr. Landon so he put this really strong emphasis on simple laws relating things in programs that's something that has continued in functional programming ever since so now I want to skip ahead more than ten years to another landmark paper by John Backus John back has won the Turing award in 1977 okay who is John Backus well everybody's heard of BNF right Backus normal form he invented the notation that we use for grammars but that's not what he got the Turing Award for he got the Turing award for developing the first Fortran compiler now by the time he got the award in 1977 Fortran was the most widely used programming language it was the programming language that all programming language people loved to hate because it was just so old-fashioned and full of mistakes but when one shouldn't let that affect one's understanding of what a huge huge contribution the first Fortran compiler was so when the Fortran compiler was written nobody cared about programmer productivity or elegant programs of any ready that nonsense the only thing people cared about was performance in those days there were still people who thought that assembly language deprived you of that close connection with the machine that you need to write efficient programs because you could no longer reuse bit patterns from instructions as data if they happen to be the right value and the reason the Fortran compiler was a success was the first successful high-level language was that it could consistently generate code better than a human program group program it could write so you know we owe the whole development of high-level languages to John Backus now when you get the Turing award you get to give it your award lecture and you can publish a paper about it and of course John Backus could have written about how wonderful Fortran was or all of the clever things they did to make the compiler so successful but he chose not to he chose to write about his new love functional programming and his paper is a manifesto for functional programming and I can't overemphasize the impact that that had if be honest Rao struck where to stand here today and say it was all a mistake I should have designed Erlang that would not have the same impact as John boxes Turing Award lecture the man who gave us Fortran said it's all wrong we should be doing functional programming instead and this paper inspired a generation of researchers to work on functional programming including myself if you haven't read this paper Google John Backus Turing Award today the PDF is the second hit it's something everybody should read at least the paper is in two halves the first half is brilliant the second half are some other ideas that haven't had the same impact but the first half of that paper is something everyone should read I'm just going to quote a little bit from the introduction to the paper conventional programming languages are growing ever more enormous but not stronger back is as thinking of languages like ADA here C++ were not was not even a glint in Strauss or die at this point inherent defects at the most basic level cause them to be both fat and weak you see it's great stuff asthma it's during their primitive word at a time style of programming inherited from their common ancestor the von Neumann computer so yeah what was he talking about he explains that a computer has three parts a central processing unit a store and a connecting tube that can transmit a single word between the CPU in the store and he says I propose to call this tube the von Neumann bottleneck next time you buy a computer don't ask how fast the bosses ask how fast the von Neumann bottleneck is so he was dead against word at a time programming their inability to use powerful combining forms with building new programs from existing ones what's he talking about here I'm going to show some diagrams to illustrate this idea so I'm going in these diagrams the boxes are going to represent functions and they're going to take inputs from the right and generate outputs on the left so Backus was interested in forms for putting functions together into more complex functions for example what he called applied to all and wrote alpha F which replicates the function once for each element of a list we'd call this map this was one of the combining forms that he proposed so that would just map all the inputs in a list two outputs here's another one if you've got four different functions F 1 2 F 4 then you might make what back is called construction you put them together to get a function that will take its input distribute it to each function and then collect the results in a list so that was another form that he proposed their lack of useful mathematical properties for a reasoning about programs what kind of property is he talking about well let's look at the diagram again here is what Backus would write as a construction of F 1 to F n composed with G that dot is function composition if you think about it that's going to produce the same results as this right it doesn't matter whether you apply G to the input first and then distribute it among the FS or whether you distribute the input first and then in each component of the construction apply both the F and the G so those two programs are equivalent here's another one this is map air for alpha F composed with the construction and that dotted line there illustrates how I've divided up the description of this program in syntactically but of course it's the same as this in which we have a construction of four functions each of which composes F with one of the genes so what you see here is two of backus's laws about his combining forms so he's emphasizing laws just like Peter Landon did but now they're they're laws involving the combining forms that he was proposing so let's look at an example of a program in backus's language FP first of all here's an Algol 60 program for computing the scalar product of two vectors and you can see it's word at a time we pick one else at a time from each array and multiply them together and add them up so Bacchus would write this instead like this where the scalar product takes a pair of vectors transposes them into a vector of pairs applies multiplication to all the all those pairs and then adds them up using insert plus and insert is what today we call fold are actually backers wouldn't write it like this you'd write it like this I think you had a little bit of APL Envy but he wanted his notation to be very very concise and powerful so let's say this was a landmark paper who had a huge influence on people working in the field so now I want to move on to the early 80s and another paper that perhaps isn't so well known but I think illustrates the ideas of functional programming very very nicely paper called functional geometry by this man Peter Henderson remember that name so Peter was actually Mary's PhD supervisor so we saw this work quite closely and Peter had two loves functional programming and the art of MC Escher there you see what an example of one of Ash's woodcuts I think and this one is called square limit and it's got a collection of fish who kind of get smaller and smaller and smaller towards the edges of the picture and Peter was fascinated by the recursive structure of pictures like this and he wanted to be able to construct them by writing functional programs but in those days if you wanted to do graphics you would write the sequence of graphics commands for you know drawing the line sequence and so on very much word at a time we didn't want to do that he wanted to work with a whole value with a picture as a value for example this picture let's call this one fish and if you can treat the whole picture as a value then you can start defining combining forms for putting them together and this fish actually fits very nicely together with itself so here's a fish overlaid on a double rotation of the fish the rotation is through 90 degrees so double rotation is 180 degrees it turns the fish upside down as you can see they fit together nicely if polishers genius and this fish you can actually also fit it together if you rotate it through 45 degrees and make it a little smaller so fish to here is that that top fish that's been rotated 45 degrees and fish three is the one on the right hand side that's been rotated 270 degrees anti-clockwise and then you can overlay all those together and you get this little tile with a big fish and two smaller ones you can even take that smaller fish and put four of them together you just overlay fish two with one rotation two rotations and three rotations four copies you get these nice four fished the might fit in the middle of that picture and Peter went on to define various operations for putting picture together like quartets takes four pictures P Q R and s put them together in a square or cycle that takes a picture and makes three rotations of it and put those together in the square and using those you can go on to make fish pictures of your own like this one for example this is a cycle of a rotation of that little picture with three fishing and why not make a quartet of those so you dislike a sure wallpaper so peter plate of these things these are not actually from Asher's print but there are similar things but but what about the print well to make the print you need to have small fish at the edge and Peter realized that it could take that little tile with three fish in and put it together in a quartet with two empty pictures and you get something that looks as though it might fit along the edge of the picture except you'd really like to make those fish get even smaller so let's call this picture side one and then let's just put two smaller copies of side one in the two blank spaces and so on and so forth and if you keep doing that you're going to get these fish getting smaller and smaller and smaller and smaller towards the side of the picture you got to do the same thing with a corner so you can take this tile and then call that corner one and fill in the blanks with a smaller corner and the side and a rotation of the side and keep doing that and you get corners that extend further and further towards the edge if you keep doing this finally you can build up the whole square limit picture by making an on edge he called it that's nine pictures arranged in square when you combine the corner and the side and rotations or the corner and rotations at the side and in the middle you have the one of the tiles I showed you with four fish there it is so Peters paper shows how to draw this picture using functional geometry there's Escher's print pretty good huh so this was very very elegant and but there's one thing Hatton told you of course Peter had to represent the picture somehow let's see how do you think he might have represented a picture wait a function of course so what he did and this was this was very clever Peter represented a picture by a function that given three vectors a B and C would return a list of drawing commands that would draw the picture in the blue box that those three vectors define and this was very clever because it made it very simple to define the operations for putting pictures together for example he's here's how you overlay P on Q you take your three vectors a B and C you draw P in the Box you draw Q in the box and you just combine the drawing commands that you get here's how you put P beside Q okay so if we want to draw pbu in a blue box defined by these vectors we split the box and then we say draw P but we give it B over 2 as its you know to define its box and we draw Q starting from a plus B over 2 so we give the vectors that correspond to the two halves of the box and draw each picture in the right place and you can even rotate pictures this way okay so if P would be drawn in this box how do you rotate it well you you give it that box on the right where you've moved point of origin over to the bottom right corner and then you have to give minus B to make it draw in the same space so that's also very very simple and that made these operations both easy to define and easy to prove things about which Peter also wanted to do so here's a law about the picture operations I haven't shown you above but you can imagine what it does so if you put P above Q and then rotate that's the same as rotating P rotating Q and putting one beside the other and there are many laws of this sort in the paper why did Peter care he says like Landon it seems there's a positive correlation between the simplicity of the rules of the laws and the quality of the algebra as a description tool in other words he used these laws as a touchstone for the design if he thought of an operator on pictures but it didn't have any nice laws he would think again and I think that helped him reach a very nice design for putting pictures together so what do we see we see working with whole values not a word at the time that's a key functional programming idea building combining forms for pictures using the algebra the laws as a litmus test for a good design and once again using functions as representations and these are ideas that come back again and again okay so now on to I'll skip ahead a little to 1994 tell you about a paper this which is quite little-known I think with a very weird title so this was a paper written by Paul Hugh deck and Mark Jones Paul Hugh deck was one of the original Haskell designers he was a leader in the field of functional programming and in the mid 90s you couldn't get research money to do functional programming for real programs of course but you could get research money to study functional programming for prototyping so DARPA had a huge program when lots of different groups were developing prototyping languages prototyping was you know it was hot in those days was like I don't know micro services or whatever so dhaba had all of these groups working away and Paul had money to develop Haskell as a software prototyping language but after they've been working for a while DARPA thought well let's see how they're doing let's give them all a problem to solve and we'll see how quickly and how productively these various groups can develop a prototype so this is why the paper has the weird name because the prototyping languages were apart from Haskell ADA C++ awk I'm quite sure how that got in there and the variety of others so DARPA gave the problem to each group and Mark Jones was the guy who got the job of solving the problem in Haskell and DARPA being DARPA the problem was a two-dimensional geometry server and it was supposed to take in geographical information about positions of hostile aircraft and commercial aircraft and so on and then divide the space up into regions with weird names like weapon doctrine and slave doctrine and engage ability zone that's this great thing this ring shaped thing that's the engage ability zone so the prototype was supposed to read this stuff and then generate output that would say you know at time 40 the commercial aircraft is going to be in the engage ability zone and in the tight zone and the hostile craft will be in the carrier slave doctrine so mark had the job of implementing this in Haskell and of course he needed to represent regions in the plane let's see how might you represent a region as a function of course so Marc chose to say that a region is going to be represented by a function from a point to a ball and the function will return true for points in the region and false for points outside and that's very very simple it makes it easy to define for example a circle you just take the points you may compute how far is it from the origin and compare that to the radius it's easier to compute the outside of a region just negate the boolean you can compute the intersection of a region you know a point is in the intersection of P and Q if it's in P and it's in Q and then you can go on to build up things like an annulus that is a ring just by saying well now is a Mewis with an inner radius of r1 and an outer radius of r2 it's the outside of a circle with radius r1 intersected with the inside of a circle with radius r2 well I think you can see now though Mark probably didn't have to write a whole lot of code and when the results were reported into DARPA they look like this now I appreciate the fonts a bit small here but I will read the important stuff so the thing with a red line about it that is mark solution it's 85 lines of Haskell and that compares very well with for example 800 lines of ADA 9x or 1100 and five lines of C++ so it was far and away the smallest solution it was also one of the solutions that worked which the evaluators didn't really believe to begin with they thought it was just just a design document but no it was actually executive all the annoying thing here is the Haskell was 85 lines oh it's the only functional language in the list by the way but mark liked writing type declarations he'd actually written 20 line lines that the type checker could have inferred for him so this could have been 56 lines of code anyway so the DARPA evaluators got their stuff and they thought there's something fishy here this happened because Mark Jones is brilliant which he is but so they just didn't trust it so what they did was without telling Paul or mark they found a graduate student somewhere else and they gave that poor guy one week to learn Haskell and then gave him the problem that's why Haskell appears in the list twice this bottom one is the student solution it's 156 lines it's almost twice the size of marks what can you expect with only weeks experience but it's the second smallest solution and the entire list so you would think this is tremendous right this is a huge success for functional programming so how did the evaluators react it's too cute for its own good higher-order functions are just a trick probably not useful in other contexts what can you do to list yeah yes it's very very good unfortunately the code didn't work there's more behind i really recommend looking for this paper actually to this day it's a great read and then you'll learn much more I can only give you know a top-level summary so so now I want to go back again to an idea that really inspired me and that is the idea of lazy evaluation in 1976 two separate papers were published with basically the same idea in them the first one was called a lazy evaluator by Henderson and Morris look remember this guy Peter Henderson again and the other was by Dan Friedman and David wise called cons should not evaluate its arguments and the basic idea in both of them was that rather than computing things you know date like argh function arguments parts of data structures when you construct them you should save the computation until later until the value is actually needed so if you're not familiar with lazy evaluation I think the best way I can explain it is by saying it's like trying to get a teenager out of the house put on your jacket I will put on your shoes I will brush your teeth I will we're going now oh wait a minute that's how lazy evaluation works so why was it important remember we've been talking about not word at a time programming but programming with a whole value well with lazy evaluation the whole value can be infinite and that opens a whole new world of possibilities so for example you could have the infinite list of natural numbers 0 1 2 3 blah blah you can have the list of all the iterations of a function in X f of X F applied twice to X and so on and the key thing here is that you can manipulate these infinite things in your program but you will never actually compute all of the elements it's the consumer of this data structure that decides how many elements you're going to compute and I saw this and I thought wow this is wonderful this lets you separate the code that defines what you want to compute from the code that defines how much you want to compute and I had some years before being forced to study in numerical methods which I was not very good at but I realized that I could write a great consumer for numerical methods many email numerical algorithms compute a sequence of approximations and then they take the first one that is within some tolerance Epsilon of the predecessor so I could just define this function limit that would take one of these infinite lists and just search down it for the first approximation that is sufficiently close to the one before and then I could use that to define for example a square root algorithm this is the newton-raphson method we you start from some value I've taken 1.0 and then you iterate a function that gives you the next approximation for the previous one and you take a limit here's how you might compute derivatives you compute the derivative of function by computing its slope across a small segment so to compute the derivative at X you will take the value of f at X plus a little bit H take the difference divide by H that gives you the slope and then the smaller you make H the more accurate the approximation will be so once again if I if I start off taking H dough by repeatedly / - a mat slope over it are getting improving sequence of approximations and I can just take the limit in the same way but the convergence check is going to be the same code in both cases it's only the code for generating the approximations that is different I thought this was nice but actually I also remembered from my numerical analysis course quite a clever idea so I already explained how to compute a derivative and it depends on this this value H but you can also compute integrals by the trapezium rule which you may remember and there again you're adding up the areas of a lot of bars with a particular width let's call that with H - so you can see that in both these methods there is this parameter H the smaller you make H the better the result that you get well it turns out that in both cases the result that you get is going to be of this form a plus B times some power of H so here a is the right answer and B times the power of H is the error term okay so this is standard numerical analysis so what if we compute what if we apply those methods for a value H and half that value then we get two approximations to our integral or derivative and we know there are this form so we know these two values and we've got two unknowns a and B think back to high school mathematics if you've got two equations and two unknowns you can solve for the unknowns so you can figure out what a is all you need is two approximations and you can compute the right answer isn't that brilliant so actually if you compute your original sequence of approximations by your original method then you can take the first two and get the right answer there but if you take the next two and so on you can get a whole sequence of right answers and it turns out they're not all the same well that would have been really magic wouldn't know that there is no real magic in the world but it's almost magic because that green sequence converges much faster than the blue one what you've done I mean the reason it's not exact is that that error term is an approximation the true error term has you know up H to the N but then there'll be a larger power of H in another error term so what we've done here is we've eliminated the first error term and we get a numerical method with a better order of convergence and we can just write a function to improve a sequence of approximations by eliminating the error term of order N and we can write that as a separate piece of code is very simple and then if we want for example a really fast derivative we can use it more than once look here I've done the basic method to get a sequence of approximations then I've eliminated the first order error term then I've eliminated the second order error term this gives me a third order numerical method for derivatives and I can just take the limit and it'll converge in no time it works even better for integration because integration is much slower so the winds is much larger and everything is programmed separately and I could understand all the parts as opposed to when I first studied numerical analysis and it's all thanks to whole value programming and lazy evaluation so I was very happy with these examples and these are the first examples in my paper so if you dig out my paper you'll find all of this stuff explaining a lot more detail the basic idea that I was emphasizing here was that of a lazy producer and consumer where the consumer figures out which values to demand and then the producer generates them in response to a demand and what we've seen here is that you can use a convergence test and a sequence of numerical approximations but there are many other ways you can use the same idea for example the consumer might be a search strategy and the producer a search base so you can write search programs where one part of the program just builds the whole space without any concern about how you're going to search in it and the search strategy is independent and can be used on any such space in the paper I use this to develop a noughts and crosses program so I opened the alpha-beta heuristic which is quite sophisticated and I played noughts and crosses because I had a very small computer but it was good fun but I use the same idea to develop a pretty printing library which I'll briefly show you so here pretty printing the problem here is for example if when you print a data structure the airline shell it comes out nicely laid out that's pretty printing or you might want to take source code and lay it out according to standard layout out conventions so pretty printing is something that is quite often a need for but if you've written the pretty printer you'll know how hard it is to get those darn things right so I was quite interested in making a library for doing this where I would build a lazy search space representing all of the ways you could lay out a document and then have a separate selection criterion that would pick the best layout from that collection so for example if you want a pretty print an if-then-else then you might be choosing between these two alternative layouts either a horizontal form if it everything fits nicely or a vertical one if it doesn't and often in the vertical one you want some indentation as well but of course you don't want spaces to appear in the horizontal form so my goal was to write a pretty printer that would write one piece of code that might render like this or like this depending on on the context and I did that by defining document fragments as values so each document fragment you can think of it as a bit of text and some indentation that's the red stuff and then I defined combining forms for putting them together vertically in which case the indentation would be preserved or horizontally in which case the indentation would be discarded so that's why I had to distinguish the indentation from just ordinary next that was this less than greater than operator and then I needed ways to build primitive documents you convert a string into a document and to add indentation that's what this nest function do i've nested by two spaces and now if you think about it there are some nice laws that these combining forms satisfy so indentation is discarded in a horizontal form so if I put a beside a nested document that's the sale is just putting a beside be the messing gets discarded on the other hand if a is the thing that's nested but it doesn't get discarded B gets put to the right of a without change of the indentation of a so there are two laws of these things satisfy here's another one if you put three things together horizontally it doesn't matter which order you do it if you put three things together vertically it doesn't matter which order you do this one's kind of cool if you put a above B besides see you get the same thing as if you put a above B besides C so even when you're mixing above and beside you can remove the brackets but these two are different if you put a beside B above C then C ends up indented the same as a if you put a beside B above C then C ends up indented more the same as B so you get a kind of interesting algebra here with many laws that hold and one that doesn't so then I also defined an operator for constructing documents with more than one possible layout I just called it separate separate a B and C by either putting them together horizontally or vertically and now if you want to write pretty printers it's very simple to do here's a pretty printer for binary trees which prints a leaf just as a text string and prints a branch by separating so this might be horizontal or vertical branch a left subtree nested and a right subtree nested and those laws they were actually really important who it's very hard to figure out what a pretty printer should really do so how did I do it simple in the implementation those laws are being applied to guarantee that what I produce is a correct output for the code that I started off with okay so then I had a heuristic for choosing the layout I know this was a good idea because very many distinguished people have improved on it afterwards so all of these people have fixed some of my mistakes and among them is our own vicar Colson who implemented a library based on these ideas in ED lang it's in syntax tools so if you want to play with pretty printing Combinator's inspired by my paper just use pretty PR so I'm probably best known nowadays for quick check and what does quick check do will you give it a general property of your code it generates random tests and if they all pass it's happy if you write a property that's not true it'll generate tests that fail here's a list that's not its own reversal and having found a failing test case then it goes on to search for a simplest possible example which we call shrinking and we end up in this case with 0 1 that's the shortest smallest list that is not its own reversal why is it smallest well if you remove either element you get a list with one element that is its own reversal and if you were to reduce the one to a zero you'd have 0 zero which is also its own reversal so this is the smallest list that isn't that's the minimal counter example so what what I sort of point out is that here the property describes a search space of test cases so we've got one part of code constructs the space of all possible tests and quick check search strategy which is actually a combination of random search to begin with followed by a systematic search for this smallest example it's the same idea all over again I just can't get away from I only have one idea obviously okay so I want to quickly now talk about some of the things that inspired Mary and and that starts with this book Mead and Conway anybody read it a few people so this book transformed VLSI design before this book VLSI design meant drawing rectangles on silicon afterwards it was about thinking in a high-level way about how the hardware circuits worked and Mary was very inspired by that not least she was inspired by what's called retiming so this diagram represents an orange box which is doing some computation and the blue circles are one clock cycle delays so both inputs of this orange box are being delayed one clock cycle if you think about it that will do the same thing as this circuit where the inputs are not delayed but there's a delay on the output so what do we have here we have two circuits that are equal and Mary was inspired by that and for her thesis work she designed a language called mu F P whose idea was circuits as values and it was basically back as his F P plus 1 clock cycle delays ok little more than that but that was the basic idea with many of the same combining forms many of the same laws and it was especially good for reasoning about this retiming because there were laws that could be applied to move those unit delays around in circuits which was otherwise quite hard to get right let me show you an example of where that's useful here's a circuit which is a chain of orange boxes that do some computation and I've just added a whole lot of unit delays so the inputs are being delayed quite a lot but now watch all of the inputs to those orange boxes are being delayed right so if I apply the law that I showed you two slides ago I move them to the end and just have one delay instead and now ignore the leftmost column all of the inputs to the rightmost three boxes are delayed so let's apply the law again and do that and so on so by applying the law we can see that the circuit I started off with does the same thing as this circuit okay what's the point of that well the circuit I started off with has a long long combinational path through all of those orange boxes and that means if you talk the circuit you have to wait for data to flow all the way from the right-hand side to the left-hand side and that will take a long time after applying the laws you've got delay elements between each box that means in one clock cycle data only has to propagate across one of the boxes so you can probably clock this circuit four times faster than the original one which is great that's why people want to do it but you have to figure out that you need this triangle of delays on the inputs and figuring out where to put those delays on the inputs that's actually quite hard if you don't have this kind of algebra so Mary even had users from ufp Plessy who are a British electronics company we're designing a chip for a video motion estimation it's part of video compression and they were designing a regular array for that and they used meu FP and they said afterwards using new FP the array processing element was described in just one line of code has that and the complete array was only four lines and new FP enabled the effects of adding or moving data latches those delays within the array to be assessed quickly so this was great they looked a paper about it and this is a nice success for a functional programming of hardware the next thing that happened was that Plessy were bought by G EC and Siemens who went interested in this at all they probably thought it was too cute for its own good so that was the end of that at Plessy but not the end of functional languages for hardware design Mary went on to design larvae which is kind of Mew fp+ functional geometry you might say so the key thing there is that it captures the semantics of a circuit but also the geometry tells you something about the placement because when a programmer or when a designer designs one of these regular circuits he knows it's an array circuit it should be laid out as an array if you just generate give synthesis tools the semantics they don't know that so here for example are four adder trees this is an FPGA configuration generated from lava using the functional geometry stuff to give placement information to the tools if you just say I want this semantics and use the synthesis tools you get this and you know you don't have to know much about FPGAs to see this is a dog's breakfast and because it's a dog's breakfast it performs much worse so Satnam Singh who was Mary student worked at Xilinx for quite a long time and he would build FPGA layout generators for customers and he he'd write them in lava and gives me Haskell binary so you know here's a layout generator for your problem he never told him what was inside it though so they didn't know they were running Haskell code once actually he had a problem one of this generates didn't work because of a bug in the Haskell compiler so he emailed silent Peyton Jones at Microsoft Research with the bug report and next day then Simon sends him a patch and he was able to continue but when he told his boss about it adds eiling's boss couldn't believe it he said what you got 24 hours support from Microsoft while we're talking about hardware let's talk about Intel remember the Pentium bug here is an example see here we taking two numbers one starting with four when starting with three and what we're doing we're taking the one starting back with four dividing by the second one multiplying by the second one again so that should give us back the first one subtracting it from the first one that should give us zero but on the buggy pensions it was 256 so that was them not good at Intel how to replace an awful lot of buggy Pentium chips it cost them four hundred and seventy five million dollars which is not enough to sync the coffee and sync the company but not that far short and afterwards they had to do something with the buggy pensions of course so you know what they did they put them in key rings and they gave them to all their employees and on the back of the keyring it says bad companies are destroyed by crises good companies survive them great companies are improved by them I've seen one of these key rings I know this guy Carl Seeger so how did Intel improve Carl Seeger who was working for them designed their own lazy functional language called FL which had some built in proof techniques and they started designing their processes with functional programming so this this system that he built it has thousands of users with Intel and they used FL is a design language a specification language scripting language they built theorem provers in it they prove things about FL programs so why hasn't there been a second Pentium bug he thanks to functional programming in part at least so functional programming for hardware has has been a very successful application area that many people don't know so much about I just want to finish with one last example of that that is a company called blue speck founded by Arvind a professor at MIT Arvind was also one of the original designers of Haskell and blue spec is a hardware description language that is purely functional it's very Haskell like you build the architecture of your circuit with functional programming but it's also got some very clever stuff for the low-level part it uses guarded atomic transition rules I'm not gonna explain what they are but they're very clever and they let the compiler find the parallelism that you need on a chip and then they generate very log that goes on into further chain of synthesis tools and blue spec gets you know the benefits you'd expect from writing high level of functional programs the compiler is very good it often beats handwritten code it lets designers use better algorithms because they have more time to think architectural changes and so on are very easy there's a very nice paper about this if you drop light to read about this fascinating application their CTO Nikhil wrote a paper called types functional programming and atomic transactions and hardware design which describes all this stuff but ok so we can write Haskell like functional programs and compile them to hardware which program would you compile or for me it's obvious quick check of course and they've actually done that they've made a version of quick check which they've written in blue spec which they can compile onto a chip that is quick check on FPGA and it generates random test cases on the chip if they fail it shrinks them down to a minimal test and this just blows hardware designers away they've never seen anything of the sort you can imagine how incredibly fast the tests run when they're being generated and executed on the same FPGA so I think that's really really fun well we've made a long journey here from church numerals in the 1940s to quick check on an FPGA last year but we've seen the same ideas coming back again and again the idea of programming with whole values instead of a word at a time of using combining forms that satisfies simple laws and often using functions as representations I think backers will be proud of us thank you

Channel: Erlang Solutions

Views: 15,187

Keywords:

Id: Z35Tt87pIpg

Length: 60min 57sec (3657 seconds)

Published: Fri Mar 11 2016

Reddit Comments

[u/Faucelme]

Ha, at 7:20 he mentions that a very early version of GHC used Church encoding for data structures.

[u/gleberp]

It's really nice to see Haskell talks cropping up in all kinds of conferences both related to other FP languages and non-FP as well!

[u/srhb]

Fantastic talk.

The buildup was fantastic -- I really thought that the MuFP and Lava story was a setup for using something akin to the layout combinators from the pretty printing library to lazily search through some space of circuit layouts. :-)