• en

# OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

948 blog posts are available. You can read the 30 more recent ones below or view older ones.

# C++ : Sums with constructors — Shayne Fletcher, Nov 28, 2015

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

# Eleventh OCaml compiler hacking evening at Pembroke College — OCaml Labs compiler hacking ( (OCaml Labs), Nov 24, 2015

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.

W…

# Visualise Randomness — Xinuo Chen, Nov 22, 2015

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, e…

# Forgive me Curry and Howard for I have Sinned. — Erik de Castro Lopo, Nov 16, 2015

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, w…

# Coq 8.5 beta 3 is out! — Coq, Nov 11, 2015

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 …

# Software Engineer - Functional Programmer - Erlang at Change Healthcare (Full-time) — Functional Jobs (FunctionalJobs.com), Nov 11, 2015

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 productio…

# Agda Writer — Andrej Bauer, Nov 07, 2015

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:

# Full Time: Software Developer (Functional Programming) at Jane Street in New York, NY; London, UK; Hong Kong — GitHub Jobs, Nov 05, 2015

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…

# CodeMesh 2015 — Amir Chaudhry, Nov 03, 2015

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 …

# On-the-fly lexer switching with Menhir — Dario Teixeira, Oct 29, 2015

Suppose you have a markup language that requires different lexers for different contexts (you have different verbatim environments, for instance). You can often solve this problem entirely within the lexer. This is the approach typically used for dealing with comments when parsing programming language source code, for example. What if, however, the markup language is complex enough that you need some help from the parser to know in which context you sit at any given moment, and therefore whi…

# SAT solving and HardCaml — Andy Ray, Oct 29, 2015

Combining a SAT solver with HardCaml to prove circuit equivalence.

# Profiling the stack — KC Sivaramakrishnan, Oct 27, 2015

In the last post, I described a flat allocation profiler for OCaml 4.02 bytecode interpreter. In this post, I'll describe further developments which add support for call stack information and better location information. Lets dive straight to the usage:

# Enabling stack profiling

Stack profiling is enabled by setting the environment variable CAML_PROFILE_STACK to the intended depth of stack. Suppose we would like to attribute any allocation to the current function, we would set CAML_PROFILE_…

# Quickcheck for Core — Jane Street (Carl Eastlund), Oct 26, 2015

Automated testing is a powerful tool for finding bugs and specifying correctness properties of code. Haskell's Quickcheck library is the most well-known automated testing library, based on over 15 years of research into how to write property-base tests, generate useful sources of inputs, and report manageable counterexamples. Jane Street's Core library has not had anything comparable up until now; version 113.00 of Core finally has a version of Quickcheck, integrating automated testing with our …

# Videos from around the world! — Open Mirage (Amir Chaudhry), Oct 23, 2015

Word about Unikernels and MirageOS is spreading and as the community grows, more people have been giving talks at user groups and conferences. Below are a selection of those that have been recorded, which alone is about 5 hours of content. The topics are wide ranging and include discussions about where unikernels fit in the ecosystem, all the way down to networking topics.

I hope you enjoy these and if you'd like to give a talk somewhere or share one of your videos, please do get in touc…

# Tooling is Awesome — Cedeela (simon), Oct 16, 2015

A quick note about my current OCaml setup, in my last project, Nunchaku.

## Oasis

First, I use Oasis to manage and build the project. It relies on OCamlbuild, but brings in several niceties:

• automatic generation of configure and Makefile files.
• it deals with sub-libraries, and the configure script can enable or disable the build of each sub-library.
• it builds and runs my tests. Yay!

## Merlin

Oh dear. Merlin has improved my workflow with OCaml so much that I can't imagine working without it now. …

# Getting Started Screencasts — Open Mirage (Amir Chaudhry), Oct 15, 2015

We put together some quick screencasts to make it easier for people to get started with MirageOS. They're all in a playlist below, which is around 10 minutes in total.

There are currently 4 videos which walk through some of the typical steps. The first three cover installation, building a 'hello world', and building a Xen unikernel on an Ubuntu machine. The fourth video gives an overview of the development workflows that are possible with OPAM and Git.

These should give everyone a clear i…

# OCaml Workshop and Strange Loop Talks — Mindy Preston, Oct 07, 2015

As a result of great encouragement from colleagues and friends, I gave a few talks in September.

Persistent Networking with Irmin and MirageOS, which I gave at the OCaml Workshop, is a talk on sticking a persistent database into various levels of the network stack. (It includes demonstrations from What a Distributed, Version-Controlled ARP Cache Gets You, as well as an Irmin-ified NAT device that I haven’t yet written up here.) The slides for my OCaml Workshop talk are also available.

Non-Impera…

# TodoMVC: a reactive version — Ocsigen blog (Stéphane Legrand), Oct 07, 2015

TodoMVC is a project which offers the same Todo application implemented using MV* concepts in most of the popular JavaScript MV* frameworks. One of the aims of TodoMVC is to enable a fair comparison between several frameworks, by providing implementations of the same application. A js_of_ocaml (JSOO) version is now available:

Our version is powered by the React module for functional reactive programming (FRP).

In this post, we outline the architecture of our implementat…

# List comprehensions in C++ via the list monad — Shayne Fletcher, Oct 04, 2015

As explained in Monads for functional programming by Philip Wadler, a monad is a triple $(t, unit, *)$. $t$ is a parametric type, $unit$ and $*$ are operations:

  val unit : α -> α t  val ( * ) : α t -> (α -> β t) -> β t
We can read expressions like

$m * \lambda\;a.n$

as, "perform computation $m$, bind $a$ to the resulting value, and then perform computation $n$". Referring to the signatures of $*$ and $unit$, in terms of types we see $m$ has the type &alpha…

# An Allocation Profiler for OCaml Bytecode Interpreter — KC Sivaramakrishnan, Sep 23, 2015

This post describes a simple flat allocation profiler for OCaml 4.02 bytecode interpreter.

OCaml is a strongly typed functional language with automatic memory management. Automatic memory management alleviates the need to manually deal with memory memory management, and by construction, avoids a large class of bugs. However, abstractions are not free in OCaml. Unlike MLton, a whole-program optimizing Standard ML compiler, which I used to hack on in an earlier life, in OCaml, one needs to be par…

# Governance of OCaml.org — Amir Chaudhry, Sep 18, 2015

For several months, I’ve been working with the maintainers of OCaml.org projects to define and document the governance structure around the domain name. I wrote about this previously and I’m pleased to say that the work for this phase has concluded, with the document now live.

## Recurring themes

There were some recurring themes that cropped up during my email discussions with people and I thought it would be useful to present a summary of them, along with my thoughts. Broadly, the discus…

View older blog posts.