OCaml Weekly News

I'm basically trying to do the equivalent of this simple fold function:

module Simple =
struct
  type term =
     | Int of int
     | Add
     | App of term * term

  let rec fold i f = function
    | Int _ as t -> f i t
    | Add -> f i Add
    | App (x, y) as t -> f (fold (fold i f x) f y) t
end

… but using a GADT:

module Gadt =
struct
  type _ term =
     | Int : int -> int term
     | Add : (int -> int -> int) term
     | App : ('b -> 'a) term * 'b term -> 'a term

  let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f -> function
    | Int _ as t -> f i t
    | Add -> f i Add
(*
     ^ Error: This pattern matches values of type (int -> int -> int) term
        but a pattern was expected which matches values of type int term
        Type int -> int -> int is not compatible with type int
*)
    | App (x, y) as t -> f (fold (fold i f x) f y) t
end

I've tried other variants of the syntax and got many encouragements but no green flag from the type-checker. Why is the compiler expecting an int term in there? I though the whole point of the type a. ... syntax was to allow the matched type to vary from one pattern to the next? Is there a way to do this?

It is the limitation of the let-bound polymorphism. A parameter of a function is monomorphic in its body. The classical example doesn't even reference any GADT,

let example f  = f "hello", f 42

It won't compile even though we can provide a polymorphic function that can applied both to integers and to strings, e.g., exampe (fun x -> x) should be possible, but not, because of the let-bounded polymorphism. There are a few solutions available in OCaml, the simplest is to use records, e.g.,

type app = {apply : 'a. 'a -> 'a}

let example {apply} = apply "hello", apply 42;;

val example : app -> string * int = <fun>

Now we have app that is polymorphic. In your case, I would define a visitor type, e.g.,

type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r}

let rec fold : type a. 'r -> 'r visitor -> a term -> 'r =
  fun i f t -> match t with
    | Int _ as t -> f.visit i t
    | Add as t -> f.visit i t
    | App (x,y) as t ->
        let i = fold i f x in
        let i = fold i f y in
        f.visit i t

Actually, this is a rare case where using a polymorphic method may be handy too:

let rec fold : type a r. r -> <v : 'b. r -> 'b term -> r> -> a term -> r =
     fun i f -> function
     | Int _ as t -> f#v i t
     | Add -> f#v i Add
     | App (x, y) as t -> f#v (fold (fold i f x) f y) t

let v =
   object method v : type a. _ -> a Gadt.term -> _ =
     fun x -> function
       | Int n -> x+n
       | Add -> x+1
       | App _ -> x+2
   end

let r = Gadt.fold 0 v (App (App (Add, Int 3), Int 5))

The point being that to match on a Gadt you will anyway need to use the (type a) construct to allow refinement.

So there is no lighter syntax to specify that f should accept any member of a GADT than the syntax to specify that f should accept any type at all?

Only three methods of introducing rank-2 polymorphism are known to me:

1. records
2. objects
3. first-class modules

Jacques has demonstrated the solution with objects, which might be a little bit more lightweight, at least as you don't need to define a new data type beforehand. But the invocation is more verbose and requires an annotation from the caller side, which could be confusing. The third solution relies on first-class modules and is even more verbose, at least on the definition side. Just for the sake of completeness,

  module type Visitor = sig
    type t
    val term : t -> 'a term -> t
  end

  let rec fold : type a r. r -> (module Visitor with type t = r) -> a term
-> r =
    fun i ((module Visit) as f) t -> match t with
      | Int _ as t -> Visit.term i t
      | Add as t -> Visit.term i t
      | App (x,y) as t ->
          let i = fold i f x in
          let i = fold i f y in
          Visit.term i t

  let s = fold 0 (module struct
      type t = int
      let term x _ = x + 1
    end)

And again, it is not about GADT. GADT act as a red herring here. As I've demonstrated earlier, using a simple pair will suffice to display the limitation of the prenex polymorphism. Even no ADT is required, just apply one term to another two and you will get them unified, e.g.,

let f g x y : unit = g x; g y

will have type

val f : ('a -> unit) -> 'a -> 'a -> unit

because 'a is quantified on the scope of f not g, in other words, it has type (not an OCaml syntax)

val f : forall 'a. ('a -> unit) -> 'a -> 'a -> unit

while we would like to have a type

val f : forall 'b, 'c. (forall 'a. 'a -> unit) -> 'b -> 'c -> unit

OCaml doesn't allow us to define types like ('a. 'a -> 'a) and the reason is not that it is hard to extend the parser it is…

I wonder, is this just a limitation of the OCaml parser or is there some deep reason for these work-around (like is the case, from my understanding, for the value restriction)?

Yep, good catch! It is because of the impurity. Indeed, Haskell has the Rank2Types extension that lets us write types like (forall a. a -> ()) -> b -> c -> (), with no extra syntactic burden (modulo having to provide the type annotation). But functions in Haskell are pure, therefore it is possible. To make the story short and obvious, let me do a simple demonstration of how things can go wrong in a language with side-effects. Let's go back to the simple example of pairs and the identity function. Consider the following nasty identity function,

let bad_id () =
  let cache = ref None in
  fun x -> match cache.contents with
    | None -> cache := Some x; x
    | Some cache -> cache

It has type unit -> 'a -> 'a therefore, if we would have the rank-1 polymorphism enabled for functions, we could apply it to the function

let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) -> f x, f y

as

let x,y : string * int = map2 (bad_id ()) "hello", 42

and will get a segmentation fault, as y will now have type int but hold a string.

And here comes the syntax as a savior as it lets us specify functions that are guaranteed to be syntactic values. Indeed, all three solutions syntactically guarantee that the provided argument is a function, not a closure. Indeed, let's introduce the universal identity via a record,

type id = { f : 'a. 'a -> 'a}

and we can see that our bad_id is not accepted due to the value restriction, while good_id, defined as,

let good_id x = x

is perfectly fine, e.g.,

let id1 = {f = good_id} (*accepted *)
let id2 = {f = bad_id}   (* rejected *)

moreover, even a fine, but not syntactic, identity is also rejected

let fine_id () x = x
let id3 = {f = fine_id ()} (* rejected *)

with the message

This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a

The same is true with modules,

module type Id = sig
  val f : 'a -> 'a
end
module Id1 : Id = struct let f = good_id end   (* accepted *)
module Id2 : Id = struct let f = bad_id () end (* rejected *)
module Id3 : Id = struct let f = fine_id () end (* rejected *)

and with objects (left as an exercise).

To summarize, in order to enable rank2 polymorphism we need a special kind of values to bear universal functions, as we can't rely on ordinary functions, which could be constructed using partial application. OCaml already had objects and records, which serve as a fine media for universally quantified functions. Later first class modules were introduced, which could also be used for the same purpose. Probably, one could devise a special syntax (or rely on the new attributes and extensions syntax, e.g., map2 [%rank2 : fun x -> x] ("hello",42) but probably this will lead to an unnecessary bloating of the language and the implementation, especially since we already have three solutions with a more or less tolerable syntax (and are in the base language, not an extension). Besides, if we will use the [@@unboxed] annotation, or visitor will have the same representation as a function, e.g.,

type 'r visitor = {visit : 'a. 'r -> 'a term -> 'r} [@@unboxed]
let count x _ = x + 1
let counter = {visit=count}

and

# Core_kernel.phys_same count counter;;
- : bool = true

Concerning rank-n polymorphism, in OCaml is is achieved using functors. Yes, they are a little bit syntactically heavy and force us to write signatures, but this is necessary anyway as rank-n is undecidable (non-inferrable). Finally, as a real-world example [1] of rank-2 polymorphism consider the universal WAVL tree that is a binary tree with each element having a different type (aka heterogeneous map). We use it in BAP as a backing store. You might find a few tricks there, especially using continuation-passing in the recursive cases.

Cheers, Ivan

[1]: https://github.com/BinaryAnalysisPlatform/bap/blob/b40689e636607b977758af048b79d65684ce48c3/lib/knowledge/bap_knowledge.ml#L847-L1693

Why is type checking creating a record different than type checking a function argument?

If we had the syntax (or something like it):

let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c)

Why would the type checker not be able to see that

map2 good_id ("hi", 42)

is valid but

map2 (fine_id ()) ("hi", 32)

is not, using the same logic that is verifying creating the "id" record is not valid?

I believe it is possible, as it is possible in Haskell (with RankNTypes and ScopedTypeVariables). The main (theoretical) difference is that in OCaml we need to check whether an expression is expansive and use a specialized generalization in case if it is (for the relaxed value restriction). It will, however, complicate the type inference engine a lot, but most importantly, changing the typing rule of functions will have a tremendous impact on the language. So this would be a very impractical solution. Especially, since we don't have the mechanism of language extensions, enabling RankNTypes will make a lot of programs untypeable, as they will now require type annotations (recall that RankN is undecidable in general). It could probably be implemented as a compiler command line parameter, like -rectypes but this will be still quite impractical since more often code like fun f -> f 1, f true is a programmer error, rather than a true request for universal polymorphism (the same as with rectypes, recursive types a more often an error rather than a deliberate attempt). Therefore, enabling RankN(^1) polymorphism will type too many programs (not that it is unsound, just many programs won't have sense) at the cost of even more obscure type errors. On the other hand, we have three syntactic constructs that let us express non-prenex polymorphism of the necessary rank(^2) without breaking anything else. So it looks like a good deal - we can have rankN polymorphism and decidable type checker at the same time. Just think of polymorphic records/methods as an embedded DSL for rankN polymorphism.

========== Footnotes:

1. An important point, that I forgot to notice, is that enabling scoped

type variables, will inevitably enable rankN polymorphism, e.g., since now any type could be a polytype, then suppose we have type 'a. ('b.'b -> 'a) -> 'a could be instantiated to 'a = 'd. ('c. -> 'd) -> 'd, so that our type is now 'd. ('b. 'b -> ('c. 'c -> 'd) -> 'd) -> ('c. 'c -> 'd) -> 'd which is now rank3. Therefore, enabling arbitrary quantification in the arrow type will lead to rankN and immediately make undecidable most of the type checker.

1. We can craft arbitrary rank using records with universally quantified

type variables, e.g., here is an example of rank3 polymorphism:

type 'a rank1 = {f1 : 's. 's -> 'a}
type 'a rank2 = {f2 : 'r. 'r -> 'a rank1}

Indeed, f2 has type 'a.('r. 'r -> ('s. 's -> 'a)

The opam cheat-sheet is now published in its final form.

You can get the colored and black-and-white versions from our website.

Happy hacking!

The release of OCaml 4.10.0 is approaching. We have published a first beta version to help you adapt your software to the new features ahead of the release.

During our preliminary tests for this new beta, we discovered that the recent work towards a multicore-ready OCaml runtime introduced compatibility issues within some opam packages, that were tweaking the runtime internals. Most of those opam packages have been fixed, or will be soon. Nevertheless, if you are affected by such compatibility issue, please speak up.

The source code is available at these addresses:

https://github.com/ocaml/ocaml/archive/4.10.0+beta1.tar.gz
https://caml.inria.fr/pub/distrib/ocaml-4.10/ocaml-4.10.0+beta1.tar.gz

The compiler can also be installed as an OPAM switch with one of the following commands.

opam switch create ocaml-variants.4.10.0+beta1 --repositories=default,beta=git+https://github.com/ocaml/ocaml-beta-repository.git

or

opam switch create ocaml-variants.4.10.0+beta1+<VARIANT> --repositories=default,beta=git+https://github.com/ocaml/ocaml-beta-repository.git

where you replace <VARIANT> with one of these:

• afl
• flambda
• fp
• fp+flambda

We want to know about all bugs. Please report them here:

https://github.com/ocaml/ocaml/issues

Happy hacking.

For the people wanting to give OCaml 4.10.0beta1 a shot, here is an opam overlay which adds fixes to major packages for them to work with this beta: https://github.com/kit-ty-kate/opam-alpha-repository

To use it, simple call:

$ opam switch 4.10
$ opam repository add alpha git://github.com/kit-ty-kate/opam-alpha-repository.git

Obviously, this repository should not be used in production and probably contains a few bugs, but at least it allows everyone to have almost as many packages available as with OCaml 4.09. Only 60ish packages are still not available, but apart from the notable exception of merlin all the essential packages and dependencies are there.

This work has been part of the release-readyness effort founded by the OCaml Software Foundation as announced here: https://discuss.ocaml.org/t/ann-the-ocaml-software-foundation/4476/13

The rest of the effort is going to be put towards having merlin available for OCaml 4.10 and upstreaming all the fixes from opam-alpha-repository (most of them have PRs associated already). I'm hopeful for them be all upstreamed and available before the stable release of OCaml 4.10.

Our team here at Elastic has positions open for a few security data engineers (aka wranglers of data and all the systems involved). We are a distributed company so you don't have to be close to an office to be considered. Infosec industry experience is not required, though of course welcome. We're surrounded by experts in the field so you'll have lots of opportunities to learn as you go!

The official postings are available here (both have the same text and only differ in title/seniority):

• Security data engineer - https://jobs.elastic.co/jobs/security-solutions/amer-distributed-/security-data-engineer/2005140#/
• Senior security data engineer - https://jobs.elastic.co/jobs/security-solutions/amer-distributed-/security-senior-data-engineer/2005152#/

Language-wise, OCaml/Reason makes up most of the code you’ll be working on. Python makes up most of the rest, in particular taking advantage of the machine learning and natural language processing goodies that ecosystem provides. Most of the tools and service we develop are internally focused, supporting security research and improvements to security protections for our users. For those so-inclined, there are lots of opportunities to present at and attend conferences, present work in blog posts, contribute to open source software projects and otherwise engage the community.

The positions are very similar to our last hiring announcement, though we had a different name at that point!

Please reach out to me if you have any questions. I’m available on the OCaml or Reason Discord servers or by email at hezekiah.carty@elastic.co.

https://github.com/shawn-mcginty/naboris

I could use input on the API and the documentation. Working on trying to improve both at the moment.

The goal was to create a very simple library for building RESTful type of web servers. Make it very easy to manage handle request/response lifecycle and sessions.

In my opinion this type of web server is a great entry point for new developers looking to explore the OCaml/Reason world.

Recently I have fallen in love with OCaml and Reason, and as a mostly web centered developer I've found this area quite lacking. I'm still new to the language and eco system so any guidance would be highly appreciated!

Wow! It seems we had much the same idea–OCaml/Reason more accessible to web developers new to the ecosystem :-D I've been working on something very similar: https://github.com/yawaramin/re-web/

There is also opium https://github.com/rgrinberg/opium

And morph https://github.com/reason-native-web/morph that has similar goals.

It would be nice if we could either create a shared core that all could build from or collaborate on one.

We've just released a new version of esy. You can install it with npm:

$ npm install -g esy@0.6.0

esy is a package.json driven workflow for native development with Reason/OCaml (and even C/C++). It provides per-project build environments which are isolated from each other but share underlying build caches so creating new environments is cheap.

While 0.6.0 is mainly about "quality-of-life" improvements it also got few new features including a basic support for garbage collection of unused build artifacts.

For more info see a blog post by @prometheansacrifice which highlights important updates in 0.6.0.