Lambda the Ultimate

Hi,

I am writing a Lisp->JavaScript compiler (link), and I am at the point where I want to add defmacro to the language, so that higher-level, convenient operators like let can be added to the language in terms of simpler, core forms.

The boostrap problem is this: the macro bodies need a sizable portion of the language as support code (e.g. AST objects, collections, map, other utilities...), but I don't want to write that part of the language without the convenient operators afforded by macros.

I see a couple of possible solutions:

1. Add a non-turing-complete macro system (e.g. syntax-rules), and write the convenience macros in that system;
2. Write the convenience macros as built-ins in the compiler's host language;
3. Use some kind of external tool, e.g. pipe my S-expressions through a Scheme and utilize its macro system;
4. Bite the bullet and write the defmacro support code without the convenience macros.

Any suggestions? Thanks,

-- Manuel

Lengrand & Miquel (2008). Classical Fω, orthogonality and symmetric candidates. Annals of Pure and Applied Logic 153:3-20.

We present a version of system Fω, called Fω^C, in which the layer of type
constructors is essentially the traditional one of Fω, whereas provability
of types is classical. The proof-term calculus accounting for the classical
reasoning is a variant of Barbanera and Berardi’s symmetric λ-calculus.
We prove that the whole calculus is strongly normalising. For the
layer of type constructors, we use Tait and Girard’s reducibility method
combined with orthogonality techniques. For the (classical) layer of terms,
we use Barbanera and Berardi’s method based on a symmetric notion of
reducibility candidate. We prove that orthogonality does not capture the
fixpoint construction of symmetric candidates.

We establish the consistency of Fω^C, and relate the calculus to the
traditional system Fω, also when the latter is extended with axioms for
classical logic.

I'm trying to assess several dependently typed languages/platforms in order to select one for a project which is to create a type-level DSEL for reasoning with quite simple formal systems. I began with the intention of doing this in Haskell+GHC extensions, emulating the types I need but I no longer think that will work for me, or rather it may be possible but is a square peg in a round hole...

I'm starting to look at Coq, Agda & Epigram by working through tutorials and putting together some code, and as far as I can see any of these would be sufficient for the task. It's obvious that there are big differences in scope between Coq and the other two on the list. A proof assistant not a programming language, although it's capable of being used as one, by far the most mature, lots of resources, extraction to Haskell/ML...

Can anyone give me a comparison of these and similar systems (Dependent ML? YNot?) w.r.t. their type systems and other capabilities? I'd also like to hear thoughts on their relative maturity, whether you think that should matter very much to me, learning curve, etc?

Thanks!

Chuck Thacker is building a new research computer called the BEE3.

There was a time, years ago, when computer architecture was a most exciting area to explore. Talented, young computer scientists labored on the digital frontier to devise the optimal design, structure, and implementation of computer systems. The crux of that work led directly to the PC revolution from which hundreds of millions benefit today. Computer architecture was sexy.

These days? Not so much. But Chuck Thacker aims to change that.

To understand the importance of such machines in computing history remember what Alan Kay says of the predecessor used to develop Smalltalk at Xerox PARC:

We invented the Alto and it allowed us to do things that weren’t commercially viable until the 80’s. A research computer is two cubic feet of the fastest computing on the planet. You make it, then you figure out what to do with it. How do you program it? That’s your job! Because real thinking takes a long time, you have to give yourself room to do your thinking. One way to buy time is to use systems not available to most people.

I want one!