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

[Alan Schmitt <alan.schmitt@polytechnique.org>]

[-- 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 --]