Here is the latest OCaml Weekly News, for the week of July 29 to August 05, 2014.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-07/msg00185.htmloleg announced:
Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop Thursday September 4, 2014, Gothenburg, Sweden Call For Participation and Program http://okmij.org/ftp/ML/ML14.html Early registration deadline is August 3. Please register at https://regmaster4.com/2014conf/ICFP14/register.php The workshop is conducted in close cooperation with the OCaml Users and Developers Workshop http://ocaml.org/meetings/ocaml/2014/ taking place on September 5. *** Program with short summaries *** (The online version links to the full 2-page abstracts) * Welcome 09:00 * Session 1: Module Systems 09:10 - 10:00 1ML -- core and modules as one (Or: F-ing first-class modules) Andreas Rossberg We propose a redesign of ML in which modules are first-class values. Functions, functors, and even type constructors are one and the same construct. Likewise, no distinction is made between structures, records, or tuples, including tuples over types. Yet, 1ML does not depend on dependent types, and its type structure is expressible in terms of plain System F-omega, in a minor variation of our F-ing modules approach. Moreover, it supports (incomplete) Hindley/Milner-style type inference. Both is enabled by a simple universe distinction into small and large types. Type-level module aliases: independent and equal Jacques Garrigue; Leo White We promote the use of type-level module aliases, a trivial extension of the ML module system, which helps avoiding code dependencies, and provides an alternative to strengthening for type equalities. * Session 2: Beyond Hindley-Milner 10:30 - 11:20 The Rust Language and Type System (Demo) Felix Klock; Nicholas Matsakis Rust is a new programming language for developing reliable and efficient systems. It is designed to support concurrency and parallelism in building applications and libraries that take full advantage of modern hardware. Rust's static type system is safe and expressive and provides strong guarantees about isolation, concurrency, and memory safety. Rust also offers a clear performance model, making it easier to predict and reason about program efficiency. One important way it accomplishes this is by allowing fine-grained control over memory representations, with direct support for stack allocation and contiguous record storage. The language balances such controls with the absolute requirement for safety: Rust's type system and runtime guarantee the absence of data races, buffer overflows, stack overflows, and accesses to uninitialized or deallocated memory. In this demonstration, we will briefly review the language features that Rust leverages to accomplish the above goals, focusing in particular on Rust's advanced type system, and then show a collection of concrete examples of program subroutines that are efficient, easy for programmers to reason about, and maintain the above safety property. Doing web-based data analytics with F# (Informed Position) Tomas Petricek; Don Syme With type providers that integrate external data directly into the static type system, F# has become a fantastic language for doing data analysis. Rather than looking at F# features in isolation, this paper takes a holistic view and presents the F# approach through a case study of a simple web-based data analytics platform. * Session 3: Verification 11:40 - 12:30 Well-typed generic smart-fuzzing for APIs (Experience report) Thomas Braibant; Jonathan Protzenko; Gabriel Scherer In spite of recent advances in program certification, testing remains a widely-used component of the software development cycle. Various flavors of testing exist: popular ones include unit testing, which consists in manually crafting test cases for specific parts of the code base, as well as quickcheck-style testing, where instances of a type are automatically generated to serve as test inputs. These classical methods of testing can be thought of as internal testing: the test routines access the internal representation of the data structures to be checked. We propose a new method of external testing where the library only deals with a module interface. The data structures are exported as abstract types; the testing framework behaves like regular client code and combines functions exported by the module to build new elements of the various abstract types. Any counter-examples are then presented to the user. Furthermore, we demonstrate that this methodology applies to the smart-fuzzing of security APIs. Improving the CakeML Verified ML Compiler Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens The CakeML project comprises a mechanised semantics for a subset of Standard ML and a formally verified compiler. We will discuss our plans for improving and applying CakeML in four directions: optimisations, new primitives, a library, and verified applications. * Session 4: Implicits 14:00 - 14:50 Implicits in Practice (Demo) Nada Amin; Tiark Rompf Popularized by Scala, implicits are a versatile language feature that are receiving attention from the wider PL community. This demo will present common use cases and programming patterns with implicits in Scala. Modular implicits Leo White; Frédéric Bour We propose a system for ad-hoc polymorphism in OCaml based on using modules as type-directed implicit parameters. * Session 5: To the bare metal 15:10 - 16:00 Metaprogramming with ML modules in the MirageOS (Experience report) Anil Madhavapeddy; Thomas Gazagnaire; David Scott; Richard Mortier In this talk, we will go through how MirageOS lets the programmer build modular operating system components using a combination of functors and metaprogramming to ensure portability across both Unix and Xen, while preserving a usable developer workflow. Compiling SML# with LLVM: a Challenge of Implementing ML on a Common Compiler Infrastructure Katsuhiro Ueno; Atsushi Ohori We report on an LLVM backend of SML#. This development provides detailed accounts of implementing functional language functionalities in a common compiler infrastructure developed mainly for imperative languages. We also describe techniques to compile SML#'s elaborated features including separate compilation with polymorphism, and SML#'s unboxed data representation. * Session 6: No longer foreign 16:30 - 18:00 A Simple and Practical Linear Algebra Library Interface with Static Size Checking (Experience report) Akinori Abe; Eijiro Sumii While advanced type systems--specifically, dependent types on natural numbers--can statically ensure consistency among the sizes of collections such as lists and arrays, such type systems generally require non-trivial changes to existing languages and application programs, or tricky type-level programming. We have developed a linear algebra library interface that guarantees consistency (with respect to dimensions) of matrix (and vector) operations by using generative phantom types as fresh identifiers for statically checking the equality of sizes (i.e., dimensions). This interface has three attractive features in particular. (i) It can be implemented only using fairly standard ML types and its module system. Indeed, we implemented the interface in OCaml (without significant extensions like GADTs) as a wrapper for an existing library. (ii) For most high-level operations on matrices (e.g., addition and multiplication), the consistency of sizes is verified statically. (Certain low-level operations, like accesses to elements by indices, need dynamic checks.) (iii) Application programs in a traditional linear algebra library can be easily migrated to our interface. Most of the required changes can be made mechanically. To evaluate the usability of our interface, we ported to it a practical machine learning library (OCaml-GPR) from an existing linear algebra library (Lacaml), thereby ensuring the consistency of sizes. SML3d: 3D Graphics for Standard ML (Demo) John Reppy The SML3d system is a collection of libraries designed to support real-time 3D graphics programming in Standard ML (SML). This paper gives an overview of the system and briefly highlights some of the more interesting aspects of its design and implementation. * Poster presentation, at the joint poster session with the OCaml workshop Nullable Type Inference Michel Mauny; Benoit Vaugon We present a type system for nullable types in an ML-like programming language. We start with a simple system, presented as an algorithm, whose interest is to introduce the formalism that we use. We then extend it as system using subtyping constraints, that accepts more programs. We state the usual properties for both systems. This is work in progress. Program Committee Kenichi Asai Ochanomizu University, Japan Matthew Fluet Rochester Institute of Technology, USA Jacques Garrigue Nagoya University, Japan Dave Herman Mozilla, USA Stefan Holdermans Vector Fabrics, Netherlands Oleg Kiselyov (Chair) University of Tsukuba, Japan Keiko Nakata Tallinn University of Technology, Estonia Didier Remy INRIA Paris-Rocquencourt, France Zhong Shao Yale University, USA Hongwei Xi Boston University, USA
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-07/msg00191.htmlJeremie Dimino announced:
I am pleased to announce the 111.25.00 release of the Core suite. With this release all packages are now compatible with OCaml 4.02. The following packages were upgraded: - async_extra - async_kernel - async - async_parallel - async_unix - core_extended - core_kernel - core - custom_printf - jenga - ocaml_plugin - patdiff - patience_diff - sexplib - textutils Files and documentation for this release are available on our website and all packages are in opam: https://ocaml.janestreet.com/ocaml-core/111.25.00/individual/ https://ocaml.janestreet.com/ocaml-core/111.25.00/doc/ Here is list of changes for this version: ## 111.25.00 ### async - add a dns example ### async_extra - Removed `lazy` from the core of `Log`. - Made `Log.Message.t` have a stable `bin_io`. The `Stable.V1` is the current serialization scheme, and `Stable.V0` is the serialization scheme in 111.18.00 and before, which is needed to talk to older systems. - Changed `Rpc` to return `Connection_closed` if a connection ends before a response makes it to the caller. Previously, the dispatch output was never determined. Also, removed an unused field in one of the internal data structures of Async RPC. - In `Versioned_rpc`, added `version:int` argument to `implement_multi ` functions. - In `Versioned_rpc`, the `Pipe_rpc.Make` functors now return an additional output functor. `Register'` is like `Register` but has in its input module: ```ocaml val response_of_model : Model.response Queue.t -> response Queue.t Deferred.t ``` rather than ```ocaml val response_of_model : Model.response -> response ``` This is analogous to `Pipe.map'` and `Pipe.map`. - Added to `Log` a `V2` stable format and better readers for time-varying formats. - In `Log`, added an optional `?time:Time.t` argument to allow callers to pass in the logged time of an event rather than relying on `Time.now ()`. ### async_kernel - Fixed `Clock.run_at_intervals` to make the initial callback at an interval multiple. Previously, if `start` was in the past, `f` would run immediately rather than waiting for an interval of the form `start + i * span`. Now it always waits for an interval, even the first time it runs. ### async_parallel - improve error handling ### async_unix - Added `Unix.Addr_info` and `Name_info`, which wrap `getaddrinfo` and `getnameinfo`. - Improved the scheduler's error message when the thread pool is stuck. ### core - Added `Gc.disable_compaction` function. - Added `Time.to_string_abs_trimmed`, which prints a trimmed time and takes a `zone` argument. - Fixed `unix_stubs.c` to suppress a warning when building with some versions of gcc. - Changed `Time.Zone` to allow the zoneinfo location to be specified by an environment variable. Closes #40 - Fix compatibility with 4.02 ### core_extended - Moved `Quickcheck` from `core`. - Added [Int.gcd]. ### core_kernel - Fix build on FreeBSD Closes #10 - Added functions to `Container` interface: `sum`, `min_elt`, `max_elt`. ```ocaml (** Returns the sum of [f i] for i in the container *) val sum : (module Commutative_group.S with type t = 'sum) -> t -> f:(elt -> 'sum) -> 'sum (** Returns a min (resp max) element from the collection using the provided [cmp] function. In case of a tie, the first element encountered while traversing the collection is returned. The implementation uses [fold] so it has the same complexity as [fold]. Returns [None] iff the collection is empty. *) val min_elt : t -> cmp:(elt -> elt -> int) -> elt option val max_elt : t -> cmp:(elt -> elt -> int) -> elt option ``` - Made `Core_hashtbl_intf` more flexible. For instance supports modules that require typereps to be passed when creating a table. Address the following issues: The type `('a, 'b, 'z) create_options` needs to be consistently used so that `b` corresponds with the type of data values in the returned hash table. The type argument was wrong in several cases. Added the type `('a, 'z) map_options` to `Accessors` so that map-like functions -- those that output hash tables of a different type than they input -- can allow additional arguments. - Fixed a bug in `Dequeue`'s `bin_prot` implementation that caused it to raise when deserializing an empty dequeue. - Made `Container.Make`'s interface match `Monad.Make`. - Deprecated infix `or` in favor of `||`. - Simplified the interface of `Arg` (which was already deprecated in favor of `Command`). - Replaced `Bag.fold_elt` with `Bag.filter`. - `Memo.general` now raises on non-positive `cache_size_bound`. - Removed `Option.apply`. - Removed `Result.call`, `Result.apply`. - Moved `Quichcheck` to `core_extended`. It should not be used in new code. ### custom_printf - Fix 4.02 compatibility. ### jenga - Switched to un-version-numbered API. - Renamed `Tenacious_sample_lib.Tenacious` to `Tenacious_sample_lib.Tenacious_sample` to avoid conflicts in the public release. - Write `buildable_targets.list` (on alias `.info`). ### ocaml_plugin - ignore more warnings by default ### patdiff - add a `?file_names` argument to `Compare_core.diff_strings` ### patience_diff - refactoring and more unit tests ### sexplib - Fix compatibility with OCaml 4.02
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-08/msg00001.htmlGerd Stolpmann announced:
This version includes a few fixes concerning the -ppx option (e.g. support it in the toploop). More documentation and download: http://projects.camlcity.org/projects/findlib.html
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-08/msg00011.htmlRichard Jones announced:
Just a friendly note for anyone who is trying to build OCaml or OCaml packages for any or all of the following: - OCaml 4.02 - i686 - x86-64 - arm64 - ppc64le I have been fixing many issues in the Fedora packages. You can look at the patches or build changes I have needed to apply in Fedora by going to: http://pkgs.fedoraproject.org/cgit/ and using the search box in the top right corner to search for the package name (eg: ocaml-mikmatch : http://pkgs.fedoraproject.org/cgit/ocaml-mikmatch.git/ ) Then look for the "master" branch, click "tree", and you will see the build recipe we use (*.spec file) and the patches we apply. Patches which are relevant for upstream are usually sent upstream, *if* I can easily find someone who will receive them (especially without too much hassle, such as requiring sign-ups).
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-08/msg00012.htmlA long time ago, Xavier Leroy said ... Diego Olivier Fernandez Pons recently replied:
> At the time Set was written, no efficient algorithms for whole-set > > operations (union, intersection, difference, etc) were known for > red-black trees. I'm not sure they are known today. The answer is no and I will try to explain. When doing a set union, at some point you will have to merge two disjoint sets represented each by a tree [1 .. 10] union [15 .. 22] At that point you need to know the "size" of each tree because if both trees are the same size you just need to append them return Node ([1..10], [15..22]) while if one tree is bigger than the other, you will need to cut that tree into smaller pieces and reorganize them (a "rotation"). divide [1..10] into [1..5], [6..10] return Node([1..5], Node ([6..10], [15..22])) The AVL implementation of OCaml gives you the "size" of each tree, its the extra int in the constructor 'a tree = Empty | Node 'a tree * 'a * 'a tree * int <--- here it is equal to the longest path in the tree f = function E -> 0 | Node (l, _, r, h) -> 1 + max (f l, fr) If you implement Weight-balanced trees, that value is the cardinal of the set represented by the tree. If you use red-black or "traditional AVL" representation, that extra bit just tells you if the tree is leaning towards the left or towards the right, but doesn't tell you any information about the global "size" of the tree. Which means you cannot implement set union directly. You have to traverse full tree in O(n) to recompute that information. There is at least one library in Haskell that implements AVL trees that way, it uses -1 | 0 | 1 information for most operations and recomputes the longest path for all trees when doing set operations, then discards that info. There is also a way to implement red black trees to do set operations just like (non-traditional) AVLs. It is described in Olivié H.J A new class of balanced search trees : half balanced search trees, RAIRO Informatique Théorique 16, 51 71 - also in his PhD Thesis. Basically a tree is red-black when shortest-branch * 2 >= longest-branch (cf. Constructing Red-Black trees, Ralf Hinze 1999 - easier to find than Olivié's works) So you can implement a tree structure that memorizes both the shortest and the longest branch in each node 'a tree = E | N of 'a tree * 'a * 'a tree * int * int <---- shortest and longest From there you just follow the same scheme than the AVL implementation in the OCaml lib, you just need to cope with a couple of triple rotation cases. > As for performance of insert/lookup operations, Jean-Christophe > Filliâtre has measurements showing that OCaml's 2-imbalance AVL > trees perform better than red-black trees. It all depends on your ratio > of insertions to lookups, of course. But the 2-imbalance trick makes > a big difference with textbook AVL trees. This is a bit more difficult but in short "red-black trees do not implement truly red-black trees" and "all implementations of red-black trees implement a different approximation of red-black trees". Any implementation of red-black trees that uses the 1 bit trick and where insertions are in log (n) is not surjective. You can understand that as meaning (1) - some red-black trees will never be built by the balancing algorithm (2) - sometimes you will give the balancing algorithm a red-black tree (= has a provable red-black coloring) and it will still rebalance it instead of noticing it's already balanced and returning it untouched. The reason is insertion in red-black trees using the 1 bit trick is linear. Meaning if I want a balancing algorithm that never falls into (1) or (2) I cannot avoid linear time insertion. The result is all algorithms found in the literature are log(n) approximations of the full algorithm. The only algorithm that is truly logarithmic is again Olivié's thanks to it's implicit representation of the red-black coloring. From there, comparing performance of AVLs with "red-black trees" in general makes no sense as the person that implemented them may have implemented any arbitrary approximation of the full algorithm. This translates in the code as a random number of "cases" to check for balancing : 4 for Okasaki, 27 in the CLR, etc. With double, triple, quadruple rotations, according to how "deep" the author was willing to go. Because what these guys are doing is "unfolding" the linear behavior of the algorithm into a constant and falling back into rebuilding any tree they are given for all other cases. In any case, some benchmarks I did very, very, very longtime ago showed AVL and Weight balanced are good all-purpose implementations. The advantage of WB being it gives you the cardinality of the set in O (1). In some sense, AVL is the log of WB (in the same way the height of a tree is the log of its size).
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-08/msg00014.htmlSylvain Le Gall announced:
ocaml-gettext provides support for internationalization of OCaml program. It uses the gettext convention and file format through a pure OCaml implementation or a C library binding. This release fixes a problem with OCaml 4.02. Thanks to Richar W. M. Jones for the patch. You can download it here: https://forge.ocamlcore.org/frs/download.php/1433/ocaml-gettext-0.3.5.tar.gz
Thanks to Alp Mestan, we now include in the OCaml Weekly News the links to the recent posts from the ocamlcore planet blog at <http://planet.ocaml.org/>. The ML Workshop looks fantastic: https://blogs.janestreet.com/the-ml-workshop-looks-fantastic/?utm_source=rss&utm_medium=rss&utm_campaign=the-ml-workshop-looks-fantastic Software Engineer (OCaml) at Cryptosense (Full-time): http://functionaljobs.com/jobs/8730-software-engineer-ocaml-at-cryptosense Generalist Engineer at Esper (Full-time): http://functionaljobs.com/jobs/8728-generalist-engineer-at-esper
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.