Hello
Here is the latest Caml Weekly News, for the week of October 24 to November 07, 2006.
A new version of dypgen is available at http://perso.ens-lyon.fr/emmanuel.onzon/ It fixes bugs with merge functions and with the files testdyn1.tiny and testdyn2.tiny. The manual has been completed with examples and more details.
I've created two Mac packages for extlib and findlib and I've submitted patches respectively against extlib-1.5 and findlib-1.1.2pl1. As far as I can see, these packages play well with the mac package of the ocaml toolchain from inria. For those who are interested, you can get patches and packages here. http://users.rsise.anu.edu.au/~abate/macosx/ It would be great if these packages could be hosted somewhere more official (hint hint :)) I haven't tested them very carefully ... so please let me know if I've done something silly...
Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/1eabdb2bc45af369/4670f52ead6095c0
Aleksey Nogin announced:I've built binary RPMs (Red Hat packages) of OCaml 3.09.3 for Fedora 2, 3, 4, 5, and 6 and for Red Hat Enterprise Linux 4. Download them from http://rpm.nogin.org/ocaml.html
I would like to announce a new snapshot release of Olmar -- a system to process C++ programs in Ocaml available from http://www.cs.ru.nl/~tews/olmar/ New in this release: - syntax trees are much larger: All xml annotated fields are available in Ocaml. This includes, for instance, an (elsa computed) type for all expressions. General description: Olmar is a patch for the Elkhound/Elsa [1] C/C++ parser that permits the Elsa parser to translate its internal abstract syntax tree into an Ocaml value, which can then be further processed by an Ocaml program. Olmar comes with ast_graph, a tool that can dump the abstract syntax tree in the dot language. You can therefore now admire the syntax tree of Ocaml's minor garbage collector at http://www.cs.ru.nl/~tews/olmar/minor_gc.ps.gz License: BSD (following Elsa/Elkhound) [1] http://www.cs.berkeley.edu/~smcpeak/elkhound/
We would like to announce the first release of a new system written in OCaml. Bedwyr is an extended logic programming language that allows model-checking directly on syntactic expressions possibly containing bindings. We believe that it's an interesting tool for computer scientists, as it allows simple reasoning on declarative specifications, with several good examples, notably bisimulation checking for the pi-calculus. Other examples include type systems, games, logics, etc. But another interest for the caml-list readers might be the re-usable core components of Bedwyr, notably higher-order pattern unification and term indexing. Although we don't distribute these separately, I'd be happy to do so if anybody is interested. You will find a general description of Bedwyr below this message. More details can be found on Bedwyr website: http://slimmer.gforge.inria.fr/bedwyr/ Sincerely, Bedwyr developers %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Bedwyr A proof-search approach to model checking http://slimmer.gforge.inria.fr/bedwyr/ Bedwyr is a programming framework written in OCaml that facilitates natural and perspicuous presentations of rule oriented computations over syntactic expressions and that is capable of model checking based reasoning over such descriptions. Bedwyr is in spirit a generalization of logic programming. However, it embodies two important recent observations about proof search: (1) It is possible to formalize both finite success and finite failure in a sequent calculus; proof search in such a proof system can capture both may and must behavior in operational semantics specifications. (2) Higher-order abstract syntax can be supported at a logical level by using term-level lambda-binders, the nabla-quantifier, higher-order pattern unification, and explicit substitutions; these features allow reasoning directly on expressions containing bound variables. The distribution of Bedwyr includes illustrative applications to the finite pi-calculus (operational semantics, bisimulation, trace analyses and modal logics), the spi-calculus (operational semantics), value-passing CCS, the lambda-calculus, winning strategies for games, and various other model checking problems. These examples should also show the ease with which a new rule-based system and particular questions about its properties can be be programmed in Bedwyr. Because of this characteristic, we believe that the system can be of use to people interested in the broad area of reasoning about computer systems. The present distribution of Bedwyr has been developed by the following individuals: David Baelde & Dale Miller (INRIA & LIX/Ecole Polytechnique) Andrew Gacek & Gopalan Nadathur (University of Minneapolis) Alwen Tiu (Australian National University and NICTA). In the spirit of an open-source project, we welcome contributions in the form of example applications and also new features from others.
When looking at inferred types in the presence of modules and
combinations of abstract and concrete types, the results are often quite
puzzling. For small pieces of code, it is not a big issue. When one is
using 4th-order functors (!), with a mixture of abstract and concrete
types, a fair amount of type synonyms, error message become extremely
difficult to interpret!
Below is some (largish for an email) code that demonstrates this. It
seems difficult to show how puzzling this gets with much smaller code,
although one can indeed reproduce the behaviour with smaller code.
Consider first
module Sig = struct
type domain_is_field
type domain_is_ring
module type DOMAIN = sig
type kind
type v
val z : v
end
module type COLL = sig
module Dom : DOMAIN
type coll
end
end
module Doms = struct
open Sig
module FDomain = struct
type kind = domain_is_field
type v = float
let z = 0.0
end
module IDomain = struct
type kind = domain_is_ring
type v = int
let z = 0
end
module GColl(Dom:DOMAIN) =
struct
module Dom = Dom
type coll = Dom.v list
end
end ;;
In the above, the printed types all seem quite reasonable.
Now we start with some more complex stuff:
module GEF = struct
open Sig
module DivisionUpdate
(C:COLL with type Dom.kind = domain_is_field) = struct
let update x = x
end
module Gen(C: COLL)
(Update: functor(C:COLL with type Dom.kind = C.Dom.kind)
-> sig val update : C.Dom.v -> C.Dom.v end) =
struct
module U = Update(C)
let foo = U.update(C.Dom.z)
end
end;;
where the printed type is
# module GEF :
sig
module DivisionUpdate :
functor
(C : sig
module Dom :
sig type kind = Sig.domain_is_field type v val z : v end
type coll
end) ->
sig val update : 'a -> 'a end
module Gen :
functor (C : Sig.COLL) ->
functor
(Update : functor
(C : sig
module Dom :
sig
type kind = C.Dom.kind
type v
val z : v
end
type coll
end) ->
sig val update : C.Dom.v -> C.Dom.v end) ->
sig
module U : sig val update : C.Dom.v -> C.Dom.v end
val foo : C.Dom.v
end
end
which seems fair enough. When we start to "test" this, we get:
module Test = GEF.Gen(Doms.GColl(Doms.FDomain))(GEF.DivisionUpdate);;
let test = Test.foo;;
# module Test :
sig
module U :
sig
val update :
Doms.GColl(Doms.FDomain).Dom.v -> Doms.GColl(Doms.FDomain).Dom.v
end
val foo : Doms.GColl(Doms.FDomain).Dom.v
end
# val test : Doms.GColl(Doms.FDomain).Dom.v = 0.
Note how the type of update and foo look very "complex", even though the
typechecker seems to know quite well that 'test' is actually of type
float. How is one supposed to know that the typechecker knows this and
that ...Dom.v is not abstract?
If we continue in that vein, contrast the following:
module C_F = Doms.GColl(Doms.FDomain);;
module Test1 = GEF.Gen(C_F)(GEF.DivisionUpdate);; (* works *)
module C_I = Doms.GColl(Doms.IDomain);;
module Test2 = GEF.Gen(C_I)(GEF.DivisionUpdate);; (* throws an error, as
expected *)
The biggest difference is that FDomain has kind = domain_is_field while
IDomain has kind = domain_is_ring.
Let's look at the printed type of C_F and Test1:
# module C_F :
sig
module Dom :
sig type kind = Doms.FDomain.kind type v = Doms.FDomain.v val z :
v end
type coll = Dom.v list
end
# module Test1 :
sig
module U : sig val update : C_F.Dom.v -> C_F.Dom.v end
val foo : C_F.Dom.v
end
Why Doms.FDomain.kind instead of Sigs.domain_is_field for the kind?
Since test1 *works*, clearly these are known to be the same.
Also, not how foo has type C_F.Dom.v -- which one has to chase to Dom.v,
to Doms.FDomain.v, and finally to float. When this occurs in an error
message, having to do 4 (or more) levels of type-expansions can be quite
difficult. (And misleading too, but that is a different issue).
Now let's look at what we get for the rest:
# module C_I :
sig
module Dom :
sig type kind = Doms.IDomain.kind type v = Doms.IDomain.v val z :
v end
type coll = Dom.v list
end
and then a long error message for Test2, which ends with
Modules do not match:
sig type kind = C_I.Dom.kind type v = Dom.v val z : v end
is not included in
sig type kind = Sig.domain_is_field type v val z : v end
Type declarations do not match:
type kind = C_I.Dom.kind
is not included in
type kind = Sig.domain_is_field
Now, C_I.Dom.kind is actually Sig.domain_is_ring -- why wasn't that
printed? That would have been SO much more informative! In similar
situations, one can take a long time chasing down why it seems that
C_I.Dom.kind was somehow abstract when it should have been concrete, and
so on.
Would it be possible to get some switches to optionally ask for all
types to be fully expanded? Also, it would be nice to be able to
visually distinguish between an abstract type and a concrete but elided
type even when not asking for types to be expanded.
Note that in other situations (the code is even larger), one can get a
strange mixture of non-expanded, partially-expanded and fully-expanded
types all for essentially the same situation, although it seems that
this latter part may be due to MetaOCaml rather than OCaml. But it is
rather difficult to be certain...
Jacques
PS: the work that led up to this email is joint work with Oleg Kiselyov.
> Has anyone done any stuff for localising Ocaml programs? > Something like GNU's gettext system? There is ocaml-gettext: http://sylvain.le-gall.net/ocaml-gettext.html Only the version in svn seems to work with latest caml though, and i can't find a way to access svn exept through the web interface. Hehe.. But we are using it with some success in the demexp project: http://savannah.nongnu.org/projects/demexpSylvain Le Gall added:
Indeed, ocaml-gettext need to be re released soon. I am pretty busy with debian ocaml stuff right now, but i will rework on it ASAP.
> Does any one here know about Ocamlp3l: > http://www.pps.jussieu.fr/~dicosmo/ocamlp3l/ OCamlP3L is a library for OCaml for parallel skeleton programming (P3L skeletons). A parallel skeleton (also know as algorithm skeleton) is a "function" that could be implemented in parallel (the goal is to have a good set of such function : "easy" to be implemented and efficient and can express many parallel problems). For example, List.map. The list could be distributed on the processors and Map could be apply in parallel (if there are no side effects). You should read the papers of Roberto Di Cosmo (for example in the revue "parallel programming") about OCamlP3L and go to this web page (of Murray Cole, the "father" of parallel skeletons) about skeleton programming http://homepages.inf.ed.ac.uk/mic/Skeletons/index.html
[ The following openings might interest members of this list, as it is strongly concerned with (mechanized proofs of) pure functional programs. - Xavier Leroy ] The Compcert project, funded by the French National Agency for Research in its program on the security of computer systems (ANR-SSIA), is offering two post-doctoral positions for durations of up to 18 months, starting in the first half of 2007. The Compcert project is concerned with the formal description of optimizing compilers for high-level languages, including a significant subset of the C programming language, and computer-verified proofs of correctness for these compilers. Foundational aspects of this project include the mechanization of programming language semantics and mechanically verified proofs of correctness for functional and imperative programs. Most proofs and algorithms are verified using the Coq proof assistant. The project is looking for applicants having a solid background in one or preferably two of the following domains: * programming language semantics, * compiler development, * computer-based proof assistants, and a real interest in the other aspects. The topics to be investigated during the post-docs range over the scope of the project, from formal compiler verification to mechanized semantics to connections with other tools (program provers, static analyzers) used to develop high-assurance software. For instance, we envision the following two topics: * A formalization of domain theory inside the type theory of the Coq proof assistant and a study of its applications in the development of correct functional programs, with a special focus on potentially non-terminating programs such as interpreters, debuggers, or semi-algorithms for optimisation problems. * A study of separation logic for the Compcert subset of the C programming language, including formal proofs of consistency between this axiomatic semantics and the operational semantics used in the compiler verification task. Proposals for other relevant topics are welcome and will be discussed between applicants and the investigators of the Compcert project: Xavier Leroy (INRIA, main investigator), Yves Bertot (INRIA), Sandrine Blazy (ENSIIE), Pierre Courtieu (CNAM), Damien Doligez (INRIA), Pierre Letouzey (University of Paris 7), Laurence Rideau (INRIA). The positions are located either in Evry (Paris area, under the supervision of Sandrine Blazy) or Sophia Antipolis (Nice area, French Riviera, under the supervision of Yves Bertot). The gross salary is around 2200 Euros per month (1800 Euros net salary after deduction of social benefits). To apply, please send a detailed vitae and a research statement (indicating the topics on which you'd like to work) to the following address: compcert@yquem.inria.fr. Other inquiries concerning these positions can be sent to this address as well.
I would like to announce availability of the OCaml client interface
library for Oracle. In the contrast to existing projects (oci8ml,
eqoci) found elsewhere, this project uses Oracle 10g's OCCI C++
interface on top of OCI. This allowed to implement a rich set of DML
and DDL operations with the database. The library requires installation
of an Oracle 10g Instant Client library. See doc/index.html file for
installation instruction of prerequisites.
The following operations with an Oracle database are supported:
- Simple DML operations including SELECT / INSERT / UPDATE / DELETE
- Parameterized DML operations including SELECT / INSERT / UPDATE /
DELETE
- Execution of PL/SQL stored procedures
- Execution of bulk DML array INSERT / DELETE / UPDATE operations
- Oracle exception handling
- Oracle bulk exception handling with specifying failed rows and
errors for each row
- Transaction control (commit and rollback)
- Automatic garbage control of Oracle resources (connections, statements
and cursors)
- Functional and Object-Oriented API included
You'll need to modify the Makefile to include paths to an Oracle home
and OCaml installation.
The OCaml portion of the library is written in the revised syntax. The
following example illustrates one of the most powerful features of using
array DML insert of records with exception-based control of failed rows
(note that the entire array is sent to an Oracle database in a single
network roundtrip):
try
let n = statement#execute_array
~sql:"insert into test (id, name, dt, num) values (:1,
:2, :3, :4)"
[
[| Var_int 1; Var_str "AAA"; Null_date; Null_float |];
[| Var_int 2; Null_str; Null_date; Null_float |];
[| Var_int 3; Null_str; Null_date; Null_float |]
]
in
Printf.printf "Inserted %d records using array DML\n" n
with [ORA_BULK_EXCEPTION (m, a) -> do {
print_endline m;
Array.iter (fun (i, e, m) -> Printf.printf " Row[%d]: %d -
%s\n" i e m) a
}
];
The project home page is http://oracaml.sourceforge.net. It contains
links to documentation and download site.
Your feedback and enhancement requests are welcome.
Here is a quick trick to help you read this CWN if you are viewing it using vim (version 6 or greater).
:set foldmethod=expr
:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'<1':1
zM
If you know of a better way, please let me know.
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.