Hello
Here is the latest OCaml Weekly News, for the week of July 21 to 28, 2015.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-07/msg00090.html
Roberto Di Cosmo announced:We are very pleased to announce the massive, open, online course Introduction to Functional Programming in OCaml the first MOOC entirely devoted to our beloved OCaml programming language. All the information on the course, including a teaser video, is available at https://www.france-universite-numerique-mooc.fr/courses/parisdiderot/56002/session01/about The course is in english, starts from the basics, and goes on for seven weeks up to the module system. An interactive exercise environment will allow to do the exercises in the browser, with an online evaluation integrated in the learning system; as you expect, this is based on tryocaml and js_of_ocaml, and is a unique distinguishing feature of this MOOC. The learning platform happens to be called FUN (yes, great to have fun with functional programming :-)), that is a variant of Open EdX run by the french ministry of education. The registration is open, and the course will start on October 19th. We finally have a MOOC on OCaml, a great tool to bring functional programming and our preferred programming language to a wide audience: now, let's tell the world! Use your social networks, mailing lists, professional and non professional conferences to spread the world. And see you soon for our first course :-) -- Roberto Di Cosmo, Yann Regis-Gianas and Ralf Treinen
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-07/msg00099.html
Sébastien Hinderer asked and Xavier Leroy replied:> What's the most efficient way to compare floats, please? > Is it the polymorphic compare function, or is there a more specialized > version of it? You'll get good performance by type-specializing Pervasives.compare: let compare_float (x: float) (y: float) = compare x y If you're absolutely sure your floats are not NaN, you can shave a few CPU cycles: let compare_float (x: float) (y: float) = if x < y then -1 else if x > y then 1 else 0Boris Yakobowski then said:
I feel obligated to point out that the _semantics_ of floating-point comparison is a bit tricky. IEEE 754 mandates that NaN == NaN should return false (as well as NaN != NaN), breaking all algebraic laws known to mankind : -). OCaml's operators '=' and '!=' follow this convention, but 'compare nan nan' returns 0, which is usually the desired behavior. However, 'compare 0. (-0.)' also returns 0, while you might want to distinguish those two values.Jacques-Henri Jourdan then said and Boris Yakobowski replied:
> Beaware: > > Nan <> Nan -> true > Nan = Nan -> false > Nan != Nan and Nan == Nan : depends on the memory layout. Indeed, thanks for the clarification... I got confused when negating OCaml's '=' operator (a dangerous side-effect of writing too much C!), hence the erroneous '!=' instead of <>. Regarding, 'nan <> nan', I had convinced myself that all comparisons with NaN returned false. I wonder why <>/!= got a special treatment since e.g. 'nan < 1.' and '1. < nan' both return false.Xavier Leroy finally said:
Perhaps so that (using Caml syntax) "x <> y" is always equivalent to "not (x = y)". But I agree it can be viewed as yet another oddity with NaNs. Just to clarify my previous post: let compare_float (x: float) (y: float) = compare x y gives a total order over floats that behaves sensibly, if somewhat arbitrarily, over NaN arguments: two NaNs are equal, and any NaN is less than any non-NaN float. In contrast, let compare_float (x: float) (y: float) = if x < y then -1 else if x > y then 1 else 0 is not a proper order, because the implied equality is not transitive. Consider: compare_float 0.0 nan = 0 compare_float nan 1.0 = 0 compare_float 0.0 1.0 = -1 So, don't use the latter definition for e.g. sorting a list of floats that can contain NaN. The former definition is more robust.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-07/msg00109.html
Markus Weißmann asked:I'm trying to do something clever regarding the interface for a communication library: There is a server and a client which can only send "client" (client to server) and "server" (server to client) messages. The current idea is to use a phantom type to annotate the socket as either being "client to server" or "server to client"; type client type server type ('a, 'b) socket type 'a message I've got a bunch of functions that only work on either "client messages", "server messages" or some on both. Something like: val p1 : 'a message -> int val p2 : server message -> float val p3 : client message -> char You can only send "client messages" on the "client socket" and "server messages" on the "server socket". val send : ('a, _) socket -> 'a message -> unit You can get these messages only on the respective other side. val recv : (_, 'b) socket -> 'b message but is there some clever way to only have the socket annotated with one type while keeping only one send and one recv function? Something in the spirit of this: type 'a socket val send : 'a socket -> 'a message -> unit val recv : [server socket -> client message | client socket -> server message] there is no "(client, client) socket" or "(server, server) socket"; regards -Markus PS: Under the hood its basically type 'a message = bytes type ('a, 'b) socket = mysocket But the underlying system allows me to add filters that guarantee me the aforementioned properties of send/receive.Nicolas Ojeda Bar suggested:
This is not exactly what you asked, but you can use GADTs to constrain the phantom type (_, _) socket: type client type server type (_, _) socket = | ClientServer : mysocket -> (client, server) socket | ServerClient : mysocket -> (server, client) socketMikhail Mandrykin also suggested:
The closest solution I can suggest is with a recv signature val recv : ('a, 'b) recv_t -> 'a socket -> 'b message (one extra argument while socket is annotated with only one type and there's only one send and recv function). This uses GADTs: type 'a socket = | Client_socket : ... -> client socket | Server_socket : ... -> server socket type 'a message = | Client_message : ... -> client message | Server_message : ... -> server message let send = ... type (_, _) recv_t = | From_client : (server, client) recv_t | From_server : (client, server) recv_t let recv : type a b. (a, b) recv_t -> a socket -> b message = function | From_client -> fun Server_socket -> ... Client_message (...) | From_server -> fun Client_socket -> ... Server_message (...) The "[server socket -> client message | client socket -> server message] " (without an extra argument) looks like a dependent type (in spirit of " 'a socket -> (reverse 'a) message"), which makes me doubt about whether it's possible in OCaml.octachron also suggested:
I see one way to do this, but I am not sure I would call it a clever way. The idea is to try to encode (-1),(1) and (~-) at the type level. With this encoding, it is possible to define send and recv as type 'a socket val send : 'n socket -> 'n message -> unit val recv : 'n socket -> '-n message A working encoding would be: type head type tail type 'a socket = ... (constraint 'a = 'b * 'c) type 'a message = ... (constraint 'a = 'b * 'c) where you can use either gadt or abstract value to enforce that 'a is only head*tail ( = 1 ) or tail*head ( = -1 ). Then -( 'a * 'b ) can be translated to ('b *' a), i.e. val send : 'n socket -> 'n message -> unit val recv: ('a * 'b) socket -> ('b * 'a) message With this encoding, you only need to decompose the type parameter of socket or message when you need to flip it. However, I am not sure that this slim advantage is worth the added complexity (and one could argue that I added a type parameter to message rather than removed one from socket).Jeremy Yallop also suggested:
> but is there some clever way to only have the socket annotated with one type > while keeping only one send and one recv function? One way to achieve this is to add some structure to the 'server' and 'client' types, by turning your descriptions of the desired behaviour into code. For example, you say > There is a server and a client which can only send "client" (client to > server) and "server" (server to client) messages. which you might encode as follows: type server = < src: server; dst: client; name: [`server] > and client = < src: client; dst: server; name: [`client] > These are object types, but there's no need to actually use object values in your code. The object type syntax is simply a convenient way to label the different components of the type so that they can be retrieved later. Once you have these types you might write type-level functions to retrieve the components. Here's a function that retrieves the 'src' component: type 'a src = 's constraint 'a = < src: 's; .. > This can be read as follows: src is a function that maps 'a to 's, where 'a is an object type with a src key, and 's is the value of that key. Similarly, here's a function to retrieve the 'dst' component: type 'a dst = 'd constraint 'a = < dst: 'd; .. > > You can only send "client messages" on the "client socket" and "server > messages" on the "server socket". > > val send : ('a, _) socket -> 'a message -> unit > > You can get these messages only on the respective other side. > > val recv : (_, 'b) socket -> 'b message > > Something in the spirit of this: > > type 'a socket > val send : 'a socket -> 'a message -> unit > val recv : [server socket -> client message | client socket -> server > message] You might then write val send : 's socket -> 's src message -> unit val recv : 's socket -> 's dst message and OCaml will enforce the constraints you describe.Török Edwin then asked:
This is very useful to know, thanks! It'd be interesting to know how you come up with these solutions :) They are easy to understand as you've explained, but I wouldn't have thought of this solution although I guessed there had to be a solution with objects (after reading [1]), and I understand (simple) phantom types and (mostly) understand object types and GADTs by now. Is there some (fundamental) knowledge I'm missing that would allow me to construct solutions to problems like these (if so could you point to some papers, lecture notes or books please), or is it just that I very rarely use objects/GADTs and lack the experience? Best regards, --Edwin [1] http://stackoverflow.com/questions/10779283/when-should-objects-be-used-in-ocaml/10780681#10780681Oleg then replied and mandrykin added:
> This is probably a folklore, but it was mentioned on this list more than > a decade ago by Jacques Garrigue. We have used this trick extensively > in > > http://okmij.org/ftp/meta-programming/HPC.html#GE-generation > > (see the description on p11 of the SCP-metamonads.pdf paper, and many > applications starting from p21) For me actually knowing the trick used in the paper alone was not enough to quickly come up with this solution. I had already used this object constraints several times in even in real-life code, but that didn't help much(. To me the key idea here (in the Jeremy Yallop's solution) is the ability to express the "negation" function on type level with a pair of mutually-recursive types and a constraint. This can actually be also done with polymorphic variants instead of object types: type client = [`cs of server * [`client]] and server = [`cs of client * [`server]] type 'a rev = 'b constraint 'a = [`cs of 'b * _] (* rev is the function *) This ensures the relations client rev = server, server rev = client and client <> server. This approach seems powerful enough to express any finite permutation group, e.g. for 2 elements: type z = [`t of [`e1] * [`e2] * z] (* initial permutation *) type 'e e1 = [`t of 'e1 * 'e2 * 'e e1] (* neutral permutation *) constraint 'e = [`t of 'e1 * 'e2 * _ ] and 'e e2 = [`t of 'e2 * 'e1 * 'e e2] (* reverse permutation *) constraint 'e = [`t of 'e1 * 'e2 * _] type 'a inv = 'b constraint 'a = [`t of _ * _ * 'b] Here "-e1 - e2 - e3 - ... - en + e1' + e2' + ... + em'" (using `+' for the group operation and `-' for the inverse) can be encoded as "z e1 e2 ... en inv e1' e2' ... em'". By Cayley's theorem (states that every finite group G is isomorphic to a subgroup of the symmetric group acting on G) this means (if I got it right) that in fact any finite group operation (and the corresponding inverse) is encodiable in OCaml as type-level function!
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-07/msg00122.html
Jeremy Yallop announced:Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop Thursday 3 September 2015, Vancouver, Canada (co-located with ICFP) Call For Participation: http://www.mlworkshop.org/ml2015/ Early registration deadline: Monday 3 August 2015 Register online: https://regmaster4.com/2015conf/ICFP15/register.php The ML Family Workshop brings together researchers, implementors and users of languages in the extended ML family and provides a forum to present and discuss common issues, both practical (compilation techniques, tooling, embedded programming) and theoretical (fancy types, module systems, type inference). ML 2015 will be held in Vancouver on 3 September, immediately after ICFP and close to a number of other related events, including the OCaml Workshop on the following day. Programme (Talk times and abstracts are available from the workshop website: http://www.mlworkshop.org/ml2015/). * The History of Standard ML: Ideas, Principles, Culture (Invited Talk) David MacQueen * Generating code with polymorphic let Oleg Kiselyov * Polymorphism, subtyping and type inference in MLsub Stephen Dolan and Alan Mycroft * Arduino programming of ML-style in ATS Kiwamu Okabe and Hongwei Xi * Resource monitoring for Poly/ML processes David Matthews, Magnus Stenqvist and Tjark Weber * Full dependency and user-defined effects in F* Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Pierre-Yves Strub, Aseem Rastogi, Antoine Delignat-Lavaud, Karthikeyan Bhargavan, and Cédric Fournet * Dependent types for real-time constraints William Blair and Hongwei Xi * Manifest contracts for OCaml Yuki Nishida and Atsushi Igarashi * Lost in extraction, recovered Éric Tanter and Nicolas Tabareau * GADTs and exhaustiveness: looking for the impossible Jacques Garrigue and Jacques Le Normand
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-07/msg00123.html
Damien Doligez announced:Dear OCaml users, We have the pleasure of celebrating the anniversary of the first transatlantic telegraph cable by announcing the release of OCaml version 4.02.3. This is mainly a bug-fix release, see the list of changes below. It is (or soon will be) available as an OPAM switch, or as a source download here: < http://caml.inria.fr/download.en.html > Happy hacking, -- Damien Doligez for the OCaml team. OCaml 4.02.3: ------------- Bug fixes: - PR#6908: Top-level custom printing for GADTs: interface change in 4.02.2 (Grégoire Henry, report by Jeremy Yallop) - PR#6919: corrupted final_table (ygrek) - PR#6926: Regression: ocamldoc lost unattached comment (Damien Doligez, report by François Bobot) - PR#6930: Aliased result type of GADT constructor results in assertion failure (Jacques Garrigue) Feature wishes: - PR#6691: install .cmt[i] files for stdlib and compiler-libs (David Sheets, request by Gabriel Radanne) - GPR#37: New primitive: caml_alloc_dummy_function (Hugo Heuzard)
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/. Fun With Opam: Advice to My Past Self: http://www.somerandomidiot.com/blog/2015/07/27/fun-with-opam-advice-to-my-past-self/ Full Time: Sr. Software Engineer-Java Scala at The Weather Channel in Atlanta, GA: http://jobs.github.com/positions/fa9f90ae-2fd8-11e5-89d8-951f8e3c66bd Building the LLVM Fuzzer on Debian.: http://www.mega-nerd.com/erikd/Blog/CodeHacking/building-llvm-fuzzer.html OCaml server-side developer at Ahrefs Research (Full-time): http://functionaljobs.com/jobs/8827-ocaml-server-side-developer-at-ahrefs-research
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.