Previous week Up Next week
Hello,
Here is the latest Caml Weekly News, week 15 to 22 July, 2003.
1) formal proof of ocaml's Set module
2) camomile-0.4.0
3) ICFP 2003 -- Call for Participation
4) adding data persistency in Ocaml...
5) ocamlmklib on Windows
6) GODI
7) Implementation of the Porter stemming algorithm
8) OCaml test release 3.07 beta 1
==============================================================================
1) formal proof of ocaml's Set module
------------------------------------------------------------------------------
** Jean-Christophe Filliatre announced:
For those interested about formal proofs: ocaml's Set module has been
formally proved correct using the Coq proof assistant. Details can be
checked out from http://www.lri.fr/~filliatr/fsets/
During the process of verification, two small mistakes were found
(AVLs incorrectly balanced), which are already fixed in ocaml's CVS
sources.
This formalization also includes the developement and formal proof of
a similar library (i.e. same interface) using red-black trees.
==============================================================================
2) camomile-0.4.0
------------------------------------------------------------------------------
** Yamagata Yoriyuki announced:
I am pleased to announce camomile-0.4.0, new release of a
comprehensive Unicode library for ocaml. The changes are
* Camomile (previously Base)
- Renamed to Camomile.
- USet (Unicode character sets), UCharTbl (fast lookup tables)
- SubText
* URe, UReStr (Regular Expression) are added.
* UTF16, UCS4 (new Unicode string types) are added.
* findlib support (contributed by KAWAKAMI shigenobu)
* ocamldoc support
Download:
http://prdownloads.sourceforge.net/camomile/camomile-0.4.0.tar.bz2
For more detail, visit our homepage,
http://camomile.sf.net
==============================================================================
3) ICFP 2003 -- Call for Participation
------------------------------------------------------------------------------
** Olin Shivers announced:
ICFP (the International Conference on Functional Programming) is coming up
soon -- August 25-29, in Uppsala, Sweden. The following "Call for
Participation" has the important bits, but here are the two key things you
need to know if you are thinking of attending this year:
- Registration is open *now*.
- You want to register *well before* July 30 -- the deadline for early
registration is 7/30, and most hotels will close out their guaranteed
reservations by then, if not earlier.
I also append the complete program of talks.
See you in Sweden...
-Olin Shivers
program chairman
-------------------------------------------------------------------------------
Call for Participation
ICFP 2003: ACM International Conference on Functional Programming
August 25-29, 2003
Uppsala, Sweden
* About ICFP
------------
The goal of ICFP is to
- stimulate and promote international research on functional programming, and
- act as focal point to bring together the functional-programming
community for intellectual cross-pollination and collaboration.
The scope of the conference includes all languages that encourage programming
with functions, including both purely applicative and imperative languages, as
well as languages that support objects and concurrency. The topics covered
range from principles to practice, from foundations to features, and from
abstractions to applications.
The conference is affiliated with PLI, a confederation of international
meetings sponsored by ACM SIGPLAN, which this year will also include
- PPDP (International Conference on Principles and Practice of
Declarative Programming)
- LOPSTR (International Symposium on Logic-based Program Synthesis
and Transformation)
- Haskell Workshop
- Erlang Workshop
- MERLIN (Mechanised Reasoning About Languages with Variable Binding)
- DPCOOL (Declarative Programming in the Context of Object-oriented
Languages)
* Useful URLs
-------------
- Main web page for the entire PLI meeting; contains information on accepted
papers, registration, accomodation, and social events:
http://www.it.uu.se/pli03/
- Main web page for ICFP:
http://www-users.cs.york.ac.uk/~colin/icfp2003.html
- ICFP programme:
http://www.cc.gatech.edu/~shivers/icfp03/schedule.html
* Registration now open
-----------------------
Registration is now open and the early registration deadline is July 30th.
NOTE: The cut-off date for guaranteed hotel reservations varies
with the hotel and is typically *before* July 30th. It is advisable to
make your hotel reservations soon.
-------------------------------------------------------------------------------
* Conference programme
----------------------
Monday 25 August 2003
Invited talk: 9:00-10:00
------------------------
Conservation of information: Applications in functional,
reversible, and quantum computing
Thomas Knight, Jr. (MIT Artificial Intelligence Laboratory)
Session I: 10:30-12:30
----------------------
Scripting the type-inference process
Bastiaan Heeren, Jurriaan Hage, Doaitse Swierstra (Universiteit Utrecht)
Discriminative sum types locate the source of type errors
Matthias Neubauer, Peter Thiemann (Universität Freiburg)
MLF: Raising ML to the power of system F
Didier Le Botlan, Didier Remy (INRIA Rocquencourt)
An extension of HM(X) with bounded existential and universal data-types
Vincent Simonet (INRIA Rocquencourt)
Session II: 2:15-3:45
---------------------
CDuce: an XML-centric general-purpose language
Véronique Benzaken (LRI, Université Paris Sud, Orsay),
Giuseppe Castagna (CNRS, LIENS, École Normale Supérieure),
Alain Frisch (LIENS, École Normale Supérieure, Paris)
Compiling regular patterns
Michael Levin (University of Pennsylvania)
Software is discrete mathematics
Rex Page (University of Oklahoma)
Session III: 4:15-6:00
----------------------
Global abstraction-safe marshalling with hash types
James Leifer (INRIA Rocquencourt), Gilles Peskine(INRIA Rocquencourt),
Peter Sewell (University of Cambridge), Keith Wansbrough
(University of Cambridge)
Dynamic rebinding for marshalling and update, with destruct-time lambda
Gavin Bierman (University of Cambridge), Michael Hicks (University of
Maryland, College Park), Peter Sewell (University of Cambridge), Gareth
Stoyle (University of Cambridge), Keith Wansbrough (University of
Cambridge)
Iterative-free program analysis
Mizuhito Ogawa (Japan Advanced Institute of Science and Technology),
Zhenjiang Hu (University of Tokyo), Isao Sasano (Japan Advanced
Institute of Technology and Science)
Report on ICFP 2003 & 2004
Olin Shivers & Kathleen Fisher
===============================================================================
Tuesday 26 August 2003
Invited talk: 9:00-10:00
------------------------
From Hilbert space to Dilbert space: Context semantics as a language for
games and flow analysis
Harry Mairson (Brandeis University)
Session IV: 10:30-12:30
-----------------------
A theory of aspects
David Walker (Princeton University), Steve Zdancewic (University of
Pennsylvania), Jay Ligatti (Princeton University)
Dependency-style Generic Haskell
Andres Löh, Dave Clarke, Johan Jeuring (Universiteit Utrecht)
Functional automatic differentiation with Dirac impulses
Henrik Nilsson (Yale University)
A user-centred approach to functions in Excel
Simon Peyton Jones (Microsoft Research), Alan Blackwell (University of
Cambridge), Margaret Burnett (Oregon State University)
Session V: 2:15-3:45
--------------------
A sound and complete axiomatization of delimited continuations
Yukiyoshi Kameyama (University of Tsukuba), Masahito Hasegawa (Kyoto
University)
Call-by-value is dual to call-by-name
Philip Wadler (Avaya Labs)
Disjunctive normal forms and local exceptions
Emmanuel Beffara, Vincent Danos (Université Paris 7)
Session VI: 4:15-6:00
---------------------
An effective theory of type refinements
Yitzhak Mandelbaum (Princeton University), David Walker (Princeton
University), Robert Harper (Carnegie Mellon University)
A static type system for JVM access control
Tomoyuki Higuchi, Atsushi Ohori (Japan Advanced Institute of Science and
Technology)
Parsing polish, step by step (functional pearl)
John Hughes (Chalmers University), Doaitse Swierstra (Universiteit
Utrecht)
Programming contest awards presentation
John Hughes et al. (Chalmers University of Technology)
===============================================================================
Wednesday 27 August 2003
Session VII: 9:00-10:30
-----------------------
Boxes go bananas: Encoding higher-order abstract syntax with parametric
polymorphism
Geoffrey Washburn, Stephanie Weirich (University of Pennsylvania)
FreshML: Programming with binders made simple
Mark Shinwell, Andrew Pitts, Murdoch Gabbay (University of Cambridge)
Meta-programming through typeful code representation
Chiyan Chen, Hongwei Xi (Boston University)
Session VIII: 11:00-11:30
-------------------------
Optimistic evaluation: An adaptive evaluation strategy for non-strict
programs
Robert Ennals (University of Cambridge), Simon Peyton Jones
(Microsoft Research)
Invited talk (joint with PPDP'03): 11:30-12:30
----------------------------------------------
Understanding aspects
Mitchell Wand (Northeastern University)
==============================================================================
4) adding data persistency in Ocaml...
------------------------------------------------------------------------------
** Following a discussion on data persistency, James Leifer said:
We (J.J. Leifer, G. Peskine, P. Sewell, K. Wansbrough) have worked on
a theory of type-safe marshalling for values of abstract types. The
theory ensures type and abstraction safety when communicating between
separately built programs. The idea is to calculate hashes
(fingerprints) of modules to generate type identifiers for abstract
types that are globally meaningful. These hashes are then compared at
run-time in a dynamic check when unmarshalling.
The ICFP paper about this is ``Global abstraction-safe marshalling
with hash types'':
http://pauillac.inria.fr/~leifer/research.html
There are limitations to the current theory (no polymorphism, no
functors, no reference cells, no versioning, no dynamic binding, ...)
that we are working to overcome. Peskine is interested in the
polymorphism question and may try to do an implementation of safe
marshalling for Ocaml. Some of Sewell's interns are also working on
implementations of various aspects of this in a toy ``mini'' Caml
language.
==============================================================================
5) ocamlmklib on Windows
------------------------------------------------------------------------------
** Richard Jones asked and Xavier Leroy answered:
> Has anyone successfully compiled ocamlmklib on Windows? I'd like to
> build a Windows native port of camlimages, but lack of this program in
> the basic distribution is stopping me.
There's a mismatch between the ocamlmklib approach and Windows DLLs
that has prevented me so far from making the former work with the
latter.
Basically, ocamlmklib assumes that, from the *same* set of object C
files, one can build both
- a static library that can be statically linked with the Caml runtime system
and the application, and
- a shared library (DLL) that can be dynamically linked with the Caml
runtime system and the application.
This does *not* appear to be the case for Windows. Namely, a static
lib that accesses a global variable defined in the Caml runtime system
does this directly, while a DLL must do it through one additional
indirection. Thus, the code for the library must be compiled differently
(using / not using "__declspec(dllimport)" specifiers) depending on
whether it is to be put in a static library or in a DLL. With the
Mingw toolchain, it seems possible to generate code that works in both
contexts, but I was unable to do this with the MSVC toolchain.
So, no ocamlmklib under Windows. Still, you can look at some of the
Win32 makefiles in the OCaml source distribution for examples of how
to build mixed C/Caml libraries under Windows. (Look at
otherlibs/win32unix/Makefile.nt for instance.)
==============================================================================
6) GODI
------------------------------------------------------------------------------
** There has been a long discussion thread about packaging. The thread starts
at http://caml.inria.fr/archives/200307/msg00140.html
Here is one message from this thread.
** Gerd Stolpmann said:
Recently I did an experiment called GODI ("Gerd's Ocaml Distribution").
The idea was to implement this kind of extended package management with
minimum effort. I call it an experiment, because the aim was not to
create a working system, but simply to find out what works and what does
not work.
At the beginning there was an analysis of the system environments. The
point is crucial for the success:
* We have the Unix world, and we have the Windows port, both with
totally different toolchains
* We have Open Source systems (Linux distros, BSD distros) that
have good library support, and we have proprietary systems that
lack libraries (think of gtk).
Any package management system should integrate well with the operating
system it runs on. It should be possible to use the components of the
system as far as possible, and to create components of the system.
Anything else is impractical. For GODI, I have ignored the Windows
problem, but there could be a solution based on mingw (as good
compromise between "Unixfication" and system integration). So I
concentrated on the integration into Unix-style systems.
The library problem: Many Unixes do not have the C libraries we need, or
have only ancient versions. Example: Solaris has ndbm, but you usually
do not want it for new programs because of its limitations, better you
install gdbm or Berkeley DB. Other required libraries (for a useful
system) are completely missing, e.g. gtk. Further problems arise with
missing tools, e.g. gmake. Of course, this is not only an O'Caml
problem, but it is a problem of the users, and we have certainly to deal
with it.
The next point is that findlib is not enough. It cannot manage arbitrary
files, but only the linkable parts of libraries. (Don't forget that
libraries sometimes need tools (e.g. rpcgen), or data files (e.g.
message catalogs). findlib cannot manage these files.)
So we definetely need a database of installed files. Many operating
systems already have such databases (e.g. rpm is such a database), and
the question arises whether to use it for O'Caml packages or not. Pro:
better system integration, especially with the required libraries if the
system provides them. Con: The various package databases are very
different, and not every system has even one. (Note: Perl has its own
very simple file database, the .packlist files.)
For GODI, I have used one of the simplest available package databases,
the NetBSD package system. It is binary-only, records dependencies and
file checksums, and this is more or less already the end of the feature
list. It fulfils an absolute requirement: It runs everywhere because of
its simplicity.
For the finally used system, I would suggest that (1) we use our own
file database, and (2) allow it to record dependencies on the native
file database of the operating system ("foreign dependencies").
When we have a real file database, we can also provide C libraries that
are missing especially in proprietary operating systems.
This would be the "binary picture" of the package system: The packages
are the units of the file database. They can have dependencies on each
other, and they can have foreign dependencies on the system packages.
Every package that is an O'Caml library would follow findlib's
conventions.
Now the more difficult question: The build environment. For GODI, I have
used the NetBSD pkgsrc system as framework. It has the following
features:
* The functions of the build environment are implemented with
Makefiles (of course, the BSD "make" is used), and by including
a Makefile of the framework into your own Makefile you can
"load" a certain set of functions
* Every binary package is created by the Makefile in a source
directory. This Makefile is a "driver Makefile" that downloads
the real source, builds it, installs it, and creates the binary
package. The driver Makefile does usually not include the rules
to compile the sources, it rather calls the Makefile contained
in the sources for this purpose.
* The framework implements build-time dependencies and the
automatic download of the source tar.gz.
* There are much more functions, most of them related to building
of C programs and libraries
The use of Makefiles for the build framework has one clear advantage:
its flexibility. More or less, the Makefiles are "action objects", and
including another Makefile is "inheritance", i.e. it is nothing but an
object-oriented build system.
The problem of the NetBSD approach is that the driver Makefiles to build
the packages are simple, unpackaged files. There are no "source
packages". If you want to update the driver Makefiles, you usually do
that by "cvs update". This is a simple solution, but there is no
guarantee that the current CVS state of the Makefiles works, especially
regarding the dependencies. One needs a release management, i.e. from
time to time the CVS depot must be stabilized.
I am not sure whether this is the right model for O'Caml packages.
First, you need people that integrate packages into the system (you need
a CVS account). Second, you need users with CVS experience. Third, it is
difficult to deviate from CVS, e.g. by installing different versions.
So far my GODI experiment. It is not yet available for download, but if
somebody is interested in it I can make a web page for it.
> Given a choice between having quick-and-dirty working code and code that
> works the 'right' way, the latter's better, of course. But when the choice
> is between working code and seeing 20 people never ever get past arguing
> what the right way it should be done is (Which seems to be what happens
> every time someone mentions an ocaml version of CPAN), I'll take something
> that works.
This is one of the reasons I actually did GODI. It is working code, and
it is now much harder to argue against its principles.
==============================================================================
7) Implementation of the Porter stemming algorithm
------------------------------------------------------------------------------
** Erik Arneson announced:
I have written an implementation of the Porter stemming algorithm for OCaml.
It only works correctly on English words, but it will be very handy for
anybody implementing any sort of searching or indexing program.
It can be downloaded at:
< http://www.aarg.net/~erik/ocaml/stemmer-0.1.0.tar.gz >
==============================================================================
8) OCaml test release 3.07 beta 1
------------------------------------------------------------------------------
** Xavier Leroy announced:
A pre-release (3.07 beta 1) of what should soon become the next stable
release of Objective Caml is available for testing at
http://caml.inria.fr/ocaml/distrib-3.07beta1.html
This is a source-only release: no precompiled binaries are available,
however the provided sources compile cleanly under Unix / Linux, MacOS X
and MS Windows. The documentation was updated and is available from
the URL above.
The purpose of this release is to give all OCaml users an opportunity
to test it against their favorite Caml applications and libraries,
and help us make a really solid stable release of OCaml by the end of
August if everything goes well.
Please keep us informed of the results of the tests: a short message
to caml@inria.fr of the form "I tested library Foo and program Bar and
it worked" will be very much appreciated. Of course, bug reports
should be sent to caml-bugs@inria.fr instead.
A detailed list of changes since OCaml 3.06 is appended below. The
main novelties are:
- Experimental support for recursive module definitions.
- "Private types", i.e. variant or record types that can be destructured
but not constructed outside of their defining module.
- Browsing of inferred types (point to an expression in the source
code and see its inferred type).
- AMD64 (Opteron) port of the native-code compiler.
Enjoy,
- Xavier Leroy
--------------------------------------------------
Objective Caml 3.07:
--------------------
Language features:
- Experimental support for recursive module definitions
module rec A : SIGA = StructA and B : SIGB = StructB and ...
- Support for "private types", or more exactly concrete data types
with private constructors or labels. These data types can be
de-structured normally in pattern matchings, but values of these
types cannot be constructed directly outside of their defining module.
- Added integer literals of types int32, nativeint, int64
(written with an 'l', 'n' or 'L' suffix respectively).
Type-checking:
- Allow polymorphic generalization of covariant parts of expansive
expressions. For instance, if f: unit -> 'a list, "let x = f ()"
gives "x" the generalized type forall 'a. 'a list, instead of '_a list
as before.
- Lots of bug fixes in the handling of polymorphism and recursion inside
types.
- Added a new "-dtypes" option to ocamlc/ocamlopt, and an emacs extension
"emacs/caml-types.el". The compiler option saves inferred type information
to file *.types, and the emacs extension allows the user to look at the
type of any subexpression in the source file. Works even in the case
of a type error (all the types computed up to the error are available).
This new feature is also supported by ocamlbrowser.
Both compilers:
- Added option "-dtypes" to dump detailed type information to a file.
- The "-i" option no longer generates compiled files, it only prints
the inferred types.
- The sources for the module named "Mod" can be placed either in Mod.ml or
in mod.ml.
- Compilation of "let rec" on non-functional values: tightened some checks,
relaxed some other checks.
- Fixed wrong code that was generated for "for i = a to max_int"
or "for i = a downto min_int".
- An explicit interface Mod.mli can now be provided for the module obtained
by ocamlc -pack -o Mod.cmo ... or ocamlopt -pack -o Mod.cmx ...
- Revised internal handling of source code locations, now handles
preprocessed code better.
- Pattern-matching bug on float literals fixed.
- Minor improvements on pattern-matching over variants.
- More efficient compilation of string comparisons and the "compare" function.
- More compact code generated for arrays of constants.
- Fixed GC bug with mutable record fields of type "exn".
- Added warning "E" for "fragile patterns": pattern matchings that would
not be flagged as partial if new constructors were added to the data type.
Bytecode compiler:
- Added option -vmthread to select the threads library with VM-level
scheduling. The -thread option now selects the system threads library.
Native-code compiler:
- New port: AMD64 (Opteron).
- Fixed instruction selection bug on expressions of the kind (raise Exn)(arg).
- Several bug fixes in ocamlopt -pack (tracking of imported modules,
command line too long).
- Signal handling bug fixed.
- x86 port:
Added -ffast-math option to use inline trigo and log functions.
Small performance tweaks for the Pentium 4.
Fixed illegal "imul" instruction generated by reloading phase.
- Sparc port:
Enhanced code generation for Sparc V8 (option -march=v8) and
Sparc V9 (option -march=v9).
Profiling support added for Solaris.
- PowerPC port:
Keep stack 16-aligned for compatibility with C calling conventions.
Toplevel interactive system:
- Tightened interface consistency checks between .cmi files, .cm[oa] files
loaded by #load, and the running toplevel.
- #trace on mutually-recursive functions was broken, works again.
Standard library:
- Match_failure and Assert_failure exceptions now report
(file, line, column), instead of (file, starting char, ending char).
- float_of_string, int_of_string: some ill-formed input strings were not
rejected.
- Added format concatenation, string_of_format, format_of_string.
- Module Arg: added new option handlers Set_string, Set_int, Set_float,
Symbol, Tuple.
- Modules Lexing and Parsing: added better handling of positions
in source file.
- Module Scanf: %n and %N formats to count characters / items read so far;
assorted bug fixes.
- Modules Set and Map: fixed bugs causing trees to become unbalanced.
- Module Printf: less restrictive typing of kprintf.
- Module Random: better seeding; functions to generate random int32, int64,
nativeint; added support for explicit state management.
- Module Sys: added Sys.readdir for reading the contents of a directory.
Runtime system:
- output_value/input_value: fixed bug with large blocks (>= 4 Mwords)
produced on a 64-bit platform and incorrectly read back on a 32-bit
platform.
- Fixed memory compaction bug involving input_value.
- Added MacOS X support for dynamic linking of C libraries.
- Improved stack backtraces on uncaught exceptions.
- Fixed float alignment problem on Sparc V9 with gcc 3.2.
Other libraries:
- Dynlink:
By default, dynamically-loaded code now has access to all
modules defined by the program; new functions Dynlink.allow_only
and Dynlink.prohibit implement access control.
Fixed Dynlink problem with files generated with ocamlc -pack.
Protect against references to modules not yet fully initialized.
- LablTK/CamlTK: added support for TCL/TK 8.4.
- Str: reimplemented regexp matching engine, now less buggy, faster,
and LGPL instead of GPL.
- Graphics: fixed draw_rect and fill_rect bug under X11.
- System threads and bytecode threads libraries can be both installed.
- System threads: better implementation of Thread.exit.
- Bytecode threads: fixed two library initialization bugs.
- Unix: make Unix.openfile blocking to account for named pipes;
GC bug in Unix.*stat fixed; fixed problem with Unix.dup2 on Windows.
Ocamllex:
- Can name parts of the matched input text, e.g.
"0" (['0'-'7']+ as s) { ... s ... }
Ocamldebug:
- Handle programs that run for more than 2^30 steps.
- Better support for preprocessed code.
Emacs mode:
- Added file caml-types.el to interactively display the type information
saved by option -dtypes.
Win32 ports:
- Cygwin port: recognize \ as directory separator in addition to /
- MSVC port: ocamlopt -pack works provided GNU binutils are installed.
- Graphics library: fixed bug in Graphics.blit_image; improved event handling.
OCamldoc:
- new ty_code field for types, to keep code of a type (with option -keep-code)
- new ex_code field for types, to keep code of an exception
(with option -keep-code)
- some fixes in html generation
- don't overwrite existing style.css file when generating HTML
- create the ocamldoc.sty file when generating LaTeX (if nonexistent)
- man pages are now installed in man/man3 rather than man/mano
- fix: empty [] in generated HTML indexes
==============================================================================
Using folding to read the cwn in vim 6+
------------------------------------------------------------------------------
Here is a quick trick to help you read this cwn if you are viewing it using
vim (at least version 6).
:set foldmethod=expr
:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'<1':1
zM
If you know of a better way, please let me know.
==============================================================================
Old cwn
------------------------------------------------------------------------------
If you happen to miss a cwn, you can send me a message
(alan.schmitt@inria.fr) and I'll mail it to you, or go take a look at
the archive (http://pauillac.inria.fr/~aschmitt/cwn/). If you also wish
to receive it every week by mail, just tell me so.
==============================================================================
Alan Schmitt