# OCaml Weekly News

Hello

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

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

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

```module Simple =3D
struct
type term =3D
| Int of int
| App of term * term

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

```module Gadt =3D
struct
type _ term =3D
| 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 =3D fun i f -> function
| Int=
_ as t -> f i t
(*
^ Error: This pattern matches values o=
f type (int -> int -> int) term
but a pattern was expected which ma=
tches 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 poin= t of the `type a. ...` syntax was to allow the matched type to v= ary 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  =3D 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 =3D {apply : 'a=
. 'a -> 'a}

let example {apply<=
/span>} =3D apply "hello", apply 42<=
span style=3D"color: #ff4500;">;;

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

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

```type 'r visitor =3D {vis=
it : 'a. 'a term -> 'r -> 'r}

let rec fold : type a. 'r -> '=
r visitor -> a term -> 'r =3D
fun f t -> match t with
| Int=
_ as t -> f.visit i t
as t -> f.visit i t
| App=
(x,y) as t ->
let i =3D fold i f x in
let i =3D 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 -> &l=
t;v : 'b. r -> 'b term -> r> -> a term -> r =3D
fun i f -> function
| Int _ as t -> f#v i t
d
| App (x, y) as t -> f#v (fold (fold =
i f x) f y) t

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

let r =3D Gadt.fold 0 v (App=
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 =
=3D sig
type t
val term : t -> 'a term -> t
end

let rec fold : type a r. r -> =
(module Visito=
r with type t =
=3D r) -> a term
-> r =3D
fun i ((module Visit) as <=
span style=3D"color: #a0522d;">f) t<=
/span> -> match t with
| Int _ as t -> Visit.term i t
| Add as t -> Visit.term i t
| App (x,y) as t ->
let i =3D fold i f x in
let i =3D fold i f y in
Visit.term i t

let s =3D fold 0 (module struct
type t =3D int
let term x _ =3D 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 =3D 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 () =3D
let cache =3D ref None in
fun match cache.content=
s with
| None -> cache :=3D 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=
=3D fun f (x,y) -> f x, f y
```

as

```let x,y : string * int =3D 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 =3D { 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 =3D x
```

is perfectly fine, e.g.,

```let id1 =3D {f =3D good_=
id} (**)
let id2 =3D {f =3D bad_id}   (* rejected *)
```

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

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

with the message

```This field value has type 'b -> 'b which is less general than 'a. 'a -&g=
t; 'a
```

The same is true with modules,

```module type Id =3D sig
val f : 'a -> 'a
end
module Id1 : Id =3D struct let f =3D good_id end   (* accepted *)<=
/span>
module Id2 : Id =3D struct let f =3D bad_id () end (* rejected *)<=
/span>
module Id3 : Id =3D struct let f =3D 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 p= robably 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]` annotatio= n, or visitor will have the same representation as a function, e.g.,

```type 'r visitor =3D {vis=
it : 'a. 'r -> 'a term -> 'r} [@@unbo=
xed]
let count x =
_ =3D x + 1
let counter =3D {visit=3Dcount}
```

and

```# Core_kernel.=
phys_same count counter;;
- : bool =3D 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

### 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 tha= n 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.

`=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D` 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 -&= gt; 'a) -> 'a``` could be instantiated to 'a =3D '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 =3D {f1 : =
's. 's -> 'a}
type 'a rank2 =3D {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! 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 rece= nt 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: http= s://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=3Ddefault,beta=3Dgit= +https://github.com/ocaml/ocaml-beta-repository.git or opam switch create ocaml-variants.4.10.0+beta1= +<VARIANT> --repositories=3Ddefault,b= eta=3Dgit+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 ov= erlay which adds fixes to major packages for them to work with this beta: <= a href=3D"https://github.com/kit-ty-kate/opam-alpha-repository">https://git= hub.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-reposit= ory.git Obviously, this repository should not be used in production and probably co= ntains a few bugs, but at least it allows everyone to have almost as many p= ackages available as with OCaml 4.09. Only 60ish packages are still not ava= ilable, 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 OCam= l 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-re= pository (most of them have PRs associated already). I'm hopeful for them b= e 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: http= s://discuss.ocaml.org/t/job-data-engineer-positions-at-elastic-us-canada-we= stern-europe-proximate-to-na-timezones/4991/1 Hezekiah Carty announced Our team here at Elastic has positi= ons open for a few security data engineers (aka wranglers of data and all t= he 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://jo= bs.elastic.co/jobs/security-solutions/amer-distributed-/security-data-engin= eer/2005140#/ Senior security data engineer - https://jobs.elastic.co/jobs/security-solutions/amer-distributed-/secur= ity-senior-data-engineer/2005152#/ Language-wise, OCaml/Reason makes up most of the code you=E2=80=99ll be wor= king on. Python makes up most of the rest, in particular taking advantage o= f the machine learning and natural language processing goodies that ecosyst= em provides. Most of the tools and service we develop are internally focuse= d, supporting security research and improvements to security protections fo= r our users. For those so-inclined, there are lots of opportunities to pres= ent at and attend conferences, present work in blog posts, contribute to op= en 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=E2=80=99m available on = the OCaml or Reason Discord servers or by email at hezekiah.carty@elastic.c= o. 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/sha= wn-mcginty/naboris I could use input on the API and the documentation. Working on trying to i= mprove both at the moment. The goal was to create a very simple library for building RESTful type of w= eb servers. Make it very easy to manage h= andle request/response lifecycle and sessions. In my opinion this type of web server is a great entry point for new develo= pers looking to explore the OCaml/Reason world. Recently I have fallen in love with OCaml and Reason, and as a mostly web c= entered 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=E2=80=93OCaml/Reason more accessibl= e to web developers new to the ecosystem :-D I've been working on something= very similar: https://git= hub.com/yawaramin/re-web/ Ulrik Strid said There is also opium https://= github.com/rgrinberg/opium And morph https://gi= thub.com/reason-native-web/morph that has similar goals. It would be nice if we could either create a shared core that all could bui= ld 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 na= tive development with Reason/OCaml (and even C/C++). It provides per-projec= t build environments which are isolated from each other but share underlyin= g 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 bui= ld artifacts. For more info see a b= log post by @prometheansacrifice which highlights important updates in = 0.6.0. 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 loo= k at the archive or the RSS feed of the archives<= /a>. If you also wish to receive it every week by mail, you may subscribe online. Alan Schmitt ```
``` --=-=-=-- ```