OCaml Planet

August 20, 2015

OCaml Labs compiler hacking

Tenth OCaml compiler hacking evening and OCaml/ML talks

We'll be meeting in the Computer Lab next Friday (28th August 2015) for another evening of compiler hacking. All welcome!

We'll also be having an afternoon of OCaml- and ML-related talks beforehand, with titles suspiciously similar to talks at the ML Workshop and OCaml Workshop the following week.

If you're planning to come along to either the talks or to compiler hacking, please add yourself to the Doodle poll. Further updates, if any, will be posted to the compiler hacking mailing list.

Schedule

3.30pm Polymorphism, subtyping and type inference in MLsub
Stephen Dolan (with Alan Mycroft)

3.55pm The State of the OCaml Platform: September 2015
Anil Madhavapeddy (with Amir Chaudhry, Thomas Gazagnaire, Jeremy Yallop, David Sheets)

4.20pm Modular macros
Jeremy Yallop (with Leo White)

4.45pm Break

5.15pm Effective Concurrency through Algebraic Effects
KC Sivaramakrishnan (with Stephen Dolan, Leo White, Jeremy Yallop, Anil Madhavapeddy)

5.40pm A review of the growth of the OCaml community
Amir Chaudhry

6.05pm Persistent Networking with Irmin and MirageOS
Mindy Preston (with Magnus Skjegstad, Thomas Gazagnaire, Richard Mortier, Anil Madhavapeddy)

6.30pm Food

7.30pm Compiler hacking

Further details

Where: Room FW26, Computer Laboratory, Madingley Road

When: 3.30pm (workshop); 6.30pm (compiler hacking), Friday 28th August 2015

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.), ocamlbuild, the documentation, and the compiler itself. We'll have suggestions for mini-projects for various levels of experience (see also some things we've done on previous evenings), but feel free to come along and work on whatever you fancy.

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

August 19, 2015

Jane Street

No (functional) experience required

Jane Street is a serious functional programming shop. We use OCaml, a statically typed functional language for almost everything and have what is probably the largest OCaml codebase anywhere.

This leads lots of people to think that they shouldn't even bother applying, under the assumption that we are only interested in hiring deep functional programming gurus. I think people get to this conclusion in part because they think of functional languages, especially those with fancy type systems, as arcane tools that can only be used effectively after deep study.

To the contrary, one of the reasons we started building production systems with OCaml was that it was relatively easy to understand, even for people with no formal CS background. Since then, we've had good experiences taking students with no functional experience at all and getting them to the point of being able to complete a project in just a few weeks. We also have a very successful "OCaml Bootcamp" program, where over four weeks, we train all of the incoming traders and many other non-developer hires on OCaml and our development tools and libraries. By the end, most of them are able to create useful applications.

All of this is to say that we don't go out of our way to hire people who are already familiar with functional programming. In practice, it's just not that hard for strong programmers to pick it up after they start.

That said, a solid majority of the developers we hire do come in with functional programming experience --- but that's because of their preferences, not ours. Programmers with an interest in functional languages have an extra reason to want to work here, and so we get an unusually high number of good applicants from that pool.

There's a more general lesson here: using well-loved tools is a good way of attracting (and retaining) great developers.

by Yaron Minsky at August 19, 2015 10:22 PM

August 18, 2015

Functional Jobs

Haskell Engineer at Wagon (Full-time)

We’re a team of functional programmers writing apps and services in Haskell (and Javascript). Yes, it’s true: Haskell is our main backend language. We also use functional programming practices across our stack.

Wagon is a great place to do your best work. We love to teach and learn functional programming; our team is humble, hard working, and fun. We speak at the Bay Area Haskell Meetup, contribute to open source, and have weekly lunches with interesting people from the community.

Work on challenging engineering problems at Wagon. How to integrate Haskell with modern client- and server-side technologies, like Electron and Docker? How to deploy and manage distributed systems built with Haskell? Which pieces of our infrastructure should we open-source?

Learn more about our stack, how we combine Haskell, React, and Electron, and what it’s like working at a Haskell-powered startup.

Background

  • love of functional programming
  • personal project or production experience using Haskell, OCaml, Clojure, or Scala
  • passionate (but practical) about software architecture
  • interested in data processing, scaling, and performance challenges
  • experience with databases (optional)

Role

  • write Haskell for client- and server-side applications
  • integrate Haskell with modern tools like Docker, AWS, and Electron
  • architect Wagon to work with analytic databases like Redshift, BigQuery, Spark, etc
  • build systems and abstractions for streaming data processing and numeric computing
  • work with libraries like Conduit, Warp, and Aeson
  • use testing frameworks like QuickCheck and HSpec
  • develop deployment and monitoring tools for distributed Haskell systems

Get information on how to apply for this position.

August 18, 2015 09:38 PM

OCamlCore Forge Projects

stdint

stdint provides exact-width integer types and functions to work with them

August 18, 2015 07:19 AM

August 17, 2015

Dario Teixeira

Announcing Lambdoc 1.0-beta4

I'm happy to announce the release of version 1.0-beta4 of Lambdoc, a library providing support for semantically rich documents in web applications. Though Lambdoc was designed with Ocsigen/Eliom integration in mind, it does not actually depend on the Ocsigen server or Eliom, and you may use it with other frameworks. In fact, you may find it useful outside the web application domain altogether.

An overview of Lambdoc's features may be found in previous posts announcing the beta1 and beta3 releases. Between beta3 and beta4, the most salient changes are as follows:

  • Introduction of Lambdoc_core_foldmap, a module for aiding the construction of functions for deep traversal and transformation of a document tree. The basic idea is inspired by the compiler's Ast_mapper module, so it should be widely familiar. Moreover, the foldmapper is the result of a functor parameterised by a custom monad, so it's easily integrated in an application using Lwt or Async if the foldmapping requires doing monadic I/O. The tutorial directory includes some examples using Lambdoc_core_foldmap:

    • Tutorial 7 illustrates one of the simplest possible applications of this feature: a function that counts the number of bold sequences used in a document.
    • Tutorial 8 depicts a link validator that uses Cohttp to verify that all external links are live. Note that it registers itself as a parsing postprocessor, allowing any found errors to be reported together with other unrelated document errors. Moreover, it lives under the Lwt monad.
    • Tutorial 9 implements a simple document transformer which replaces all instances of Eastasia with Eurasia and vice-versa.
  • The addition of Lambdoc_core_foldmap enabled the simplification of the extension mechanism. Previous versions of Lambdoc feature hooks for reading/writing link and image URLs. All of those hooks are now gone.

  • Lambdoc documents may now carry information about the parsed source (location, etc) in every attribute. I briefly entertained the possibility of making the attribute polymorphic, thus allowing for document to carry custom meta-data. However, at this moment I have no practical need for this extra flexibility, and I am wary of increasing complexity in the name of hypothetical use cases.

Lambdoc 1.0-beta4 should be available in OPAM any moment now. Documentation is still a work in progress, and since OCamldoc gets terribly confused with Lambdoc's heavy use of module aliases, we may have to wait for Codoc before proper API docs can get generated. In a small effort to ameliorate this situation, the examples directory includes a tutorial with self-contained demos of Lambdoc's various features.

by Dario at August 17, 2015 06:28 PM

August 07, 2015

GaGallium

Merging OCaml patches

In Merging OCaml Patches I wrote a description of my personal process to merge OCaml patches (usually submitted as github pull requests) in the upstream repository (currently SVN). This description may be useful for external contributors to understand the process, and maybe meet me halfway by doing a bit of the work upfront.

In particular, as an external contributor, you

  • must add tests to the testsuite,
  • should write a proper changelog entry,
  • should rebase your PR into a good patch series when it converges, and
  • could include authorship information in commit messages.

I'm busy writing a thesis manuscript right now (gave up on the ICFP programming contest this year!), and limiting my OCaml-related work to the minimum: merging stuff on my free time. I think it has been a good deal so far. Thanks to all for the good work!

by Gabriel Scherer at August 07, 2015 08:00 AM

August 05, 2015

Andrej Bauer

Provably considered harmful

This is officially a rant and should be read as such.

Here is my pet peeve: theoretical computer scientists misuse the word “provably”. Stop it. Stop it!

Theoretical computer science is closer to mathematics than it is to computer science. There are definitions, theorems and proofs. Theoretical computer scientists must understand mathematical terminology. The words “proof” and “provable” are in the domain of mathematical logic. A statement is provable if it has a proof in a given formal system. It makes no sense to say “provable” without specifying or implying a specific proof system.

But theoretical computer scientists say things like (I just googled these randomly) “A Provably Optimal Algorithm for Crowdsourcing” and “A Provably Correct Learning Algorithm for Latent-Variable PCFGs” and even “provably true”.

So what is a “provably optimal algorithm” ? It is an algorithm for which there exists a proof of optimality. But why would you ever want to say that in the title of your paper? I can think of several reasons:

  1. You proved that there exists a proof of optimality but did not actually find the proof itself. This of course is highly unlikely,  but that does even not matter, for as soon as we know there exists a proof, the algorithm is optimal. Just say “optimal algorithm” and the world will be a more exact place.
  2. Your paper is an intricate piece of logic which analyzes existence of proofs of optimality in some super-important formal systems. This of course is not what theoretical computer scientists do for the most part. Any paper which actually did this, would instead say something like “$\mathrm{Ind}(\Sigma^0_1)$-provability of optimality”.
  3. You distinguish between algorithms which are optimal and those which are optimal and you proved they’re optimal. In that case we should turn tables: if you ever publish a claim of optimality without having proved it, put that in your title and call it “Unproved optimal algorithm”.
  4. You proved that your algorithm is optimal, showed the proof to the anonymous referee and the editor, and then published your optimal algorithm without proof. You want to tease your readers by telling them “there is a proof but it’s a secret”. If this is what you meant to convey, then the title was well chosen.

To see that “provable” is just a buzzword, consider what it would mean to have the opposite, that is an “unprovably optimal algorithm”. That is an algorithm which is optimal, but there exists no proof of optimality. Such a thing can be manufactured by a logician, probably, but is certainly not found in everyday life.

As someone is going to say that “provably true” makes sense, let me also comment on that. A statement is true if it is valid in all models. So “provably true” would mean something like “there exists a proof in a given formal system that the statement is valid in all models”. Well, I will not deny that a situation might arise in which this sort of thing is precisely what you would consider, but I will also bet you that it is far more likely that “provably true” should just be replaced by either “provable” or “true”, depending on the particularities of the situation.

As a rule of thumb, unless you are a logician, if you feel like using the word “provably”, just skip it.

And as long as I am ranting, please stop introducing every single concept with “informally” and prefixing every single displayed formula with “formally”. Which is it,

  1. you think that “informal” descriptions are somehow unworthy or broken, and you should therefore alert the reader that you’re lying to them, or
  2. you think that “formal” descriptions are an unnecessary burden which must be included in the paper to satisfy the gods of mathematics?

If the former, stop lying to your readers, and if the latter stop doing theoretical computer science.

Now I will go on to refereeing that pile of POPL papers which must contain at least a dozen misuses of “provably” and two dozen false formal/informal dichotomies.

by Andrej Bauer at August 05, 2015 06:19 PM

OCamlCore Forge News

Release of OCaml-bitcoin 2.0

This new release brings the API up-to-date with the latest versions of Bitcoin Core. It also features two new optional backends based on Cohttp and OCurl (contributed by Vincent Bernardoff). Finally, note that the code is now licensed under the LGPL 2.1 (W.O.L.E.).

by Dario Teixeira at August 05, 2015 10:20 AM