Re: GSoC: Emacs Lisp support for GNU Guile

[Stefan Monnier]

> as already discussed briefly with the Guile guys behind the new VM thing,
> I got the idea to implement Emacs Lisp as supported language for the Guile
> VM system.

I won't have time to mentor it, but I'd like to point out some relevant
directions in Emacs's future: as some of you know, other than hacking on
Emacs and its weakly typed C code and dynamically typed Lisp code, my
day job revolves around static typing and type theory, which makes for
some frustrations.  But while thinking of how to integrate Miles's
lexical scoping branch, it occurred to me that it would be a good
opportunity to try and combine both lives: with modern type systems (as
seen in Coq, Agda, TSCB, and friends), we can easily accomodate any
valid Lisp code.  While the plan is not fully fledged out yet, I've been
talking to Richard and Chong about it and we'll probably end up using
a variant of Agda's type system in Emacs-24: the code should be 100%
backward compatible, except that to take advantage of the newer features
(like closures, unboxed values, tail recursion, ...), you might need to
add a few simple type annotations at key places, like:

   (defun append (l1 l2)
     (declare (type _∷_ <↓> x ⊛ sequence Γ))
     (if (null l1)
         (withtype l2 ∃ \i -> sequence (i ⊕ (1 + max bal)))
       (cons (car l1) (append (cdr l1) l2))))

As I said, it's not fully fledged out, so take the above example with
a grain of salt.  I didn't really want to talk about it in public yet,
but figured that maybe now would be the right time after all, especially
since Guile people might be interested in it as well.


        Stefan