Hello, Here is the latest Caml Weekly News, for the week of January 08 to 15, 2013.
1) Batteries 2.0.0 released 2) wrap/unwrap some OCaml code in Emacs 3) some beautiful OCaml code 4) PG'OCaml 1.7 5) FoCaLiZe 0.8.0 6) new meetup: OUPS - Ocaml Users in PariS and OPAM Party 7) ilist-0.1.0 - indexed lists 8) Propagating types to pattern-matching 9) Other Caml News ======================================================================== 1) Batteries 2.0.0 released Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00025.html> ------------------------------------------------------------------------ ** Edgar Friendly announced: Batteries 2.0.0 is now available for general consumption. After years of having to put up with the oddity that is "Batteries_uni" and the issues with Camomile's data files, the Batteries Included Team is proud to break backwards compatibility and release version 2.0.0 to fix these. Now free of any camlp4 and made of 100% pure OCaml with no external dependencies, batteries is easier to build and better than ever. A complete list of API incompatible changes and new additions is available at <https://github.com/ocaml-batteries-team/batteries-included/wiki/Interfacechanges12> and the new documentation is online at <http://ocaml-batteries-team.github.com/batteries-included/hdoc2/index.html> Download from ocamlforge at <https://forge.ocamlcore.org/frs/download.php/1096/batteries-2.0.tar.gz> ======================================================================== 2) wrap/unwrap some OCaml code in Emacs Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00031.html> ------------------------------------------------------------------------ ** Francois Berenger asked and Gaius Hammond replied: > Anyone has something to recommend in order to do this in Emacs for OCaml > code? > > The use case is you have a big file and you only want to only see the > code of a few functions and only the first line for other functions. Code folding, this is usually called. See <http://gaiustech.wordpress.com/2010/09/20/code-folding-in-emacs/> ======================================================================== 3) some beautiful OCaml code Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00032.html> ------------------------------------------------------------------------ ** Francois Berenger said: The code is here: <https://raw.github.com/orbitz/blog_post_src/master/intro_return_t/ex5.ml> There is a full blog post about it there: <http://functional-orbitz.blogspot.se/2013/01/introduction-to-resultt-vs-exceptions.html> Regards, F. PS: I'm not the author of this beauty ** David Mentre asked and Malcolm Matalka replied: > Regarding this blog post, the final code is using Polymorphic Variants > (<http://caml.inria.fr/pub/docs/manual-ocaml/manual006.html#toc36>). > E.g. > """ > | _ -> > Error (`Bad_line s) > """ > > I never fully grasped polymorphic variants compared to regular ones > but I always had the feeling the polymorphic variants where less safe > that variants because they would allow more possibility to mix > unrelated things[1]. > > Are the use of polymorphic variant mandatory to write code > Return-Value-style code or can regular variants be used? > > Best regards, > david > > [1] Of course this ability is the very thing that is of interest to > people using polymorphic variants. Hey, author here, The problem polymorphic variants are solving here is that if you want to sequence unrelated functions but return their errors, you have to join their return types with the return types of the function that is calling them. Polymorphic variants basically do this for you without every function defining its own error return variant. This, so far, is the only time I have found polymorphic variants the best solution for a problem in Ocaml. ** Gerd Stolpmann also replied to David: > I never fully grasped polymorphic variants compared to regular ones > but I always had the feeling the polymorphic variants where less safe > that variants because they would allow more possibility to mix > unrelated things[1]. That's exactly the point: Polyvariants allow you to mix unrelated things. I don't think, though, that they are unsafer, because you get help from the compiler to keep these things nevertheless separated. You need to be aware what can happen, and here and there it is helpful to add a type hint or a coercion to control typing. > Are the use of polymorphic variant mandatory to write code > Return-Value-style code or can regular variants be used? No. You can also use normal variants, but of course you need then a declaration like type error = Bad_line of string | Bad_name of string | ... before using it. Also, function composition can be very painful. Imagine you wrote two modules M1 and M2 in this style, and each module defines an error type. Now you want to call functions from both modules at one place, and run into the problem that you get [Error e1] values with [e1:M1.error_type] and [Error e2] values with [e2:M2.error_type]. There is no simple way to mix that. Probably you need to do type error = M1_error of M1.error | M2_error of M2.error which is kind of inelegant. Polyvariants, in contrast, allow you to directly unite the error types as long as the tags are not contradictory. This means function composition as again as easy as if you used exceptions for error reporting. ** Kristopher Micinski also replied: I would say that it's not that polymorphic variants are less safe, but they can occasionally be more painful, because of the explicit type signatures, and because of type inference you can end up with some ugly errors. It's typically recommended that when you use polymorphic variants you use explicit annotations. I suppose they could be unsafe if, say, you had two similarly named constructors with the same signature that had different semantics between different modules. But that would probably be bad style to begin with. There's a StackOverflow guide on when to use polymorphic variants, I agree with the answer: <http://stackoverflow.com/questions/9367181/variants-or-polymorphic-variants> ======================================================================== 4) PG'OCaml 1.7 Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00039.html> ------------------------------------------------------------------------ ** Dario Teixeira announced: I'm happy to announce release 1.7 of PG'OCaml. This release brings the long awaited cleanup of the directory structure (or previous lack thereof), and the migration of the build system to OASIS, which should make life easier for users and packagers. Speaking of the latter: I welcome feedback from maintainers of Debian/Fedora/Arch packagers on further changes that would make their life easier. Note that building the tests is currently broken due to a known issue with OASIS and syntax extensions. Also of note is that PG'OCaml now depends on Batteries 2.0. Users of ExtLib are strongly advised to migrate to Batteries, as there is no easy mechanism to build against ExtLib (if someone *really* needs this, it's not particularly hard either, but it does require some manual tweaking of the _oasis file). The package for 1.7 has already been pushed to the OPAM repository, and should appear upon an 'opam update'. ** He later added: In the meantime, Sebastien Mondet noticed a missing dependency in the _oasis file which caused a linking error. I've just released version 1.7.1, which fixes that problem (OPAM package has already been pushed to the repository). ======================================================================== 5) FoCaLiZe 0.8.0 Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00048.html> ------------------------------------------------------------------------ ** François Pessaux announced: It is my pleasure to announce the new release for FoCaLiZe (the 0.8.0 version). After a pretty long time without release, this new version brings number of enhancements, from the focalizec compiler and Zenon. New versions of OCaml and Coq are now supported as well as previous ones for sake of legacy. Zenon made impressive progress so as to be helpful in proving inductive properties for species. Installation and setup have been fully revisited, leading in a simpler and lighter mechanism. The standard library has been extended with low-level theorems. Termination proofs for structurally recursive functions are now possible. A certains number of bugs found in the focalizec compiler have been fixed. And a new tutorial about making proofs with Zenon is born. A complete description of changes / new features can in found in the CHANGES file of the distribution. The 0.8.0 release is available from FoCaLiZe.inria.fr at <http://focalize.inria.fr/download/focalize-0.8.0.tgz> Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.8.0 and follow the simple instructions written there. A public GIT repository is also available, allowing to fetch the latest development state of FoCaLiZe. However, its content is not bullet-proof and may be unstable at some times. It reflects the real-time state of FoCaLiZe and may bring fixes and features not available in previous releases and that will be part of the next release. To clone the current FoCaLiZe GIT repository, invoke: git clone <http://focalize.inria.fr/focalize.git> This will create a focalize repository in your current directory. Once cloned, it is possible to fetch updates with the usual GIT commands (essentially git pull origin master). Note that this access being public, it doesn't allow pushing (i.e. submitting) modifications done in the sources tree. To join people and discussions write to focalize-users AT inria.fr. Implementors also listen to suggestions and compliments at mail adress focalize-devel AT inria.fr. Enjoy. For the entire FoCaLiZe implementor group, -- François Pessaux ENSTA ParisTech - UIIS - francois.pessaux (at) ensta-paristech.fr January 2013 What is it FoCaLiZe ? --------------------- FoCaLiZe is an integrated development environment to write high integrity programs and systems. It provides a purely functional language to formally express specifications, describe the design and code the algorithms. Within the functional language, FoCaLiZe provides a logical framework to express the properties of the code. A simple declarative language provides the natural _expression_ of proofs of properties them from within the program source code. The FoCaLiZe compiler extracts statements and proof scripts from the source file, to pass them to the Zenon proof generator to produce Coq proof terms that are then formally verified. The FoCaLiZe compiler also generates the code corresponding to the program as an Objective Caml source file. This way, programs developped in FoCaLiZe can be efficiently compiled to native code on a large variety of architectures. Last but not least, FoCaLiZe automatically generates the documentation corresponding to the development, a requirement for high evaluation assurance. The FoCaLiZe system provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation, while proving that their implementation meets its specification or design requirements. The FoCaLiZe language offers high level mechanisms such as inheritance, late binding, redefinition, parametrization, etc. Confidence in proofs submitted by developers or automatically generated ultimately relies on Coq formal proof verification. FoCaLiZe is a son of the previous Focal system. However, it is a completely new implementation with vastly revised syntax and semantices, featuring a rock-solid infrastructure and greatly improved capabilities. ======================================================================== 6) new meetup: OUPS - Ocaml Users in PariS and OPAM Party Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00065.html> ------------------------------------------------------------------------ ** Fabrice Le Fessant announced: We have created a meetup for OCaml users, located around Paris. It is called OUPS (Ocaml Users in PariS), and we plan to use it to organize events regularly about OCaml in different places around Paris: <http://meetup.ocaml-lang.fr/> (or <http://www.meetup.com/ocaml-paris/> ) The first event will be an "OPAM party", on Tuesday, Jan 29, at IRILL. It will be an oppportunity to meet, discuss about OCaml, and also start using OPAM, or even more, start packaging programs and libraries with OPAM. During the event, it is possible to give small talks on OCaml related topics. If you are interested to do so, you should send me a title and a duration, so that I can organize the timing of the talks. Do not hesitate to register on the meetup to be kept informed, and to tell other people interested about OCaml in Paris area about this meetup, so that they can register and come too ! ** He later added: I forgot to specify : it's on Tuesday evening, not during working hours. The idea is to have informal discussions, some light presentations. Since the next "main" topic is OPAM, you can also send us the particular things that you would like to know about it, specific things that you want to do, etc... ======================================================================== 7) ilist-0.1.0 - indexed lists Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00066.html> ------------------------------------------------------------------------ ** Wojciech Meyer announced: I'm happy to release a small library that brings up to use convenience and safety of indexed lists using GADT encodings. The tarball can be fetched here: <http://danmey.org/ilist-0.1.0.tar.gz> OPAM packaging will be available shortly. Currently the library contains just two modules: NList - length indexed list IList - heterogeneous list where each element can have it's own type syntax extension: Pa_ilist - allows to use the list literals and pattern matching on the lists. While using Camlp4 might be useful, it's being considered to use -ppx extensions instead present on the current OCaml trunk. and plenty of examples what can be done using the library. NList can be used everywhere we need an invariant on length encoded in a type. For instance now a list of at least one element encoded as a tuple of the first element and the rest as a list now can be encoded directly as an Nlist. IList is probably most similar to tuples with one exception, that now we can encode a generic extraction and extending functions that will work on any sized lists (compare IList.hd to fst), so it behaves like an extensible tuple. Project home: <https://github.com/danmey/Ilist> Bugs & features: <https://github.com/danmey/Ilist/issues> License: BSD3 ** Erkki Seppala asked and Wojciech Meyer replied: > Pretty nice! But I must not be the only one thinking this would be even > more useful with arrays? I imagine it would need to be a bit different, > have the array type alongside with similar kind of linked list of > types. Thanks. > Do you think it would be doable, though? I can't see it. I believe it would be only practical with a decent syntax extension. We would need be able to encode the length inside the type, and for arrays this might be quite huge - however this would be no problem part (apart from efficiency of type checking), the problematic part would be to encode the concatenation of arrays - which can be done as in omega encoding using witnesses. Also then random access of arrays would need sort of natural encoded integers. One could even think about arrays of size n^2 supporting only doubling the size. We would be getting here to dependent types, that's probably why I decided that Ilist is would not be a collection of data structures. ======================================================================== 8) Propagating types to pattern-matching Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00072.html> ------------------------------------------------------------------------ ** Jacques Garrigue said: Dear Camlers, It is a bit unusual, but this message is about changes in trunk. As you may be aware from past threads, since the introduction of GADTs in 4.00, some type information is propagated to pattern-matching, to allow it to refine types. More recently, types have started being used to disambiguate constructors and record fields, which means some more dependency on type information in pattern-matching. However, a weakness of this approach was that propagation was disabled as soon as a pattern contained polymorphic variants. The reason is that typing rules for polymorphic variants in patterns and expression are subtly different, and mixing information without care would lose principality. At long last I have removed this restriction on the presence of polymorphic variants, but this has some consequences on typing: * while type information is now propagated, information about possibly present constructors still has to be discarded. For instance this means that the following code will not be typed as you could expect: let f (x : [< `A | `B]) = match x with `A -> 1 | _ -> 2;; val f : [< `A | `B > `A ] -> int What happens is that inside pattern-matching, only required constructors are propagated, which reduces the type of x to [> ] (a polymorphic variant type with any constructor?) As before, to give an upper bound to the matched type, the type annotation must be inside a pattern: let f = function (`A : [< `A | `B]) -> 1 | _ -> 2;; val f : [< `A | `B ] -> int = <fun> * the propagation of type information may lead to failure in some cases that where typable before: type ab = [ `A | `B ];; let f (x : [`A]) = match x with #ab -> 1;; Error: This pattern matches values of type [? `A | `B ] but a pattern was expected which matches values of type [ `A ] The second variant type does not allow tag(s) `B During pattern-matching it is not allowed to match on absent type constructors, even though the type of the patterns would eventually be [< `A | `B], which allows discarding `B. ([? `A | `B] denotes a type obeying the rules of pattern-matching) * for the sake of coherence, even if a type was not propagated because it was not known when typing a pattern-matching, we are still going to fail if a matched constructor appears to be absent after typing the whole function. (This only applies to propagable types, i.e. polymorphic variant types that contain only required constructors) In particular the last two points are important, because previously such uses would not have triggered even a warning. The idea is that allowing propagation of types is more important than keeping some not really useful corner cases, but if this is of concern to you, I'm interested in feedback. ======================================================================== 9) Other Caml News ------------------------------------------------------------------------ ** From the ocamlcore planet blog: Thanks to Alp Mestan, we now include in the Caml Weekly News the links to the recent posts from the ocamlcore planet blog at <http://planet.ocaml.org/>. Focalize 0.8.0: <http://caml.inria.fr/cgi-bin/hump.cgi?contrib=326> PGOCaml 1.7.1: <http://caml.inria.fr/cgi-bin/hump.cgi?contrib=501> Static exceptions: <http://www.lexifi.com/blog/static-exceptions> Introduction to Mezzo: <http://gallium.inria.fr/blog/introduction-to-mezzo> ======================================================================== Old cwn ------------------------------------------------------------------------ If you happen to miss a CWN, you can send me a message (alan.schm...@polytechnique.org) and I'll mail it to you, or go take a look at the archive (<http://alan.petitepomme.net/cwn/>) or the RSS feed of the archives (<http://alan.petitepomme.net/cwn/cwn.rss>). If you also wish to receive it every week by mail, you may subscribe online at <http://lists.idyll.org/listinfo/caml-news-weekly/> . ======================================================================== _______________________________________________ caml-news-weekly mailing list caml-news-weekly@lists.idyll.org http://lists.idyll.org/listinfo/caml-news-weekly
