OCaml Planet

November 24, 2015

OCaml Labs compiler hacking

Eleventh OCaml compiler hacking evening at Pembroke College

It's time for the eleventh Cambridge OCaml compiler-hacking evening! This time we're heading to central Cambridge, to enjoy all that Pembroke College has to offer.

If you're planning to come along, it'd be helpful if you could indicate interest via Doodle and sign up to the mailing list to receive updates.

Where: Outer Parlour, Pembroke College, Cambridge CB2 1RF. Head through the entrance on Trumpington Street, and we'll be there at the Porter's Lodge to direct you.

When: 6pm, Monday 30th November

Who: anyone interested in improving OCaml. Knowledge of OCaml programming will obviously be helpful, but prior experience of working on OCaml internals isn't necessary.

What: fixing bugs, implementing new features, learning about OCaml internals

Wiki: https://github.com/ocamllabs/compiler-hacking/wiki

We're defining "compiler" pretty broadly, to include anything that's part of the standard distribution, which means at least the standard library, runtime, tools (ocamldep, ocamllex, ocamlyacc, etc.), camlp4, ocamlbuild, the documentation, OPAM, and the compiler itself. We'll have suggestions for mini-projects for various levels of experience, but feel free to come along and work on whatever you fancy.

Drinks and finger buffet will be provided.

by OCaml Labs (cl-ocamllabs@lists.cam.ac.uk) at November 24, 2015 12:00 PM

November 22, 2015


Visualise Randomness


It has been almost half year since my last blog post on OCaml. Well, actually I haven't even touched OCaml for that long time. My current job (in Python) got much busier and was buying a new home for my family.

Honestly, buying a home in UK is really frustrating. I had to take care of this, that, constantly talking to lawyer, sales, developer, etc. The whole process took me like 3 months. In August, we moved in our beloved new home, happy, but immediately started to worry about furnitures, etc.

In September, I had a trip to the Hongkong office of my company (I really love Hongkong, see the photo I took as below) for a week and 2 weeks of holidays afterwards. Finally back to London, still busy job tasks, home stuff ...


For the past half year, my life had never been so busy. But finally, things camls calms down a bit now. I can at least have time sitting in front of my 2008 macbook pro, opening terminal, doing

opam update

opam upgrade

opam switch 4.02.3

eval `opam config env`

Hmmmm, I like this feeling.

typeocaml is back now. I digged my typeocaml notebook from one of our 78 packing boxes, and went through the list of many things about OCaml that I planned to write about. Those items still look familiar but obviously not very clear in my mind now. One should never put a vacuum space in things beloved. They would fade.

Anyway, enough chit-chat, back to the topic.

This post is about visualising the randomness of random number generators. It will be lightweight and is just something I did for fun with OCaml. We will know a good way to test randomness and also learn how to create a jpg picture using an OCaml image library: camlimages. I hope it would be tiny cool.

What is randomness?

Say, we got a function var ran_gen : int -> int from nowhere. It claims to be a good random integer generator with uniform distribution, which takes a bound and "perfectly" generates a random integer within [0, bound). The usage is simple but the question is can you trust it or will the numbers it generates be really random?

For example, here is a rather simple ran_gen_via_time:

let decimal_only f = f -. (floor f)  
let ran_via_time bound =  
  ((Unix.gettimeofday() |> decimal_only) *. 100,000,000. |> int_of_float) mod bound
  Unix.gettimeofday() returns float like 1447920488.92716193 in second. 
  We get the decimal part and then amplify it to be integer like, i.e., 1447920488.92716193 ==> 0.92716193 ==> 92716193.
  Then we mod it by bound to get the final "random" number.

This generator is based on the timestamp when it is called and then mod by the bound. Will it be a good generator? My gut tells me not really. If the calls to the function has some patterns, then eaily the numbers become constant.

For example, if the bound is 10, then at t I make first call, I will get t mod 10. If I call at t + 10 again, I will get (t+10) mod 10 which is actually t mod 10. If I call it every 10 seconds, then I get a constant. Thus this generator's randomness would not be as good as it claims to be.

For any given random number generator, we have to really make sure its randomness is good enough to suite our goal, especially when we have to rely on them for trading strategies, gaming applications, online gambling hosting, etc.

However, we also need to be aware of that most of random generators are not perfect (Random number generator and Pseudorandom number generator). What we often do is just to see whether the randomness of a given generator can reach a certain level or not.

Test randomness using statistics

Chi-squared test is a fairly simple and common methodology to test randomness mathematically.

Say, we have a generator producing random integers between [0, 10) with uniform distribution. So ideally, if the generator is perfect, and if we ran 1000 times, then there would be 100 of 0, 100 of 1, ..., 100 of 9 , right? For the test, we can just try the generator N times, and see whether the frequency of each number generated somehow matches or is close to N / bound.

Of course, the frquencies of numbers would not exactly match expectation. So we need some mathematics to measure the level of matching.

  1. k is the number of possible candidates - e.g., k = 10 for [0, 10)
  2. Ei is the expected frequency for each candidate - i = 1, 2, k
  3. Oi is the frequency for each candidate produced by the generator - i = 1, 2, k

Thus we can get X^2 = (O1-E1)^2/E1 + ... + (Ok-Ek)^2/Ek

Essentially, the bigger X^2 is, the matching is more unlikely. If we really want to see how unlikely or likely they match each other, then we need to check X^2 against the chi square distribution table like below:

chi square distribution table

  1. The Degrees of Freedom is our k-1 (if k = 1, then our freedom is 0, which means we just have one to choose all the time and don't have any freedom).
  2. The bold headings of columns are the probabilities that the observations match the expectations.
  3. The many numbers in those cells are values of X^2.

For example, say in our case above, k = 10, so Degree of freedom is 9.

If we get X^2 as 2, which is less than 2.088, then we can say we have more than 0.99 probability that the observations match the expectations, i.e., our random generator follows uniform distribution very well.

If we get X^2 as 23, which is bigger than 21.666, the probability of matching is less than 0.01, so our generator at least is not following uniform distribution.

This is roughly how we could use Chi-squared test for randomness checking. Of course, the description above is amateur and I am just trying to put it in a way for easier understanding.

Test randomness via visualisation

Let's admit one thing first: Math can be boring. Although math can describe things most precisely, it does not make people like me feel intuitive, or say, straightforward. If I can directly see problems and the solutions via my eyes, I would be much happier and this was the reason why I tried to visualise the randomness of generators.

The way of the visualisation is fairly simple.

  1. We create a canvas.
  2. Each pixel on the canvas is a candidate random number that the generator can produce.
  3. We run the generator for lots of times.
  4. The more times a pixel gets hit, we draw a deeper color on it.
  5. In the end, we can directly feel the randomness depending on the color distribution on the canvas.

A trivial example

Initially we have such a canvas.


We use the random generator generating numbers. If a slot get a hit, we put a color on it.


If any slot keeps been hit, we put deeper and deeper color on it.


When the generator finishes, we can get a final image.


From the resulting image, we can see that several numbers are really much deeper than others, and we can directly get a feeling about the generator.

Of course, this is just trivial. Normally, we can get much bigger picture and see the landscape of the randomness, instead of just some spots. Let's get our hands dirty then.


Assuming the essentials of OCaml, such as ocaml itself, opam and ocamlbuild, have been installed, the only 3rd party library we need to get now is camlimagges.

Before invoke opam install camlimages, we need to make sure libjpeg being installed first in your system. Basically, camlimages relies on system libs of libjpeg, libpng, etc to save image files in respective formats. In this post, we will save our images to .jpg, so depending on the operating system, we can just directly try installing it by the keyword of libjpeg.

For example,

  • mac -> brew install libjpeg;
  • ubuntu -> apt-get install libjpeg;
  • redhat -> yum install libjpeg

After libjpeg is installed, we can then invoke opam install camlimages.

In addition, for easier compiling or testing purposes, maybe ocamlbuild opam install ocamlbuild and utop opam install utop could be installed, but it is up to you.

brew install libjpeg  
opam install camlimages  
opam install ocamlbuild  
opam install utop  

The general process

The presentation of an RGB image in memory is a bitmap, which is fairly simple: just an 2-d array (width x height) with each slot holding a color value, in a form like (red, green, blue). Once we have such a bitmap, we can just save it to the disk in various formats (different commpression techniques).

So the process could be like this:

  1. Create a matrix array, with certain size (width and height)
  2. Manipulate the values (colors) of all slots via random generated numbers
  3. Convert the matrix bitmap to a real image
  4. Save the image to a jpg file

Fill the matrix

First, let's create a matrix.

open Camlimages

(* w is the width and h is the height *)
let bitmap = Array.make_matrix w h {Color.r = 255; g = 255; b = 255}  
  Color is a type in camlimages for presenting RGB colors,
  and initially white here.

When we generate a random number, we need to map it to a slot. Our image is a rectangle, i.e., having rows and columns. Our random numbers are within a bound [0, b), i.e., 1-d dimension. A usual way to convert from 1-d to 2-d is just divide the number by the width to get the row and modulo the number by the width to get the col.

let to_row_col ~w ~v = v / w, v mod w  

After we get a random number, we now need to fill its belonging slot darker. Initially, each slot can be pure white, i.e., {Color.r = 255; g = 255; b = 255}. In order to make it darker, we simply just to make the rgb equally smaller.

let darker {Color.r = r;g = g;b = b} =  
  let d c = if c-30 >= 0 then c-30 else 0 
  {Color.r = d r;g = d g;b = d b}
  The decrement `30` really depends on how many times you would like to run the generator 
  and also how obvious you want the color difference to be.

And now we can integrate the major random number genrations in.

  ran_f: the random number generator function, produce number within [0, bound)
         fun: int -> int
  w, h:  the width and height
  n:     the expected times of same number generated

  Note in total, the generator will be called w * h * n times.
let random_to_bitmap ~ran_f ~w ~h ~n =  
  let bitmap = Array.make_matrix w h {Color.r = 255; g = 255; b = 255} in
  let to_row_col ~w ~v = v / w, v mod w in
  let darker {Color.r = r;g = g;b = b} = let d c = if c-30 >= 0 then c-30 else 0 in {Color.r = d r;g = d g;b = d b} 
  for i = 1 to w * h * n do
    let row, col = to_row_col ~w ~v:(ran_f (w * h)) in
    bitmap.(row).(col) <- darker bitmap.(row).(col);

Convert the matrix to an image

We will use the module Rgb24 in camlimages to map the matrix to an image.

let bitmap_to_img ~bitmap =  
  let w = Array.length bitmap in
  let h = if w = 0 then 0 else Array.length bitmap.(0) in
  let img = Rgb24.create w h in
  for i = 0 to w-1 do
    for j = 0 to h-1 do
      Rgb24.set img i j bitmap.(i).(j)

Save the image

Module Jpeg will do the trick perfectly, as long as you remembered to install libjpeg before camlimages arrives.

let save_img ~filename ~img = Jpeg.save filename [] (Images.Rgb24 img)  

Our master function

By grouping them all together, we get our master function.

let random_plot ~filename ~ran_f ~w ~h ~n =  
  let bitmap = random_to_bitmap ~ran_f ~w ~h ~n in
  let img = bitmap_to_img ~bitmap in
  save_img ~filename ~img

All source code is in here https://github.com/MassD/typeocaml_code/tree/master/visualise_randomness

Result - standard Random.int

OCaml standard lib provides a random integer genertor:

val int : int -> int

Random.int bound returns a random integer between 0 (inclusive) and bound (exclusive). bound must be greater than 0 and less than 230.  

Let's have a look what it looks like:

let _ = random_plot ~filename:"random_plot_int.jpg" ~ran_f:Random.int ~w:1024 ~h:1024 ~n:5  


Is it satisfying? Well, I guess so.

Result - ran_gen_via_time

Let's try it on the ran_gen_via_time generator we invented before:

let decimal_only f = f -. (floor f)  
let ran_via_time bound =  
  ((Unix.gettimeofday() |> decimal_only) *. 100,000,000. |> int_of_float) mod bound

let _ = random_plot ~filename:"random_plot_time.jpg" ~ran_f:ran_via_time ~w:1024 ~h:1024 ~n:5  


Is it satisfying? Sure not.

Apparently, there are quite some patterns on images. Can you identify them?

For example,


One pattern is the diagonal lines there (parrallel to the red lines I've added).

Only quick and fun

Of course, visualisation of randomness is nowhere near accurately assess the quality of random geneators. It is just a fun way to feel its randomness.

I hope you enjoy it.


Pointed by Ono-Sendai on hacker news, it might be better to use png rather than jpg.

I've tried and the results for the bad ran_gen_via_time are like:





Seems not that different from my eyes. But anyway it was a good point.

https://github.com/MassD/typeocaml_code/blob/master/visualise_randomness/plot_random.ml has been updated for png support. Please remember to install libpng-devel for your OS for png saving support.

Fortuna random generator from nocrypto

@h4nnes has suggested me to try the fortuna generator from nocrypto.

opam install nocrypto  


let _ = Nocrypto_entropy_unix.initialize()  
let _ = random_plot ~filename:"random_plot_fortuna" ~ran_f:Nocrypto.Rng.Int.gen ~w:1024 ~h:1024 ~n:5  

and we get


It is a very nice generator, isn't it?

by Jackson Tale at November 22, 2015 01:14 PM

November 16, 2015

Erik de Castro Lopo

Forgive me Curry and Howard for I have Sinned.

Forgive me Curry and Howard for I have sinned.

For the last several weeks, I have been writing C++ code. I've been doing some experimentation in the area of real-time audio Digital Signal Processing experiments, C++ actually is better than Haskell.

Haskell is simply not a good fit here because I need:

  • To be able to guarantee (by inspection) that there is zero memory allocation/de-allocation in the real-time inner processing loop.
  • Things like IIR filters are inherently stateful, with their internal state being updated on every input sample.

There is however one good thing about coding C++; I am constantly reminded of all the sage advice about C++ I got from my friend Peter Miller who passed away a bit over a year ago.

Here is an example of the code I'm writing:

  class iir2_base
      public :
          // An abstract base class for 2nd order IIR filters.
          iir2_base () ;

          // Virtual destructor does nothing.
          virtual ~iir2_base () { }

          inline double process (double in)
              unsigned minus2 = (minus1 + 1) & 1 ;
              double out = b0 * in + b1 * x [minus1] + b2 * x [minus2]
                              - a1 * y [minus1] - a2 * y [minus2] ;
              minus1 = minus2 ;
              x [minus1] = in ;
              y [minus1] = out ;
              return out ;

      protected :
          // iir2_base internal state (all statically allocated).
          double b0, b1, b2 ;
          double a1, a2 ;
          double x [2], y [2] ;
          unsigned minus1 ;

      private :
          // Disable copy constructor etc.
          iir2_base (const iir2_base &) ;
          iir2_base & operator = (const iir2_base &) ;
  } ;

November 16, 2015 11:22 AM

November 11, 2015


Coq 8.5 beta 3 is out!

The third beta release of Coq 8.5 is available for testing. The 8.5 version brings several major features to Coq:
  • asynchronous edition of documents under CoqIDE to keep working on a proof while Coq checks the other proofs in the background (by Enrico Tassi);
  • universe polymorphism making it possible to reuse the same definitions at various universe levels (by Matthieu Sozeau);
  • primitive projections improving space and time efficiency of records, and adding eta-conversion for records (by Matthieu Sozeau);
  • a new tactic engine allowing dependent subgoals, fully backtracking tactics, as well as tactics which can consider multiple goals together (by Arnaud Spiwack);
  • a new reduction procedure called native_compute to evaluate terms using the OCaml native compiler, for proofs with large computational steps (by Maxime Dénès).
More information about the changes from 8.4 to 8.5 and since the first two beta releases can be found in the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy!

by Maxime Dénès at November 11, 2015 07:30 PM

Functional Jobs

Software Engineer - Functional Programmer - Erlang at Change Healthcare (Full-time)

Job Description

Change Healthcare is a leading provider of United States healthcare solutions. Our division is responsible for consumer engagement and transparency. We have a very lean, Agile team with a rapid deployment schedule for processing X12 in Erlang doing insurance calculations. Functional programming in Erlang has created a robust, scalable foundation for our organization.

What You Could Be Working On:

Full product life-cycle development, working with product management to production delivery for multiple clients. Team environment is a product manager, a QA, 2 developers and 1 architect. Cross team cooperation with Ops and Data is required. X12 transaction processing applies across the US for electronic data interchange, and is used extensively in healthcare. JIRA and git are key tools in the daily workflow.

Where You Will Work:

Our office in Nashville, TN is a casual open cube plan with a motto of work hard, play hard. Foosball play is competitive, and individual creativity is valued here at Change Healthcare. Nashville is a great place to live, and is growing rapidly like Change Healthcare

What We Commit to YOU:

  • You will get to work with one of the most innovative teams in the IT marketplace and solve real strategic problems in a 99.99% uptime production environment.
  • We will invest in things that are important to you both professionally and personally.
  • We will provide you with a team environment like no other – we are listed in the "100 Best Places to Work in Healthcare".
  • We will build a relationship with you to accelerate your Career.
  • We provide some of the best benefits around.

What Is Required:

  • Have 3+ years experience with a functional language (e.g. Lisp, Scheme, F#, OCAML, Erlang, Haskell).
  • Ability to identify, communicate and push toward resolution of requirement gaps.
  • A Bachelors degree in computer science is a major plus.
  • Passion and pride in your personal work product.
  • Ability to work with a team, and hand off work as needed to drive towards hard delivery dates.
  • Worked with Restful API design.
  • Experience with scalable parallel solution design.
  • Experience with writing test cases

Get information on how to apply for this position.

November 11, 2015 04:07 PM

November 07, 2015

Andrej Bauer

Agda Writer

My student Marko Koležnik is about to finish his Master’s degree in Mathematics at the University of Ljubljana. He implemented Agda Writer, a graphical user interface  for the Agda proof assistant on the OS X platform. As he puts it, the main advantage of Agda Writer is no Emacs, but the list of cool features is a bit longer:

  • bundled Agda: it comes with preinstalled Agda so there is zero installation effort (of course, you can use your own Agda as well).
  • UTF-8 keyboard shortcuts: it is super-easy to enter UTF-8 characters by typing their LaTeX names, just like in Emacs. It trumps Emacs by converting ASCII arrows to their UTF8 equivalents on the fly. In the preferences you can customize the long list of shortcuts to your liking.
  • the usual features expected on OS X are all there: auto-completion, clickable error messages and goals, etc.

Agda Writer is open source. Everybody is welcome to help out and participate on the Agda Writer repository.

Who is Agda Writer for? Obviously for students, mathematicians, and other potential users who were not born with Emacs hard-wired into their brains. It is great for teaching Agda as you do not have to spend two weeks explaining Emacs. The only drawback is that it is limited to OS X. Someone should write equivalent Windows and Linux applications. Then perhaps proof assistants will have a chance of being more widely adopted.

by Andrej Bauer at November 07, 2015 11:06 AM

November 05, 2015

Github OCaml jobs

Full Time: Software Developer (Functional Programming) at Jane Street in New York, NY; London, UK; Hong Kong

Software Developer

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 400 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still. Every day, we have new problems to solve and new theories to test. Our entrepreneurial culture is driven by our talented team of traders and programmers. At Jane Street, we don't come to work wanting to leave. We come to work excited to test new theories, have thought-provoking discussions, and maybe sneak in a game of ping-pong or two. Keeping our culture casual and our employees happy is of paramount importance to us.

We are looking to hire great software developers with an interest in functional programming. OCaml, a statically typed functional programming language with similarities to Haskell, Scheme, Erlang, F# and SML, is our language of choice. We've got the largest team of OCaml developers in any industrial setting, and probably the world's largest OCaml codebase. We use OCaml for running our entire business, supporting everything from research to systems administration to trading systems. If you're interested in seeing how functional programming plays out in the real world, there's no better place.

The atmosphere is informal and intellectual. There is a focus on education, and people learn about software and trading, both through formal classes and on the job. The work is challenging, and you get to see the practical impact of your efforts in quick and dramatic terms. Jane Street is also small enough that people have the freedom to get involved in many different areas of the business. Compensation is highly competitive, and there's a lot of room for growth.

You can learn more about Jane Street and our technology from our main site, janestreet.com. You can also look at a a talk given at CMU about why Jane Street uses functional programming (http://ocaml.janestreet.com/?q=node/61), and our programming blog (http://ocaml.janestreet.com).

We also have extensive benefits, including:

  • 90% book reimbursement for work-related books
  • 90% tuition reimbursement for continuing education
  • Excellent, zero-premium medical and dental insurance
  • Free lunch delivered daily from a selection of restaurants
  • Catered breakfasts and fresh brewed Peet's coffee
  • An on-site, private gym in New York with towel service
  • Kitchens fully stocked with a variety of snack choices
  • Full company 401(k) match up to 6% of salary, vests immediately
  • Three weeks of paid vacation for new hires in the US
  • 16 weeks fully paid maternity/paternity leave for primary caregivers, plus additional unpaid leave

More information at http://janestreet.com/culture/benefits/

November 05, 2015 09:51 AM

November 03, 2015

Amir Chaudhry

CodeMesh 2015

<script async="" class="speakerdeck-embed" data-id="3035d63437234495ad1cddc117321ff0" data-ratio="1.33333333333333" src="http://speakerdeck.com/assets/embed.js"></script>

These are the slides from my talk today at CodeMesh. This time around I was earlier in the schedule so I get to enjoy the rest of the conference! If you’re reading this at the conference now, please do follow the link in my talk to rate it and give me feedback!

The specific items I reference in the talk are below with links to more information.

Security and the Bitcoin Piñata

This is a bounty where we have locked away some bitcoin in a unikernel that is running our new TLS stack. This was a new model of running a bounty and has proven a great way to stress test the code in the wild.

You can follow up with more of the background work on the TLS stack by looking at the paper, “Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation” and find other users of the libraries via https://nqsb.io.

Automated deployment

I’ve previously written about how we do unikernel deployments for MirageOS. Although the scripts themselves have evolved and become more sophisticated, these are still a good introduction.

Summoning on demand

The work on summoning unikernels was presented at Usenix this year and you can read the paper, “Jitsu: Just-In-Time Summoning of Unikernels”. The example I showed in the talk can be found at http://www.jitsu.v0.no.

Other resources

To get involved in the development work, please do join the MirageOS devel list and try out some of the examples for yourselves!

by Amir Chaudhry at November 03, 2015 11:15 AM