I can sort of make sense of this, but I don't know enough OCaml or FbInfer to really grok it. Why would this be a particularly good example of how OCaml simplifies symbolic evaluation?

Thank you, by the way! Actual code examples are kind of exactly what I'd like to see.

If I oversimplify I would say that due to pattern matching and functional nature of OCaml you can avoid much of the boilerplate code needed for building tree nodes, or finding the node you want, allowing you to focus on the high-level task you want to actually achieve.

In fact one thing that you might notice in the beginning when reading OCaml is that the code seems more "dense". In C I was used to reading code by skipping over large chunks of it (again I'm oversimplifying here) like the one below, and one of the things I had to get used to when learning OCaml was to slow down and avoid skipping large chunks of code:

   if (some_complex_condition == failed) {
     /* ... large block of code for error handling to ignore on first read .. */
   }
   
   result = malloc(...);
   result->... = ...;
   result->... = ....;

Here are some examples of what is possible with symbolic manipulation in OCaml, although I would recommend learning a bit of OCaml syntax and concepts from a book first (such as Real World OCaml):

A short example of implementing regular expression matching using Antimirov's partial derivatives that illustrates symbolic manipulation: http://semantic-domain.blogspot.ro/2013/11/antimirov-derivat...

A step-by-step explanation of a DSL optimizer that doesn't use too many advanced notions of OCaml: http://okmij.org/ftp/tagless-final/course/optimizations.html

A nice example of symbolic manipulation is this counter-example generator for regular expression equivalence: http://perso.ens-lyon.fr/damien.pous/symbolickat/

Not from pfff/FbInfer, but Benjamin Pierce's excellent book on types (Types and Programming Languages) uses OCaml as well, with heavy use of pattern matching on AST.

Here is one example, in this case type-checking a ternary operator (from http://www.cis.upenn.edu/~bcpierce/tapl/checkers/tyarith/cor...):

   | TmIf(fi,t1,t2,t3) ->
     if (=) (typeof t1) TyBool then
       let tyT2 = typeof t2 in
       if (=) tyT2 (typeof t3) then tyT2
       else error fi "arms of conditional have different types"
     else error fi "guard of conditional not a boolean"

In addition to pattern matching, SML and Ocaml are popular languages for this type of work as some of the graph algorithms used in static analysis are easier expressed with eager evaluation and mutability. I am guessing there are commonly accepted idioms and libraries around the use of functors, monads, applicatives, etc.. for doing these things in Haskell; there is a Haskell version of TAPL examples (as well as a Scala one). Here's a talk from Intel about their use of SML in this field, which (in a collegial manner) mocked Haskell by saying in a slide "yeah, I am sure Simon Peyton Jones has a paper on it somewhere..." (note: I attended this talk at CUFP in 2010... IIRC Simon Peyton Jones was in the room when this remark was made :-))

A great deal of this also seems to be convention/pragmatism: e.g., pfff and Hack are in OCaml -- and predate the use of Haskell at FB -- hence FbInfer is as well. Coq, which is often used for proofs of correctness of type systems, is in OCaml so someone who already uses/hacks on Coq might as well use OCaml for implementation work.

Yes you right, I am not exactly clear. My understanding of symbolic manipulation is the following (from wikipedia):

"In mathematics and computer science, computer algebra, also called symbolic computation or algebraic computation is a scientific area that refers to the study and development of algorithms and software for manipulating mathematical expressions and other mathematical objects."

Now obviously if you have types in your language that make this easier than it is a win. I thought algebraic data types makes this easier. I might be wrong. On the pattern matching side, you are not concerned about the actual value of the variables in your expressions rather the patters those are matching to. That was my intention to show with the second URL in the previous comment, but again I might be wrong on that too.