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

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00025.html

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
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00031.html

> 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/
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00032.html

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
      

> 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.
      

> 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.
      

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
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00039.html

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'.
      

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).
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00048.html

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.
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00065.html

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 !
      

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...        
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00066.html

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
      

> 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.
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00072.html

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.
      

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