## First impression of “Real World OCaml”

Tomorrow I will be flying to Cambridge to attend International Summer School on Metaprogramming. One of the prerequisites required from the participants is basic knowledge of OCaml, roughly the first nine chapters of “Real World OCaml” (RWO for short). I finished reading them several days ago and thought I will share my impressions about the book.

RWO was written by Yaron Minsky, Anil Madhavapeddy and Jason Hickey. It is one of a handful of books on OCaml. Other titles out there are “OCaml from the Very Beginning” and “More OCaml: Algorithms, Methods and Diversions” by John Whitington and “Practical OCaml” by Joshua Smith. I decided to go with RWO because when I asked “what is the best book on OCaml” on #ocaml IRC channel RWO was an unanimous response from several users. The title itself is obviously piggybacking on an earlier “Real World Haskell” released in the same series by O’Reilly, which was in general a good book (though it had its flaws).

The first nine chapters comprise about 40% of the book (190 pages out of 470 total) and cover the basics of OCaml: various data types (lists, records, variants), error handling, imperative programming (eg. mutable variables and data structures, I/O) and basics of the module system. Chapters 10 through 12 present advanced features of the module system and introduce object-oriented aspects of OCaml. Language ecosystem (ie. tools and libraries) is discussed in chapters 13 through 18. The remaining chapters 19 through 23 go into details of OCaml compiler like garbage collector or Foreign Function Interface.

When I think back about reading “Real World Haskell” I recall that quite a lot of space was dedicated to explaining in detail various basic functional programming concepts. “Real World OCaml” is much more dense. It approaches teaching OCaml just as if it was another programming language, without making big deal of functional programming model. I am much more experienced now than when reading RWH four years ago and this is exactly what I wanted. I wonder however how will this approach work for people new to functional programming. It reminds my of my early days as a functional programmer. I began learning Scala having previously learned Scheme and Erlang (both unusual for functional languages in lacking a type system). Both Scala and OCaml are not pure functional languages: they allow free mixing of functional and imperative (side-effecting) code. They also support object-oriented programming. My plan in learning Scala was to learn functional programming and I quickly realized that I was failing. Scala simply offered too many back-doors that allowed escaping into the imperative world. So instead of forcing me to learn a new way of thinking it allowed me to do things the old way. OCaml seems to be exactly the same in this regard and RWO offers beginners little guidance to thinking functionally. Instead, it gives them a full arsenal of imperative features early on in the book. I am not entirely convinced that this approach will work well for people new to FP.

“Real World OCaml” was published less than three years ago so it is a fairly recent book. Quite surprisingly then several sections have already gone out of date. The code does not work with the latest version of OCaml compiler and requires non-obvious changes to work. (You can of course solve the problem by working with the old version of OCaml compiler.) I was told on IRC that the authors are already working on the second edition of the book to bring it to date with today’s OCaml implementation.

Given all the above my verdict on “Real World OCaml” is that it is a really good book about OCaml itself (despite being slightly outdated) but not necessarily the best book on basics of functional programming.

## Coq’Art, CPDT and SF: a review of books on Coq proof assistant

I have been pretty quiet on the blog in the past couple of months. One of the reasons for this is that I have spent most of my time learning Coq. I had my first contact with Coq well over a year ago when I started reading CPDT. Back then I only wanted to learn the basics of Coq to see how it works and what it has to offer compared to other languages with dependent types. This time I wanted to apply Coq to some ideas I had at work, so I was determined to be much more thorough in my learning. Coq is far from being a mainstream language but nevertheless it has some really good learning resources. Today I would like to present a brief overview of what I believe are the three most important books on Coq: “Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions” (which I will briefly refer to as Coq’Art) by Yves Bertot and Pierre Castéran, “Certified Programming with Dependent Types” (CPDT) by Adam Chlipala and “Software Foundations” (SF for short) by Benjamin Pierce and over a dozen over contributors. All three books significantly differ in their scope and focus. CPDT and Coq’Art are standard, printed books. CPDT is also available online for free. Software Foundations is only available as an online book. Interestingly, there is also a version of SF that seems to be in the process of being revised.

I believe Coq’Art was the first book published on Coq. There are two editions – 2004 hardcover version and a 2010 paperback version – but as far as I know there are no differences between them. Too bad the 2010 edition was not updated for the newest versions of Coq – some of the code examples don’t work in the newest compiler. Coq’Art takes a theoretical approach, ie. it teaches Coq largely by explaining how the rules of Calculus of Constructions work. There are also practical elements like case studies and exercises but they do not dominate the book. Personally I found Coq’Art to be a very hard read. Not because it dives too much in theory – it doesn’t – but because the presentation seems to be chaotic. For example, description of a single tactic can be spread throughout deveral places in the book. In principle, I don’t object to extending earlier presentation with new details once the reader gets a hold of some new concepts, but I feel that Coq’Art definitely goes too far. Coq’Art also presents material in a very unusual order. Almost every introduction to Coq or any other functional language begins with defining data types. Coq’Art introduces them in chapter 6. On the other hand sorts and universes – something I would consider an advanced concept for anyone who is not familiar with type-level programming – are presented in the second chapter. (Note that first chapter is a very brief overview of the language.) By contrast, CPDT goes into detailed discussion of universes in chapter 12 and SF does not seem to cover them at all. Overall, Coq’Art is of limited usefulness to me. To tell the truth this is not because of its focus on theory rather than practice, but because of language style, which I find rather inaccessible. Many times I had problems understanding passages I was reading, forcing me to re-read them again and again, trying to figure out what is the message that the authors are trying to convey. I did not have such problems with CPDT, SF, nor any other book I have read in the past few years. At the moment I have given up on the idea of reading the book from cover to cover. Nevertheless I find Coq’Art a good supplementary reading for SF. Most importantly because of the sections that explain in detail the inner workings of various tactics.

As mentioned at the beginning, I already wrote a first impressions post about CPDT. Back then I said the book “is a great demonstration of what can be done in Coq but not a good explanation of how it can be done”. Having read all of it I sustain my claim. CPDT does not provide a thorough and systematic coverage of basics, but instead focuses on advanced topics. As such, it is not the best place to start for beginners but it is a priceless resource for Coq practitioners. The main focus of the book is proof automation with Ltac, Coq’s language for writing automated proof procedures. Reader is exposed to Ltac early on in the book, but detailed treatment of Ltac is delayed until chapter 14. Quite surprisingly, given that it is hard to understand earlier chapters without knowing Ltac. Luckily, the chapters are fairly independent of each other and can be read in any order the reader wishes. Definitely it is worth to dive into chapter 14 and fragments of apter 13 as early as possible – it makes understanding the book a whole lot easier. So far I have already read chapter 14 three times. As I learn Coq more and more I discover new bits of knowledge with each read. In fact, I expect to be going back regularly to CPDT.

Coq’Art and CPDT approach teaching Coq in totally different ways. It might then be surprising that Software Foundations uses yet another approach. Unlike Coq’Art it is focused on practice and unlike CPDT it places a very strong emphasis on learning the basics. I feel that SF makes Coq learning curve as flat as possible. The main focus of SF is applying Coq to formalizing programming languages semantics, especially their type systems. This should not come as a big surprise given that Benjamin Pierce, the author of SF, authored also “Types and Programming Languages” (TAPL), the best book on the topic of type systems and programming language semantics I have seen. It should not also be surprising that a huge chunk of material overlaps between TAPL and SF. I find this to be amongst the best things about SF. All the proofs that I read in TAPL make a lot more sense to me when I can convert them to a piece of code. This gives me a much deeper insight into the meaning of lemmas and theorems. Also, when I get stuck on an exercise I can take a look at TAPL to see what is the general idea behind the proof I am implementing.

SF is packed with material and thus it is a very long read. Three months after beginning the book and spending with it about two days a week I am halfway through. The main strength of SF is a plethora of exercises. (Coq’Art has some exercises, but not too many. CPDT has none). They can take a lot of time – and I really mean a lot – but I think this is the only way to learn a programming language. Besides, the exercises are very rewarding. One downside of the exercises is that the book provides no solutions, which is bad for self-studying. Moreover, the authors ask people not to publish the solutions on the internet, since “having solutions easily available makes [SF] much less useful for courses, which typically have graded homework assignments”. That being said, there are plenty of github repositories that contain the solved exercises (I also pledge guilty!). Although it goes against the authors’ will I consider it a really good thing for self-study: many times I have been stuck on exercises and was able to make progress only by peeking at someone else’s solution. This doesn’t mean I copied the solutions. I just used them to overcome difficulties and in some cases ended up with proofs more elegant than the ones I have found. As a side note I’ll add that I do not share the belief that publishing solutions on the web makes SF less useful for courses. Students who want to cheat will get the solutions from other students anyway. At least that has been my experience as an academic teacher.

To sum up, each of the books presents a different approach. Coq’Art focuses on learning Coq by understanding its theoretical foundations. SF focuses on learning Coq through practice. CPDT focuses on advanced techniques for proof automation. Personally, I feel I’ve learned the most from SF, with CPDT closely on the second place. YMMV

## To Mock a Mockingbird or: How I learned to stop worrying and learned combinatory logic

Yesterday I finished reading one of the most remarkable books I read in my life: “To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic” by Raymond Smullyan. When I finished reading The Little Schemer that book was listed as one of the suggested further readings. The title was quite intriguing so I got the book and started reading it. That was a year ago and I finished the book yesterday. Why? Because I got stuck and couldn’t understand some of the material. Luckily I now had some time to approach the book once again and grok it.

As the title suggests the book is a collection of logic puzzles. Out of six parts of the book – 25 chapters total – two are devoted to general logic puzzles, many of them about different aspects of truth telling. These can be regarded as a warm-up because in the third part the book makes a sudden turn towards combinatory logic. And this is the moment I found difficult in the book. Of course Smullyan doesn’t expect that readers work with combinators so he camouflages them as singing birds. Having some mathematical background I rejected this cover and tried to approach problems formally. Now, after reading the book, I think this was a major mistake that lead to my failure. I wasn’t able to deal with first 10 puzzles but I was more or less able to follow the solutions. Still I felt that reading solutions without being able to solve puzzles by myself was cheating so I gave up. A few months later I made another approach to the book but the results were exactly the same. Three weeks ago I made a third attempt, but I decided not to give up even if I won’t be able to come up with my own solutions. I figured that being able to only understand given solutions is completely fine. That decision turned out to be a good one. Although at first I wasn’t able to solve puzzles on my own at some point things just clicked. I solved one puzzle, then another and another and I realized that I know how to solve most of the puzzles. From now on the book went quite smoothly. Part four about logical paradoxes and inconsistencies in logical systems gave me some problems and I was afraid that each subsequent part will be equally challenging but it turned out that it was not the case. Part five gives a nice overview of computations using SKI combinators, while part six presents Church encoding of natural numbers and culminates with a proof of Gödel’s theorem.

# Some advice

The book is challenging on the one hand but it is also very rewarding. One of the most satisfying moments was realizing that I am able to write expressions like

$g\tilde{a}\tilde{b}=Z\tilde{a}f(Z\tilde{b}t(g(P\tilde{a})(P\tilde{b})))$

and then seeing that these are in fact nothing more but recursive programs. However it took me some work to get to this point and I think I can give future readers some advice about approaching the book. I’ve seen people on the internet saying they don’t understand parts of the book about combinators. In fact this is the same problem I faced on my initial contact. So my advice number one is: don’t give up. It looks like working with combinators just isn’t an inborn talent for most of us. It’s something that we just need to learn and it’s completely fine if you can’t figure out solutions on your own. It is important however to follow solutions given in the book. At some point you should understand how all of this works. Also don’t make my mistake of trying too formalize things to much. Don’t try to apply presented facts about combinators to anything else you know like maths or functional programming. This seems to only bring confusion. At some point things will become clear, but until then be patient. I wasn’t and in my attempts I even tried to introduce universal and existential quantification, which was a complete overkill. Also, it is very important to make notes. Keep conclusions of the puzzles in a notebook so you have easy access to a list of known facts. This is crucial since some solutions are based on facts proved 100 pages earlier. I also suggest having a separate scratch-pad.

# Summary

To “Mock a Mockingbrd” was a very insightful book and one of the most unusual ones I have read. It presents difficult material in a fun and entertaining way, but don’t be fooled – you will spend hours with pen and paper to complete this book. I highly recommend it to anyone interested in logic and functional programming. What functional programming has to do with it? Unrelated as it may seem I feel that this book has given me knowledge necessary to tackle type-level programming in Haskell. Just three weeks ago this seemed like a complete black magic and now it looks comprehensible.

Staypressed theme by Themocracy