Lambda the Ultimate

An interesting writeup of the GC techniques used in DrScheme.

3m [the newer "moving memory manager"] definitely works better than [the current] CGC for SirMail, and in principle it should always work at least as well as CGC. Despite having a 3m that works well enough for SirMail for many years, however, we have not yet switched to it as the main build.

Quite interesting for those interested in implementation techniques or using DrScheme. Since GC seems to be a hot topic in the forum these day, I suspect many will want to check this out.

Securing the .NET Programming Model. Andrew J. Kennedy.

The security of the .NET programming model is studied from the standpoint of fully abstract compilation of C#. A number of failures of full abstraction are identified, and fixes described. The most serious problems have recently been fixed for version 2.0 of the .NET Common Language Runtime.

This is highly amusing stuff, of course. Some choice quotes:

if source-language compilation is not fully abstract, then there exist contexts (think ‘attackers’) in the target language that can observably distinguish two program fragments not distinguishable by source contexts. Such abstraction holes can sometimes be turned into security holes: if the author of a library has reasoned about the behaviour of his code by considering only source-level contexts (i.e. other components written in the same source language), then it may be possible to construct a component in the target language which provokes unexpected and damaging behaviour.

One could argue that full abstraction is just a nicety; programmers don’t really reason about observations, program contexts, and all that, do they? Well, actually, I would like to argue that they do. At least, expert programmers...

"A C# programmer can reason about the security properties of component A by considering the behaviour of another component B written in C# that “attacks” A through its public API." -
This can only be achieved if compilation is fully abstract.

To see the six problems identified by thinking about full abstraction you'll have to go read the paper...

Since we've been discussing hybrid type checking, dependent types, etc. recently...

Sage

Sage is a prototype functional programming language designed to provide high-coverage checking of expressive program specifications (types). Sage allows a programmer to specify not only simple types such as "Integers" and "Strings" but also arbitrary refinements from simple ranges such as "Positive Integers" to data structures with complex invariants such as "Balanced binary search trees." In addition to featuring these predicates upon types, Sage merges the syntactic categories of types and terms, in the spirit of Pure Type Systems, to express dependent types such as that of the infamous printf function.

Sage performs hybrid type checking of these specifications, proving or refuting as much as possible statically, and inserting runtime checks otherwise. For the complete details of the theory and empirical results, we direct you to the technical report.

I was going to post this to the front page, but it's already a Forum Topic. So go there to read about a preprocessor that adds continuations to JavaScript by transforming to CPS (I think).

Erlang/OTP R11B has now been released with support for transparently scheduling Erlang processes across multiple CPUs.

Congratulations to the OTP and HiPE teams and to Tony Rogvall for making this a reality!

Building Interpreters by Composing Monads

We exhibit a set of functions coded in
Haskell that can be used as building blocks to construct
a variety of interpreters for Lisp-like languages. The
building blocks are joined merely through functional
composition. Each building block contributes code to
support a specific feature, such as numbers, continuations,
functions calls, or nondeterminism. The result of
composing some number of building blocks is a parser,
an interpreter, and a printer that support exactly the
expression forms and data types needed for the combined
set of features, and no more.
The data structures are organized as pseudomonads,
a generalization of monads that allows composition.
Functional composition of the building blocks implies
type composition of the relevant pseudomonads.

So actually it is about building interpreters by composing pseudomonads.

PS: I stumbled upon this paper while trying to factor an interpreter into a set of features (and yes, I tried to package them as monads).
After a day of fighting with undecidable instances and rigid type variables I gave up and started googling - well, I was trying to invent a wheel.
Any comments on how pseudomonads relate to arrows (and other generalizations of monads) are appreciated.

What I find most interesting here is that the difference between yield and "inline" is this negligible, which explains why Ruby users are so enamored with the feature.

That stated, the runtime wonk in me would love for some Ruby expert out there to explain the underlying reasons why yield is so much faster than Proc.call.

I can guess, but I'd rather be told.

Don Box does some experimenting...

HashCaml

Peter Sewell and crew follow up on their work on Acute:

In this paper we put these ideas into practice, describing the HashCaml extension to the OCaml bytecode compiler, which supports type-safe and abstraction-safe marshalling, together with related naming constructs. Our contribution is threefold: (1) We show how to define globally meaningful runtime type names for key OCaml type constructs that were not covered in our previous work, dealing with the generativity issues involved: user-defined variant and record types, substructures, functors, arbitrary ascription, separate compilation, and external C functions. (2) We support marshalling within polymorphic functions by type-passing, requiring us to build compositional runtime type names and revisit the OCaml relaxed value restriction. We show that with typed marshalling one must fall back to the SML97 value restriction. (3) We show how the above can be implemented with reasonable performance as an unintrusive modification to the existing OCaml language, implementation, and standard libraries. An alpha release of HashCaml, capable of bootstrapping itself, is available, along with an example type-safe distributed communication library written in the language.

I was just getting all depressed realizing that I'd probably have to write a syntax extension in camlp4 to get reflection out of O'Caml. Then I discovered that someone just did recently. This serves both as a practical implementation of reflection for a statically-typed language and as a showcase for O'Caml/camlp4's ability to define new syntax.

A Monadic Semantics for Core Curry

The structure of our semantics sheds some light on how the basic components
of the language interact. In particular, we can see that the addition
of non-determinism, logic variables and narrowing can be accomplished just
by making a suitable shift in interpretation monad. We could emphasize
this modularity further by presenting the relevant monads as compositions of
monad transformers.

While being primarily an "interpreter as semantics" paper, it looks like a nice example of a DSL in Haskell.

As a bonus, it also discusses some features of logic programming.