Lambda the Ultimate

Lots of buzz surrounding Clojure these days. The main knock on Clojure has been the lack of tail call optimization. Because of the current lack of TCO on the JVM, Clojure currently doesn't support automated TCO - though the plan is that if the JVM ever adds the capability, Clojure will implement it at that point. The recur syntax is a way to mimic TCO for self-recursion. Now the trampoline for mutual recursion is available for more involved forms of recursion:

I've added trampoline to ease the conversion/creation of mutually
recursive algorithms in Clojure.

Trampolines are a well known technique for implementing TCO - instead
of actually making a call in the tail, a function returns the function
to be called, and a controlling loop calls it, thus allowing chained
execution without stack growth.

As an aside, I have been tinkering with the language and it seems well thought out. For a newbie like myself, the main difference maker is the promotion of common sequences (lists, vectors, maps, sets) to built-in first class collections making it comparable in ease of use to other scripting languages.

Type-Checking Zero Knowledge

This paper presents the first type system for statically analyzing security protocols that are based on zero-knowledge proofs. We show how certain properties offered by zero-knowledge proofs can be characterized in terms of authorization policies and statically enforced by a type system. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. We develop a new type-checker that conducts the analysis in a fully automated manner. We exemplify the applicability of our technique to real-world protocols by verifying the authenticity and secrecy properties of the Direct Anonymous Attestation (DAA) protocol. The analysis of DAA takes less than three seconds.

A little dependent type theory, a little Pi calculus, a little cryptography... there's something for everyone! This is follow-up work to this story that Ehud posted.

The source code can be found here.

Modeling Abstract Types in Modules with Open Existential Types, by Benoît Montagu Didier Rémy:

We propose F^¥, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as done in module systems. The static semantics of F^¥ adapts standard techniques to deal with linearity of typing contexts, its dynamic semantics is a small-step reduction semantics that performs extrusion of type abstraction as needed during reduction, and the two are related by subject reduction and progress lemmas. Applying the Curry-Howard isomorphism, F^¥ can be also read back as a logic with the same expressive power as second-order logic but with more modular ways of assembling partial proofs. We also extend the core calculus to handle the double vision problem as well as type-level and term-level recursion. The resulting language turns out to be a new formalization of (a minor variant of) Dreyer’s internal language for recursive and mixin modules.

This approach to existentials seems to considerably improve their power and simplify their use. It also brings us one step closer to first-class modules!

Factor: an extensible interactive language, Google Tech Talk by Slava Pestov.

Factor is a general-purpose programming language which has been in development for a little over five years and is influenced by Forth, Lisp, and Smalltalk. Factor takes the best ideas from Forth -- simplicity, succinct code, emphasis on interactive testing, meta-programming -- and brings modern high-level language features such as garbage collection, object orientation, and functional programming familiar to users of languages such as Python and JavaScript. Recognizing that no programming language is an island, Factor is portable, ships with a full-featured standard library, deploys stand-alone binaries, and interoperates with C and Objective-C.

In this talk, I will give the rationale for Factor's creation, present an overview of the language, and show how Factor can be used to solve real-world problems with a minimum of fuss. At the same time, I will emphasize Factor's extensible syntax, meta-programming and reflection capabilities, and show that these features, which are unheard of in the world of mainstream programming languages, make programs easier to write, more robust, and fun.

A rather amusing thread on the plt-scheme mailing list, reminded me of Wadler's paper Why Calculating is Better than Scheming from 1987, which wasn't discussed here as far as I recall.

It's a bit of a blast from the past, but still worth reading.

Story on Nabble here. Release note highlights:

Objective Caml 3.11.0:
----------------------

(Changes that can break existing programs are marked with a "*" )

Language features:
- Addition of lazy patterns: "lazy " matches suspensions whose values,
after forcing, match the pattern .
- Introduction of private abbreviation types "type t = private ",
for abstracting the actual manifest type in type abbreviations.

Compilers:
* The file name for a compilation unit must correspond to a valid identifier
(no more "test-me.ml" or "my file.ml".)
* Revised -output-obj: the output name must now be provided; its
extension must be one of .o/.obj, .so/.dll, or .c for the
bytecode compiler. The compilers can now produce a shared library
(with all the needed -ccopts/-ccobjs options) directly.
- With -dtypes, record (in .annot files) which function calls
are tail calls.
- All compiler error messages now include a file name and location.
- Optimized compilation of "lazy e" when the argument "e" is
already evaluated.
- Optimized compilation of equality tests with a variant constant constructor.
- The -dllib options recorded in libraries are no longer ignored when
-use_runtime or -use_prims is used (unless -no_auto_link is
explicitly used).
- Check that at most one of -pack, -a, -shared, -c, -output-obj is
given on the command line.
- Optimized compilation of private types as regular manifest types
(e.g. abbreviation to float, float array or record types with only
float fields).

Native-code compiler:
- A new option "-shared" to produce a plugin that can be dynamically
loaded with the native version of Dynlink.
- A new option "-nodynlink" to enable optimizations valid only for code
that is never dynlinked (no-op except for AMD64).
- More aggressive unboxing of floats and boxed integers.
- Can select with assembler and asm options to use at configuration time.

Run-time system:
- Changes in freelist management to reduce fragmentation.
- New implementation of the page table describing the heap (a sparse
hashtable replaces a dense bitvector), fixes issues with address
space randomization on 64-bit OS (PR#4448).
- New "generational" API for registering global memory roots with the GC,
enables faster scanning of global roots.
(The functions are caml_*_generational_global_root in .)
- New function "caml_raise_with_args" to raise an exception with several
arguments from C.
- Changes in implementation of dynamic linking of C code:
under Win32, use Alain Frisch's flexdll implementation of the dlopen
API; under MacOSX, use dlopen API instead of MacOSX bundle API.

Standard library:
- Parsing library: new function "set_trace" to programmatically turn
on or off the printing of a trace during parsing.
- Printexc library: new functions "print_backtrace" and "get_backtrace"
to obtain a stack backtrace of the most recently raised exception.
New function "record_backtrace" to turn the exception backtrace mechanism
on or off from within a program.
- Scanf library: debunking of meta format implementation;
fscanf behaviour revisited: only one input buffer is allocated for any
given input channel;
the %n conversion does not count a lookahead character as read.

Other libraries:
- Dynlink: on some platforms, the Dynlink library is now available in
native code. The boolean Dynlink.is_native allows the program to
know whether it has been compiled in bytecode or in native code.
- Bigarrays: added "unsafe_get" and "unsafe_set"
(non-bound-checking versions of "get" and "set").
- Bigarrays: removed limitation "array dimension - Labltk: added support for TK 8.5.
- Num: added conversions between big_int and int32, nativeint, int64.
More efficient implementation of Num.quo_num and Num.mod_num.
- Threads: improved efficiency of mutex and condition variable operations;
improved interaction with Unix.fork (PR#4577).
- Unix: added getsockopt_error returning type Unix.error.
Added support for TCP_NODELAY and IPV6_ONLY socket options.
- Win32 Unix: "select" now supports all kinds of file descriptors.

Tools:
- ocamldebug now supported under Windows (MSVC and Mingw ports),
but without the replay feature. (Contributed by Sylvain Le Gall
at OCamlCore with support from Lexifi.)
- ocamldoc: new option -no-module-constraint-filter to include functions
hidden by signature constraint in documentation.
- ocamlmklib and ocamldep.opt now available under Windows ports.
- ocamlmklib no longer supports the -implib option.
- ocamlnat: an experimental native toplevel (not built by default).

Bug fixes:
- Major GC and heap compaction: fixed bug involving lazy values and
out-of-heap pointers.
- PR#3915: updated some man pages.
- PR#4261: type-checking of recursive modules
- PR#4308: better stack backtraces for "spontaneous" exceptions such as
Stack_overflow, Out_of_memory, etc.
- PR#4338: Str.global_substitute, Str.global_replace and the Str.*split*
functions are now tail-recursive.
- PR#4503: fixed bug in classify_float on ARM.
- PR#4512: type-checking of recursive modules
- PR#4517: crash in ocamllex-generated lexers.
- PR#4542: problem with return value of Unix.nice.
- PR#4557: type-checking of recursive modules.
- PR#4562: strange %n semantics in scanf.
- PR#4564: add note "stack is not executable" to object files generated by
ocamlopt (Linux/x86, Linux/AMD64).
- PR#4566: bug in Ratio.approx_ratio_fix and Num.approx_num_fix.
- PR#4582: weird behaviour of String.index_from and String.rindex_from.
- PR#4583: stack overflow in "ocamlopt -g" during closure conversion pass.
- PR#4585: ocamldoc and "val virtual" declarations.
- PR#4587: ocamldoc and escaped @ characters.
- PR#4605: Buffer.add_substitute was sometime wrong when target string had backslashes.
- PR#4614: Inconsistent declaration of CamlCBCmd in LabelTk library.

Now for some unfortunate news:

Native dynlink used to work on Mac OS X

The clean solution to make natdynlink work on recent Mac OS X systems (beside convincing Apple to support the old behavior of their linker in their new implementation) is to change OCaml's x86 backend so that it produces only PIC code (this has been done for the AMD64 port). I don't think there is currently any plan to work on that.

...

Ouch, this makes it almost a dead end for us. I can offer some time to help in this effort, working in the port, or providing feedback. The native dynlink and toplevel are, at least to me, the killer features in 3.11, but adding another hole for Mac OS X intel (in addition to not supporting x86_64) does not seem like the best choice for an increasingly popular architecture.

...

Well, we'd very much like to support native dynlink on OS X 10.5, but Apple is not helping in the least by crippling their linker compared with the one in 10.4. If anyone from Apple is on this list, feel free to contact us at caml-devel@... for more information on this regression.

So it seems like OCaml needs help along two dimensions: support for the X86_64 in general, and support for Position-Independent Code (PIC) in particular. At least on the PIC side, we can steal from the AMD64 port.

A Simon Peyton Jones interview as part of the series The A-Z of Programming Languages that Naomi Hamilton has been putting together. Posting this one to the front page, not because of any bias towards functional programming, so much as it stands on its own as interesting and insightful from the standpoint of programming language design and evolution.

To supplant established languages, even in the functional programming area, like Haskell or ML or Scheme, you have to build a language that’s not only intriguing and interesting, and enables people to write programs faster, but you also need an implementation that can handle full scale applications and has lots of libraries and can handle profilers and debuggers and graphical analyzers… there’s a whole eco-system that goes with a programming language, and it’s jolly hard work building that up.

Proving that particular methods within a code base are functionally pure - deterministic and side-effect free - would aid verification of security properties including function invertibility, reproducibility of computation, and safety of untrusted code execution. Until now it has not been possible to automatically prove a method is functionally pure within a high-level imperative language in wide use such as Java. We discuss a technique to prove that methods are functionally pure by writing programs in a subset of Java called Joe-E; a static verifier ensures that programs fall within the subset. In Joe-E, pure methods can be trivially recognized from their method signature.

The paper includes a nice discussion of security benefits that can stem from being able to identify pure functions (of course, it is not obvious that guarantees at the programming language level are maintained at the run time level). I am sure many here have opinions about whether it makes more sense to try to graft purity on an imperative language, exposing it as an added feature, or to move programmers to functional languages..

Here's a little light reading for your day-after-Labor-Day (or whatever yesterday was where you live): Unchecked Exceptions can be Strictly More Powerful than Call/CC, Mark Lillibridge and Olivier Danvy, 1999, Higher-Order and Symbolic Computation.

We demonstrate that in the context of statically-typed purely-functional lambda calculi without recursion, unchecked exceptions (e.g., SML exceptions) can be strictly more powerful than call/cc. More precisely, we prove that a natural extension of the simply-typed lambda calculus with unchecked exceptions is strictly more powerful than all known sound extensions of Girard’s Fω (a superset of the simply-typed lambda calculus) with call/cc. This result is established by showing that the first language is Turing complete while the later languages permit only a subset of the recursive functions to be written.

I have to say that on seeing the title I was surprised: I cut my functional teeth on Scheme and every baby Schemer sucks up the knowledge that call/cc lets you create all manner of flow control including exceptions. But, as the paper makes clear, that's not necessarily the case in a statically-typed context.

Edit: Citeseerx was not responding very well, here's an alternative URL for the paper.

As a follow up to the previous post, check out how Chung-chieh Shan applied regions to a seemingly unrelated problem. His post begins by explaining how automatic (numerical) partial differentiation can be implemented, and goes on to show how to use regions to avoid mixing-up the variables being differentiated.