Brute force SAT solver in Haskell

Sometimes people get wrong impressions after a Theory of Computation course. A "hard" problem there is not necessarily hard to solve with a program, just hard to solve well in realistic circumstances. Take SAT, for example, the boolean satisfiability problem for propositional logic. It's a classic example of a NP-complete problem, whose naive solution -- generate all possible combinations of truth-values for each atomic proposition and then calculate the value for the whole formula -- is clearly exponential. But this naive solution is very easy to write. For example, in Haskell we get something like the following:

import Data.List  ( nub )
import Data.Maybe ( fromJust )

data Formula = Var String | And Formula Formula |
              Or Formula Formula | Not Formula

getVarsDup (Var v)     = [v]
getVarsDup (And f1 f2) = (getVarsDup f1) ++ (getVarsDup f2)
getVarsDup (Or f1 f2)  = (getVarsDup f1) ++ (getVarsDup f2)
getVarsDup (Not f)     = getVarsDup f

genValues n = genAux $ [replicate n True]
   where genAux (v:vs)     = if not $ or $ v then v:vs
                             else genAux ((next v) : v : vs)
         next (True : ts)  = (False : ts)
         next (False : ts) = (True : (next ts))

solveFormula (Var v) env     = fromJust $ lookup v env
solveFormula (And f1 f2) env = (solveFormula f1 env) &&
                              (solveFormula f2 env)
solveFormula (Or f1 f2) env  = (solveFormula f1 env) ||
                              (solveFormula f2 env)
solveFormula (Not f) env     = not $ solveFormula f env

allSolutions f = map (solveFormula f) (map (zip vars) vals)
   where vars = nub $ getVarsDup f
         vals = genValues (length vars)

-- solve the SAT problem
sat f = or $ allSolutions f

-- pointfree!
sat2 = or . allSolutions

The idea is the same as creating a truth-table for the formula and then looking for a T in the possible values for it. Function genValues generates all possible values for the atomic propositions, and this is fed into solveFormula. It would be very easy to alter the code to output the complete truth-table; I leave it as an exercise to the reader. Another standard exercise in logic textbooks is to prove that if a formula contains n atomic propositions, the truth-table will have 2^n lines. Thus, generating all combinations is easily seen to be exponential in time.

But the fact that it is hard for the computer to solve doesn't mean that it's hard for someone to write a (naive) program to solve it. In practical applications, like circuit design, we may need to solve SAT for thousands of variables, and the naive algorithm would not work. For this we must use a more clever technique, like Binary Decision Diagrams. They're not that hard to code either; the book Expert F# includes an example of BDDs in F#.

Tumbalalaika

It's probably too late to be hip because of this now, but I have created a tumblelog. It's easier to post there, so it should be updated more often than this blog. I'll probably post a good number of links in common with anarchaia.

Functional programming in the mainstream

Here is a bit from Ted Neward, commenting on the outcome of his predictions for 2007:

THEN: Languages: Interest in functional-object hybrid languages will grow. Scala, Jaskell, F#, and others not-yet-invented will start to capture developers' attention, particularly when they hear the part about functional languages being easier to use in multi-core systems because it encourages immutable objects and discourages side effects (meaning we don't have to worry nearly so much about writing thread-safe code). NOW: It grew, and it continues to grow. New languages in general are being released (see Clojure, Jaskell, dynalang, and others), and lots of them are incorporating functional language concepts. If you've never programmed in Haskell, now's a good time to learn, because those concepts and syntax are fast making their way towards you...

Book review: Expert F#

Expert F#, by Don Syme, Adam Granicz and Antonio Cisternino, Apress

When a new programming language arrives and manages to make an impact, books about it will certainly appear. However, most often the books will be geared to beginners, to people that is either not very experienced in programming or in the programming paradigms embodied by the language. For a experienced programmer, these books stop right when the fun would begin: the advanced stuff, the corners, the details are left out.

Expert F#, as suggested by its title, is not like this: it is aimed at more experienced programmers. The book will not teach you, for instance, what is functional programming or hammer to your head the best ways to use lists, an ubiquitous data structure in functional languages. But it explains how the things work in F#, so that programmers already familiar with other functional languages will have no trouble picking it up. F# also has object-oriented capabilities, which are explained in a chapter, without however going much deep into OO concepts; the book is about the language, not the paradigms.

And it does this well. Roughly half of the book is about the language itself, the other half are examples of applications and how to use some important libraries. As I was already familiar with OCaml and Haskell, I mostly skimmed through chapters 1 to 4, reading more closely from chapters 5 (generic types) and 6 (how objects fit into F#). From chapter 7 (encapsulating and packaging your code) on, the book starts to get really interesting; the next one is about common techniques, and chapter 9 is the best in the first part, explaining language-oriented programming, an area where functional languages really shine.

There are mandatory chapters about Windows Forms (11), Web programming (14) using .NET and data access, including how to use LINQ in F#, but I really liked chapters 12 (working with symbolic representations), and 13 (concurrency and asynchronous workflows). The former includes two cool examples: a symbolic differentiator and a verifier for logic circuits based on BDDs (Binary Decision Diagrams). There are other important and advanced chapters treating topics like interoperation with C and COM, debugging and testing F# programs, and F# library design.

All in all a very good book about the best current functional language to use in the Windows platform. I have two minor quibbles about it, though: the first few chapters about the language really could be made more interesting (although it didn't affect me much, as I only skimmed them) and some of the more exciting new features of F# could be explained in more detail. Specifically, workflows and active patterns. They are quite recent additions to the language, however, and there is some additional material promised to feature in the book's site.

Anyway, I will keep this book nearby when programming in F#. It is this kind of book that you'd want to keep around, even after learning the language.

Do it yourself: Visual F# Express 2008

As noted in this post, if you want Visual Studio just to have an IDE to work with F#, you can get it for free. Now with Visual Studio 2008, Microsoft has released a bare-bones VS, without any language, that can be used with language extensions and plugins, as is the case of F#. This bare-bones VS is called Visual Studio 2008 Shell (integrated mode).

After downloading and installing VS 2008 Shell (it takes a lot of unpacking and installing), you can install F# 1.9.3.7 and voilà, you have a pretty good F# IDE in your box, without having to shell out any cash.

I tested it with F# version 1.9.3.7 in a machine running Windows XP SP2 and no previous version of Visual Studio installed, and it worked. I even compiled and ran some test projects. If it doesn't work at first, take a look at the original post.

Further news on World Domination

Don Syme blogs about taking F# forward, which means, it seems, that F# will leave the confines of MS Research and be fully integrated into Visual Studio, as a product. If this is right, it's a great step for F# as a language and for functional programming in general, as we'll have a first-class IDE, by a major vendor, shipping with a functional programming language.

F# is already a great language to use, so I look forward to it getting still greater. The next step for Microsoft is to embrace Visual Haskell and fully integrate Haskell in Visual Studio too :)

Review: OCaml for Scientists

When we think about what makes a programming book good, what separates a classic from a run-of-the-mill for-dummies-learn-in-X-days book, it's not hard to get to the conclusion that the examples are an important piece of what we perceive as quality. I would say that this is even more so for books on programming languages: K&R had great examples; Practical Common Lisp has great examples that are now being copied by many authors; the list could go on.

So it was not that surprising to discover that one of the reasons of all the praise received by Dr. Jon Harrop's book OCaml for Scientists is its set of examples. There are even two entire chapters devoted to examples, the first for simple and the second for more significative ones. They are really good: well-chosen, interesting and well-written. Most of them have a scientific flavor, in keeping with the book's title, but to me this is a plus. Also, I don't recall seeing wavelet transforms as examples in a programming language book before; originality also counts.

The book's title is accurate: it is a book about OCaml primarily targeted for scientific applications. But most of the topics covered are really useful to anyone wanting to learn the OCaml language. Of all the ten chapters, I would say only one -- Chapter 4, Numerical Analysis -- is mostly directed to scientists. Well, probably game programmers too. And programmers of computer graphics applications, and anyone using floating-point arithmetic. Anyway, the other chapters that have somewhat of a scientific bent are: Chapter 6, Visualization, which is really about how to use OpenGL and GLUT in OCaml, which is quite cool in itself; and Chapter 10, Complete Examples, but each example is well explained and can be (mostly) understood without previous knowledge.

To give some idea about the book's contents, here is a quick tour: Chapter 1 is a quick introduction, covering most important concepts of the core language. Chapter 2 is about how to structure bigger programs, including function nesting, modules, objects, and how to manage dependencies and compilation. Chapter 3 is a very interesting chapter on data structures in OCaml, beginning with a section on algorithmic complexity; it covers the more important containers provided in the library, and also how to implement and work with trees. Chapter 4 is the one about numerical analysis, covering the basics about doing calculations with limited-precision numbers, and how to use more precise forms of arithmetic. Chapter 5 tackles input and output in OCaml, going beyond the call of duty to present the lexer generator (ocamllex) and parser generator (ocamlyacc) in the OCaml toolset. Chapter 6 is about visualization with OpenGL and GLUT, Chapter 7 is a very good one about optimization, and Chapter 8 a very useful one about libraries. The final two chapters have examples, and don't be fooled by the title of Chapter 9, Simple Examples. There is good stuff there. There are also two appendices, about more advanced features and troubleshooting advice respectivelly.

To be fair, the book has some small weaknesses that, in the end, are not that important, if you consider its target audience and what's common OCaml style. One is the treatment of objects: it is very cursory, and one of the examples (about real and complex numbers) could easily be considered a bad case of OO design. Considering most OCaml programmers rarely use objects, this is not so troubling. The other weakness I'd like to cite is more of a wish from my part: I wish there were more about advanced topics, especially functors (only very lightly touched in Appendix A).

But it's really a very good book about OCaml, both for beginners and for people with some previous exposure to it. It has advice on good programming style throughout, great examples (shown in color, properly syntax-highlighted), and distilled practical experience on some important topics (optimization, using libraries) that is hard to get elsewhere. It is remarkable not only in the very restricted universe of OCaml books, but as a programming book, in general: it stands between the best I've seen.

Monads in OCaml

So, there. Someone who has never programmed in Haskell probably never encountered the idea of monads -- unless it is someone who works in semantics and has read Moggi's works; but I digress. An interesting way to tackle the idea of monads is to look at them outside of Haskell, and see how it works in other languages. Often, other languages don't have what it takes to express the concept of a monad in its full generality, but specific monads can always be implemented. In this regard, there's this page by oleg, and there's this other one about monads in Ruby. I remember seeing somewhere a page that compiled monad implementations in various languages, but I can't seem to find it now.

Anyhow, Brian Hurt has written a very nice tutorial about monads in OCaml. It uses the module system and functors (see comments) to define a reasonably general monad concept in OCaml. It's a good read.

Towards Global Domination

If you haven't yet seen them or heard about them somewhere else, it seems that the videos of Simon Peyton-Jones' talks at OSCON are quite a hit.

And people still look at me funny when I say that functional programming is going to take over the world.

Battle of the OCaml plugins for Eclipse

A new OCaml plugin for Eclipse, called OcaIDE, has just been announced. Apparently, it has been under development for a long time. It seems to be quite complete in features, although I didn't try it yet. The question is that this is the third OCaml plugin being developed currently; there's ODT, about which I talked in a earlier post, and another one being developed as one of the OCaml projects in the Google Summer of Code. The competition is good in some ways, but on the other hand the resulting fragmentation can be a problem to a small community like that of OCaml. It would be best if the teams managed to combine their efforts in some way. Let's see how this plays out.

Speaking of collaboration, there's mention on OcaIDE's site about a free-software license, but the source code doesn't seem to be available.

UPDATE: As someone pointed in the comments, the source is available together with the plugin. See here.

Review: Practical OCaml

Executive summary: this is not Practical Common Lisp for OCaml. It's ambitious but disappointing. However, it's not so bad as it seems at first sight.

OCaml is a sexy language that combines the expressiveness and terseness of scripting languages with the static type checking and performance of languages like C++ and Java. A book may be a good investment to learn a new language, and this is one of the few books available on the language. How does it fare?

This book has received very harsh criticism overall, and it mostly deserves it; it is somewhat of a mess. But it is not uniformly bad: some chapters are very bad, others are acceptable or interesting, depending on your background. The problem seems to be that the worst chapters come first; although it shows signs of bad editing throughout, the first few chapters are especially bad. And I mean really bad: bad text, bad editing, bad examples, lots of senseless repetition, conceptual errors, using language features not yet introduced (and that go unexplained), the list goes on. Later chapters are considerably less irritating.

Clearly inspired by Peter Seibel's terrific book Practical Common Lisp, the chapters on this one are divided in two types: the ones that explain the language, and the "Practical" ones, containing extended examples. This is a great idea, and even badly executed as it may be in Practical OCaml, it still results in interesting chapters. Actually, the Practical chapters are overall better than the language ones; from them, a reader can get a real sense of using OCaml in simple but realistic projects, integrating many different libraries and tools, some of them not contained in the standard OCaml distribution. Still, the code in these chapters can be criticized for their style. For one thing, I think the author uses classes and other OO features much more often than they appear on real OCaml programs. Nonetheless, an experienced programmer could get a lot of interesting pointers from these chapters, by knowing what to salvage and what not to replicate from the code.

But the rest of the book, the OCaml chapters, are in really bad shape. They don't explain things very well, and fails miserably at the more difficult aspects of the language. The chapter on modules and functors is so bad as to be almost useless; don't try to learn about functors from this book. Camlp4, the nifty tool for metaprogramming and extension, is other subject with a bad treatment. The chapter on Threads could be improved a lot, but it still gives a general idea of how multithreaded programming in OCaml is. Again, for experienced developers, it should provide pointers for further study.

If experienced developers can get something from this book, novice ones should stay away from it. Not only is the text confusing, but there are a lot of glaring conceptual errors. Maybe some errors are to be expected from a trade book, from an author that is not an academic, but there
are things that are completely confusing. For example, this is the definition of type (page 24): "A type is a thing (or a collection of things) or value." And there is a lot more like this, unfortunately.

Overall, it has interesting parts, but surely not enough to make worth the full cover price. For experienced programmers and people already familiar with other typed functional programming languages (Haskell, F#, SML, etc), the book could serve as an initial guide for OCaml programming, but there are better alternatives around.

F# Performance

There's a comparison of F# versus IronPython in Robert Pickering's blog. The results show that F# has roughly the same level of conciseness and terseness of Python, while being close in performance to C#. This is a .NET-based comparison, but it would be interesting to compare F# with CPython to see where it stands. If we are to believe this discussion on the python-dev mailing list, it seems that IronPython's performance must be comparable to CPython's, so there we have it: .NET or not, F# strikes an interesting balance in the expressiveness versus performance trade-offs.

This is also my personal experience with OCaml: performance roughly comparable to C/C++, but expressive and concise like scripting languages. It is this interesting position in the expressiveness x performance curve that makes both F# and OCaml very worthwhile languages to learn and use today.

The EOPL in F# wiki

I've started moving the content for the "EOPL in F#" translation to a wiki. Unfortunately, I have also been insanely busy as of late, so there's only the beginning there. However, as I'll have more free time from now on, I intend to catch up with what's already here and then start posting more sections that I already translated. I also noticed I never posted some parts because I forgot to, so it will be added to the wiki as well. Anyway, here is the link:

EOPL in F# Wiki

OCaml with Eclipse

The primary editor on which to write OCaml code has always been Emacs. This tends to be a problem for users on Windows, that mostly aren't familiar with the editor. And of course there are many people that use unix platforms and don't like Emacs.

A good alternative is Eclipse, which has very good plugins for Java programming, and can be extended to handle other languages. ODT, a plugin for OCaml development in Eclipse, is being actively developed by Emmanuel Dieul. Actually there's another plugin in development by someone under the Google Summer of Code, and we hope they can integrate both efforts to get a better plugin in the end.

Anyway, ODT looks interesting right now, and it's been evolving quite fast. Eclipse is quite a memory hog, but if you already use it or are willing to pay the requirements, it can provide a modern IDE for OCaml under Windows or unix, and a good alternative for Emacs. Let's hope ODT keeps improving.

Great news in the Haskell Books front

This was recently announced and everyone must already know about it (I was away at a conference), but just in case: O'Reilly will publish a book about Haskell called Real-World Haskell, written by people very active in the Haskell community. Such a book from O'Reilly has the potential to seriously increase Haskell's popularity, and familiarize more people with functional programming.

Considering that a book about F# is already out and another one is on the way, and that APress recently published a book on OCaml (it doesn't seem to be very good, unfortunately), I guess functional programming is really getting more popular.

Maybe there's hope that Haskell will take over the world and everyone will use monads and pure lazy functional programming :)

The EOPL in F# thing

I have translated more of the EOPL book into F#, but the examples keep growing and proving how unfit the whole enterprise is to the blog format. I knew this from the beginning, and would prefer a wiki, but then I couldn't find a decent wiki server. I may have found one now, and if all goes well I'll link to it here after moving there some of the contents posted here. After this, I don't know if this blog will still be useful, but I'll wait and see.

Functional programming in Wall Street

The latest issue of Monad.Reader (a electronic magazine about Haskell) includes an interesting article about Jane Street Capital (a Wall Street trading company) and its use of OCaml. The author points good and bad things about the language; these aren't new, in fact the things pointed are well-known by the community, but it's good to hear them from someone using the language in a production setting.

Anyway, it's a case of large-scale adoption -- in the sense of using it as the main language for all development -- of a functional programming language, which is still rare, unfortunately.

One Language to Rule Them All

A discussion on LtU about the Next Big language, the next Java or something like it. Links to the post by Steve Yegge too. Once again Scala is mentioned as a fine language that anyone needing to develop for the JVM should try.

I don't believe Scala will be the next big language, but it really is fine. At the moment I'm finishing implementation of a simple distributed system written in Scala. It had to run on the JVM to communicate with other Java programs. It was a breeze to do, thanks to the Actors library. Scala's type system is quite interesting too, I plan on giving more attention to it when I have the time.

EOPL - 3.2 - Exercise 3.5

Exercise 3.5 asks you to add a print primitive to the language, which prints its argument and returns the value 1. The relevant changes are simple. In module Eopl_3 only the definition of type Primitive and function apply_primitive are different:

// in eopl_3.fs (module Eopl_3)
type Primitive = AddPrim | SubtractPrim | MultPrim | IncrPrim 
               | DecrPrim | PrintPrim

let apply_primitive prim args = 
    match (prim, args) with
      (AddPrim, [a; b]) -> a + b
    | (SubtractPrim, [a; b]) -> a - b
    | (MultPrim, [a; b]) -> a * b
    | (IncrPrim, [a]) -> a + 1
    | (DecrPrim, [a]) -> a - 1
    | (PrintPrim, [a]) -> (print_endline (string_of_int a); 1)
    | _ -> failwith "Incorrect argument list for primitive" 

In the lexer specification a token for the print primitive is added:

rule token = parse
| whitespace { token lexbuf }
| '%' [^ '\n']* { token lexbuf } 
| newline       { record_newline lexbuf; token lexbuf }
| "+"         { PLUS }
| "-"         { MINUS }
| "*"  { MULT }
| "("           { LPAREN }
| ")"         { RPAREN }
| ","           { COMMA  }
| "add1" { INCR }
| "sub1" { DECR }
| "print"       { PRINT }
| id         { ID(lexeme lexbuf) }
| ['-']?digit+  { LIT (Int32.Parse(lexeme lexbuf)) }
| eof   { EOF }

And, in the parser, this token must be declared and dealt with:

%token PRINT INCR DECR LPAREN RPAREN PLUS MINUS MULT COMMA EOF

Prim: PLUS                        { AddPrim }
    | MINUS                       { SubtractPrim }
    | MULT                        { MultPrim }
    | INCR                        { IncrPrim }
    | DECR                        { DecrPrim }
    | PRINT                       { PrintPrim }

The remaining parts of these three files are the same as the previous two posts.

Scala web programming

A post on Lambda the Ultimate pointing to this post on David Pollak's blog. In a comment on the Lambda thread, he writes some points about what makes Scala a good language for web programming, comparing with Java and Ruby (with Rails). Having used all three, he gets to the conclusion that Scala has the best of the other two.