## December 01, 2015

## November 30, 2015

### Shayne Fletcher

#### C++ : Sums with constructors

## C++ : Sums with constructors

I've been working recently on a type to model "sums with constructors" in C++ (ala OCaml). The implementation technique is "novel" in that it makes use of C++11's "unrestricted unions" feature. I learned it from the FTL library where the idea is credited to Björn Aili. FTL also shows how to provide a NEAT (for C++) syntax for pattern matching but, unless I just didn't get it, the FTL version doesn't admit recursive types "out-of-the-box". So, I extended Björn's work to admit recursive types by applying the recursive wrapper idea from Boost.Variant (Eric Friedman, Itay Maman). The resulting library, I call the "pretty good sum" library. It's C++14 but can be back-ported to C++11 I think. The code is online here if you want to play with it in your own programs.

There are a number of usage examples provided in the library tests/documentation. I'll provide a small one here - the ubiquitous `option`

` type (c.f. Boost.Optional and OCaml's builtin `

`type α option`

).

`In OCaml, the type definition is given by `

type α option = Some of α | None

`which is not recursive (see the other examples on github for that e.g. functional lists, abstract syntax trees) but I hope this example is still interesting in that it explores the type's monadic nature to implement so called "safe-arithmetic", that is, integer arithmetic that guards against overflow and division by zero (source : "Ensure that operations on signed integers do not result in overflow"). See this post for more on monads in C++. `The code in the example is fairly extensively commented so I hope you will excuse me this time if I don't provide my usual narrative (I've presented this program before in a Felix tutorial - there's a narrative there *note to self : and some typos that I mean to get back to and fix*).

Without further ado... A type for optional values in C++ using the "pretty good sum" type!

#include <gtest/gtest.h>

#include "sum_type.hpp"

#include <iostream>

#include <cstdlib>

//type 'a t = Some of 'a | None

namespace {

using namespace pgs;

template <class T>

struct some_t { //Case 1

T data;

template <class U>

explicit some_t (U&& data) : data (std::forward<U> (data))

{}

};

struct none_t //Case 2

{};

//Options are a type that can either hold a value of type `none_t`

//(undefined) or `some_t<T>`

template<class T>

using option = sum_type<some_t<T>, none_t>;

//A trait that can "get at" the type `T` contained by an option

template <class>

struct option_value_type;

template <class T>

struct option_value_type<option<T>> { typedef T type; };

template <class T>

using option_value_type_t = typename option_value_type<T>::type;

//Factory function for case `none_t`

template <class T>

option<T> none () {

return option<T>{constructor<none_t>{}};

}

//Factory function for case `some_t<>`

template <class T>

option<T> some (T&& val) {

return option<T>{constructor<some_t<T>>{}, std::forward<T> (val)};

}

//is_none : `true` if a `some_t<>`, `false` otherwise

template<class T>

bool is_none (option<T> const& o) {

return o.match<bool> (

[](some_t<T> const&) { return false; },

[](none_t const&) { return true; }

);

}

//is_some : `false` if a `none_t`, `true` otherwise

template<class T>

inline bool is_some (option<T> const& o) {

return !is_none (o);

}

//Attempt to get a `const` reference to the value contained by an

//option

template <class T>

T const& get (option<T> const & u) {

return u.match<T const&> (

[](some_t<T> const& o) -> T const& { return o.data; },

[](none_t const&) -> T const& { throw std::runtime_error {"get"}; }

);

}

//Attempt to get a non-`const` reference to the value contained by an

//option

template <class T>

T& get (option<T>& u) {

return u.match<T&> (

[](some_t<T>& o) -> T& { return o.data; },

[](none_t&) -> T& { throw std::runtime_error {"get"}; }

);

}

//`default x (Some v)` returns `v` and `default x None` returns `x`

template <class T>

T const& default_ (T const& x, option<T> const& u) {

return u.match<T const&> (

[](some_t<T> const& o) -> T const& { return o.data; },

[=](none_t const&) -> T const& { return x; }

);

}

//`map_default f x (Some v)` returns `f v` and `map_default f x None`

//returns `x`

template<class F, class U, class T>

auto map_default (F f, U const& x, option<T> const& u) -> U {

return u.match <U> (

[=](some_t<T> const& o) -> U { return f (o.data); },

[=](none_t const&) -> U { return x; }

);

}

//Option monad 'bind'

template<class T, class F>

auto operator * (option<T> const& o, F k) -> decltype (k (get (o))) {

using result_t = decltype (k ( get (o)));

using t = option_value_type_t<result_t>;

return o.match<result_t>(

[](none_t const&) { return none<t>(); },

[=](some_t<T> const& o) { return k (o.data); }

);

}

//Option monad 'unit'

template<class T>

option<T> unit (T&& a) {

return some (std::forward<T> (a));

}

//map

template <class T, class F>

auto map (F f, option<T> const& m) -> option<decltype (f (get (m)))>{

using t = decltype (f ( get (m)));

return m.match<option<t>>(

[](none_t const&) { return none<t>(); },

[=](some_t<T> const& o) { return some (f (o.data)); }

);

}

}//namespace<anonymous>

TEST (pgs, option) {

ASSERT_EQ (get(some (1)), 1);

ASSERT_THROW (get (none<int>()), std::runtime_error);

auto f = [](int i) { //avoid use of lambda in unevaluated context

return some (i * i); };

ASSERT_EQ (get (some (3) * f), 9);

auto g = [](int x) { return x * x; };

ASSERT_EQ (get (map (g, some (3))), 9);

ASSERT_TRUE (is_none (map (g, none<int>())));

ASSERT_EQ (default_(1, none<int>()), 1);

ASSERT_EQ (default_(1, some(3)), 3);

auto h = [](int y){ return float (y * y); };

ASSERT_EQ (map_default (h, 0.0, none<int>()), 0.0);

ASSERT_EQ (map_default (h, 0.0, some (3)), 9.0);

}

namespace {

//safe "arithmetic"

auto add (int x) {

return [=](int y) {

if ((x > 0) && (y > INT_MAX - x) ||

(x < 0) && (y < INT_MIN - x)) {

return none<int>(); //overflow

}

return some (y + x);

};

}

auto sub (int x) {

return [=](int y) {

if ((x > 0) && (y < (INT_MIN + x)) ||

(x < 0) && (y > (INT_MAX + x))) {

return none<int>(); //overflow

}

return some (y - x);

};

}

auto mul (int x) {

return [=](int y) {

if (y > 0) { //y positive

if (x > 0) { //x positive

if (y > (INT_MAX / x)) {

return none<int>(); //overflow

}

}

else { //y positive, x nonpositive

if (x < (INT_MIN / y)) {

return none<int>(); //overflow

}

}

}

else { //y is nonpositive

if (x > 0) { // y is nonpositive, x is positive

if (y < (INT_MIN / x)) {

return none<int>();

}

}

else { //y, x nonpositive

if ((y != 0) && (x < (INT_MAX / y))) {

return none<int>(); //overflow

}

}

}

return some (y * x);

};

}

auto div (int x) {

return [=](int y) {

if (x == 0) {

return none<int>();//division by 0

}

if (y == INT_MIN && x == -1)

return none<int>(); //overflow

return some (y / x);

};

}

}//namespace<anonymous>

TEST(pgs, safe_arithmetic) {

//2 * (INT_MAX/2) + 1 (won't overflow since `INT_MAX` is odd and

//division will truncate)

ASSERT_EQ (get (unit (INT_MAX) * div (2) * mul (2) * add (1)), INT_MAX);

//2 * (INT_MAX/2 + 1) (overflow)

ASSERT_TRUE (is_none (unit (INT_MAX) * div (2) * add (1) * mul (2)));

//INT_MIN/(-1)

ASSERT_TRUE (is_none (unit (INT_MIN) * div (-1)));

}

by Shayne Fletcher (noreply@blogger.com) at November 30, 2015 09:50 PM

## 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

### @typeocaml

#### 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.

*k*is the number of possible candidates - e.g.,*k = 10*for [0, 10)*Ei*is the expected frequency for each candidate -*i = 1, 2, k**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:

- 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). - The bold headings of columns are the probabilities that the observations match the expectations.
- 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.

- We create a canvas.
- Each pixel on the canvas is a candidate random number that the generator can produce.
- We run the generator for lots of times.
- The more times a pixel gets hit, we draw a deeper color on it.
- 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.

## Preparation

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:

- Create a matrix array, with certain size (
*width*and*height*) - Manipulate the values (colors) of all slots via random generated numbers
- Convert the matrix bitmap to a real image
- 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
in
{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
int
n: the expected times of same number generated
int
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}
in
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);
done;
bitmap
```

## 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)
done
done;
img
```

## 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.

# JPG vs PNG

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:

## JPG

## PNG

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
```

and

```
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?

## 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 11, 2015

### Coq

#### Coq 8.5 beta 3 is out!

- 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).

### 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 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.

## 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/