[Caml-list] Attn: Development Editor, Latest OCaml Weekly News

Alan Schmitt
2020-01-14T14:17:06Z

[-- Attachment #1: Type: text/plain, Size: 24944 bytes --]

Hello

Here is the latest OCaml Weekly News, for the week of January 07 to 14,
2020.

Table of Contents
─────────────────

Calling a single function on every member of a GADT?
OCamlPro's opam cheat sheet, with a new theme!
OCaml 4.10.0, first beta
Data engineer positions at Elastic, US/Canada/Western Europe (proximate to NA timezones)
Release of naboris 0.1.0 a simple http server
esy@0.6.0 release
Old CWN

Calling a single function on every member of a GADT?
════════════════════════════════════════════════════

Archive:
<https://sympa.inria.fr/sympa/arc/caml-list/2020-01/msg00007.html>

Ivan Gotovchits asked
─────────────────────

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?

Ivan Gotovchits replied
───────────────────────

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
└────

Jacques Garrigue also replied
─────────────────────────────

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.

rixed asked and Ivan Gotovchits replied
───────────────────────────────────────

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>

Malcolm Matalka asked and Ivan Gotovchits replied
─────────────────────────────────────────────────

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

OCamlPro's opam cheat sheet, with a new theme!
══════════════════════════════════════════════

Archive:
<https://discuss.ocaml.org/t/rfc-ocamlpros-opam-cheat-sheet-with-a-new-theme/4689/3>

Thomas Blanc announced
──────────────────────

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!

[colored]
<http://www.ocamlpro.com/wp-content/uploads/2019/11/ocaml-opam.pdf>

[black-and-white]
<http://www.ocamlpro.com/wp-content/uploads/2020/01/ocaml-opam-bw.pdf>

OCaml 4.10.0, first beta
════════════════════════

Archive: <https://discuss.ocaml.org/t/ocaml-4-10-0-first-beta/4989/1>

octachron announced
───────────────────

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.

Kate added
──────────

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.

Data engineer positions at Elastic, US/Canada/Western Europe (proximate to NA timezones)
════════════════════════════════════════════════════════════════════════════════════════

Archive:
<https://discuss.ocaml.org/t/job-data-engineer-positions-at-elastic-us-canada-western-europe-proximate-to-na-timezones/4991/1>

Hezekiah Carty announced
────────────────────────

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.

[Elastic] <https://www.elastic.co/>

[last hiring announcement]
<https://discuss.ocaml.org/t/filled-posting-is-no-longer-open-threat-research-engineer-job-endgame-us/1937>

Release of naboris 0.1.0 a simple http server
═════════════════════════════════════════════

Archive:
<https://discuss.ocaml.org/t/release-of-naboris-0-1-0-a-simple-http-server/4994/1>

Shawn McGinty announced
───────────────────────

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

Yawar Amin replied
──────────────────

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

Ulrik Strid said
────────────────

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.

esy@0.6.0 release
═════════════════

Archive: <https://discuss.ocaml.org/t/ann-esy-0-6-0-release/5010/1>

Andrey Popp announced
─────────────────────

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.

[esy] <https://esy.sh>

[blog post] <https://esy.sh/blog/2020/01/12/0.6.0.html>

Old CWN
═══════

If you happen to miss a CWN, you can [send me a message] and I'll mail
it to you, or go take a look at [the archive] or the [RSS feed of the
archives].

If you also wish to receive it every week by mail, you may subscribe
[online].

[Alan Schmitt]

[send me a message] <mailto:alan.schmitt@polytechnique.org>

[the archive] <http://alan.petitepomme.net/cwn/>

[RSS feed of the archives] <http://alan.petitepomme.net/cwn/cwn.rss>

[online] <http://lists.idyll.org/listinfo/caml-news-weekly/>

[Alan Schmitt] <http://alan.petitepomme.net/>

[-- Attachment #2: Type: text/html, Size: 53238 bytes --]