C9 Lectures: Dr. Graham Hutton - Functional Programming Fundamentals Chapter 11 of 13

Well, my friends, the day has arrived. For thirteen weeks, you have been provided all the conceptual tools to take the leap into the deep end of the functional programming pool and float safely. The great Dr. Erik Meijer has generously given his value time to teach us the fundamentals as delivered by Graham Hutton in his book
Programming in Haskell. Of course, Erik merged his own extensive knowledge, unique perspective and experience into the educational weave: so, you got the best of two worlds. We hope you enjoyed this series, the first in a new a format of Channel 9 content (lectures).
The Channel 9 team and Niner nation thank our dear friend Erik for this stellar contribution to Channel 9 and programming education, generally. Of course, we also thank Graham Hutton for writing the book (and for guest lecturing Chapter 11) that Erik is both so fond of and which provided a basis for these lectures, which, by the way, were all done in true Channel 9 fashion: They were recorded in single takes with Erik doing a brilliant job articulating, contextualizing, expanding on the fundamentals and being, well, Erik, one of our favorite geniuses, all in real time.
In Chapter 13, Equational Reasoning (and also revealing why Erik says 'uhm' and 'you know' so often), the grand finale, Dr. Meijer digs into referential transparency and being able to replace equals by equals in all contexts.
In some sense, the purity inherent in functional languages like Haskell makes it easy to express and implement equational reasoning. In Haskell, our old friend "=" means "is equal to by definition". But what does equational reasoning
mean? It is clear that propositional logic is too weak for many applications and that equational logic is a first step towards a more powerful system*. Is it? Dr. Meijer, please do explain.
Tune in. Enjoy.
* source: http://www.cs.cmu.edu/~cdm/pdf/EquLogic.pdf
Chapter 1
Chapter 2
Chapter 3
Chapter 4
Chapter 5
Chapter 6
Chapter 7
Chapter 8
Chapter 9
Chapter 10
Chapter 11
Chapter 12
Chapter 13
Happy Holidays everyone, and thanks a lot for watching.
Thank you Dr. Meijer for this wonderful and enlightening series.
a truly amazing series, and hopefully more to come in this format from Channel 9. I can't say as I've been educated as much and enjoyed it at the same time in many, many years. I've already watched most of these lectures a few times, and each time I learn something new. I can't recommend this series enough, both as an introduction to functional programming and haskell, and as a solid grounding in many general programming concepts. Fantastic.
Thank you Erik, this has been an amazing journey and one of my learning highlights of the year. Seasons greetings to Channel 9 and all who sail with her.
Happy holidays! If you celebrate Christmas, then have a merry one! In either case, I hope all of you get to have some time to recharge and enter the new year healthy and happy.
Erik, see you in '10 for more lectures and more E2Es! Thank you, man!!
Cheers!!!
C
Thank you so much Erik! This has been a great series.
I was wondering how you would finish the series. I had expectations for something nice. But this... this was just simply wunderbar. Magnificent! Like the finale at a 4th of July fireworks display. Thanks for giving us all this and thanks especially for the book list! How could anyone not be ignited by your enthusiasm, love and passion? I certainly am caught up in it.
f (g x) = h (f x)
f (g (fix g)) = h (f (fix g))
f (fix g) = h (f (fix g))
f (fix g) = h (f (g (fix g)))
f (fix g) = h (h (f (fix g)))
f (fix g) = h (h (h (f (fix g))))
...
f (fix g) = fix h
???
This series was an amazing Christmas present for us all. Erik's spirit of giving cannot be denied or underestimated.
Thanks!
Just Amazing, the best present I've ever received. Thanks so much Erik.
Thank you, Erik! I enjoyed a lot your lectures. They're really cool! Hope to meet you again with a new set of lectures!
Wow, this is the first episode where Erik wears 2 different shirts. Apparently, the “short break” was not that short.
He could've changed in-situ; just shedding the outer skin
A great conclusion to this series. It's enough to make your brain explode.
Thank you !
In trying to prove that
reverse ((x:xs) ++ ys) = (reverse ys) ++ (reverse x:xs)
Why do we need to prove that?
reverse ((x:xs) ++ ys) = (reverse ys) ++ reverse (x:xs)
Proving that (xs ++ ys) ++ zs == xs ++ (ys ++ zs) is enough.
reverse ((x:xs) ++ ys) = (reverse ys) ++ (reverse (x:xs)) reverse (x:(xs ++ ys)) = (reverse ys) ++ (reverse xs ++ [x]) reverse (xs ++ ys) ++ [x] = (reverse ys) ++ ((reverse xs) ++ [x]) reverse (xs ++ ys) ++ [x] == ((reverse ys) ++ (reverse xs)) ++ [x] reverse (xs ++ ys) == (reverse ys) ++ (reverse xs)!
Done.
series are great, camera man is bad.
The reason why we need a white/black board(and nowadays power point slide) in a classroom is that not everyone is a fast reader. I found that I don't have enough time to read through the slides then the camera zoom back to Dr. Meijer.
He is not MJ and it is what he said(that usually I need to refer to the slide) and not his facial expression that I am interest in.
Hi Erik -- you mentioned that the "sleight-of-hand" of induction is similar to the kind magicians use:
the fast-reverse (linear time) algorithm is exactly the one you would use to reverse a pack of playing cards by dealing them off the top, face-down, into another pile that starts off empty .
There are other famous algorithms that are isomorphic to manual procedures with playing cards, like quicksort, merge sort, binary search, etc. Working out such algorithms with a pack of cards in-hand is not completely crazy
Erik Meijer’s List of Books
1.
Logic and Computation: Interactive Proof with Cambridge LCF (Cambridge Tracts in Theoretical Computer Science) (Paperback)
2.
Mathematical Theory of Programme Correctness (Prentice-Hall International series in computer science) (Hardcover)
3.
The Haskell School of Expression: Learning Functional Programming through Multimedia (Paperback)
4.
LaTeX: A Document Preparation System (2nd Edition) (Paperback)
5. Denotational Semantics
6.
Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (Paperback)
7. Programs and Machines
8.
The Denotational Description of Programming Languages: An Introduction (Paperback)
9.
Erik Meijer’s Thesis – Calculating Compilers
10.
Lectures on the Logic of Computer Programming (CBMS-NSF Regional Conference Series in Applied Mathematics) (Paperback)
11. Erlang – Joe Armstrong
12.
The Algebra of Programming (Prentice-Hall International Series in Computer Science) (Hardcover)
13.
Algorithmic Language and Program Development (Monographs in Computer Science) (Hardcover)
14.
Algebraic Approaches to Program Semantics (Texts and Monographs in Computer Science) (Hardcover)
Thanks for putting up these links. I am certain folks will enjoy reading these books.
Erik,
It would be great if you can mention all the other books that you recomended during the series. To Mock a Mockingbird was an excelent sugestion. Specially seeing how combinator that seem so abstract in the book can be used for equational reasoning. Thank for that suggestion.
Here is the link: http://www.amazon.com/gp/product/0394534913/ref=oss_product