
keyboard_arrow_down
Equational Reasoning  From Code To Math and Back Again
45 mins
Talk
Beginner
Equational Reasoning [1,2] is an intermediate/advanced FP technique, that sits at the intersection of programming and mathematics and has many interesting uses. It can be used to prove that a piece of code is correct, has specific performance properties, to drastically reduce the size of a particular piece of code , assure that your code will scale to a bazillion servers, etc etc.
But how this technique works is often considered a mystery. What is also missing is a step by step way to learn this method so you can use it in your code. Many books and blog entries show you examples and then you, the reader, are supposed to infer from these examples how Equational Reasoning works. When I first ventured into FP, I could (more or less) follow published examples, but never could figure out how this technique works and how to apply it to my code.
The key to such understanding (as I discovered much later) is to grok the underlying mathematical structure, specifically the nature of the logic and proof technique that provides the working machinery of Equational Reasoning.
In this presentation, I look at the mathematical underpinnings of this excellent programming technique. Once you understand how the math works [3], it is easy to see how the programming technique works. And once you know how that works, you can use Equational Reasoning as just another tool in your dev toolbox.
Once they learn the basics of FP, most programmers are stuck with respect to how to get to the next level.
The most common solution (especially for Haskellers) is to try to deep dive into Category Theory and Algebra, and their uses in FP. Which is a good step if you can pull it off, but in practice this is much harder than it needs to be (which is the topic of another lecture someday), and many people give up at this point.
(imo) Understanding Equational Reasoning levels up your FP skills without necessarily having to learn CT structures simultaneously (though, of course nothing prevents you from learning both and combining them, as many Haskellers do), and is a gentler 'level up' than wrestling with Categories and Arrows and such.
This presentation reveals the nuts and bolts of why and how Equational Reasoning works. Then you can read the existing literature and gain much more out of it than otherwise.
Essentially, this talk is what I wish someone had told me when I was trying to learn FP and got stuck. You might be able to gain from my struggles!
[1] A blog entry explaining the basics
[2] A good book with many examples
Some quotes from the preface
".. I (Richard Bird) was interested in the specific task of taking a clear but inefficient functional program, a program that acted as a specification of the problem in hand, and using equational reasoning to calculate a more efficient one."
" One factor that stimulated growing interest
in functional languages in the 1990s was that such languages were good for
equational reasoning. Indeed, the functional language GOFER, invented by
Mark Jones, captured this thought as an acronym. GOFER was one of the
languages that contributed to the development of Haskell, the language on
which this book is based. Equational reasoning dominates everything in this
book."To be clear, this talk is not about the problems tackled in the book, though I'll use a couple of them as dissection specimens. The book shows (excellent) examples of applied ER, with a focus on generating efficient algorithms. My talk is about how ER works, and bridging the mathematical and programmatic machinery. We'll see, for example, why such derivation of efficient algorithms via ER works.
[3] I keep the math bits programmer friendly, so don't worry if you are not big on formal math. This is a talk addressed to programmers. If you can write nested if statements or SQL queries, say, (iow if you have a couple of years of programming experience), specifically if you understand how logical operators (and, or, not) work, you'll be fine. I'll fill in the rest.

keyboard_arrow_down
Equational Reasoning  From Code To Math and Back Again
45 mins
Talk
Beginner
Equational Reasoning [1,2] is an intermediate/advanced FP technique, that sits at the intersection of programming and mathematics and has many interesting uses. It can be used to prove that a piece of code is correct, has specific performance properties, to drastically reduce the size of a particular piece of code , assure that your code will scale to a bazillion servers, etc etc.
But how this technique works is often considered a mystery. What is also missing is a step by step way to learn this method so you can use it in your code. Many books and blog entries show you examples and then you, the reader, are supposed to infer from these examples how Equational Reasoning works. When I first ventured into FP, I could (more or less) follow published examples, but never could figure out how this technique works and how to apply it to my code.
The key to such understanding (as I discovered much later) is to grok the underlying mathematical structure, specifically the nature of the logic and proof technique that provides the working machinery of Equational Reasoning.
In this presentation, I look at the mathematical underpinnings of this excellent programming technique. Once you understand how the math works [3], it is easy to see how the programming technique works. And once you know how that works, you can use Equational Reasoning as just another tool in your dev toolbox.
Once they learn the basics of FP, most programmers are stuck with respect to how to get to the next level.
The most common solution (especially for Haskellers) is to try to deep dive into Category Theory and Algebra, and their uses in FP. Which is a good step if you can pull it off, but in practice this is much harder than it needs to be (which is the topic of another lecture someday), and many people give up at this point.
(imo) Understanding Equational Reasoning levels up your FP skills without necessarily having to learn CT structures simultaneously (though, of course nothing prevents you from learning both and combining them, as many Haskellers do), and is a gentler 'level up' than wrestling with Categories and Arrows and such.
This presentation reveals the nuts and bolts of why and how Equational Reasoning works. Then you can read the existing literature and gain much more out of it than otherwise.
Essentially, this talk is what I wish someone had told me when I was trying to learn FP and got stuck. You might be able to gain from my struggles!
[1] A blog entry explaining the basics
[2] A good book with many examples
Some quotes from the preface
".. I (Richard Bird) was interested in the specific task of taking a clear but inefficient functional program, a program that acted as a specification of the problem in hand, and using equational reasoning to calculate a more efficient one."
" One factor that stimulated growing interest
in functional languages in the 1990s was that such languages were good for
equational reasoning. Indeed, the functional language GOFER, invented by
Mark Jones, captured this thought as an acronym. GOFER was one of the
languages that contributed to the development of Haskell, the language on
which this book is based. Equational reasoning dominates everything in this
book."To be clear, this talk is not about the problems tackled in the book, though I'll use a couple of them as dissection specimens. The book shows (excellent) examples of applied ER, with a focus on generating efficient algorithms. My talk is about how ER works, and bridging the mathematical and programmatic machinery. We'll see, for example, why such derivation of efficient algorithms via ER works.
[3] I keep the math bits programmer friendly, so don't worry if you are not big on formal math. This is a talk addressed to programmers. If you can write nested if statements or SQL queries, say, (iow if you have a couple of years of programming experience), specifically if you understand how logical operators (and, or, not) work, you'll be fine. I'll fill in the rest.