Interpret haskell within haskell.

[Lauri Alanko]

On Fri, Dec 20, 2002 at 01:43:07PM +0100, Frank Atanassow wrote:
> There is quite a bit of work on staged evalution, metaprogramming,
> quasiquotation, reflection and run-time code generation in typed and ML-like
> languages. It's a very active and, IMO, promising area of research.

Yes. Thanks for the references, some of them I hadn't been acquainted with.

I was already aware of MetaML, but I had mostly thought of it as a
sophisticated macro system. But of course if you defer some stages until
"runtime" you essentially get _some_ form of eval.

After quickly skimming through some of these papers, it seems that they
aren't really after the same thing as I am. Template Haskell is explicitly
a macro system, and MetaML seems to be designed for partial evaluation so
that even at the first stage (in the source code) we have _some_ idea of the
structure of the code that is to be generated. Specifically, it seems that
there is no way to dynamically generate identifiers from strings, and I
guess this makes real evaluation of arbitrary input impossible.

Staged computation is very interesting in its own right, but I'm after
something different. I don't really want eval as a language construct, I
want a language that makes it possible to _implement_ eval, among other
things.

Let's take Scheme for an example. R5RS Scheme includes eval, but by itself
it's not particularly interesting. An interpreter for a language is just a
program, after all, and a full scheme evaluator can be implemented in a
couple of hundred lines. So there's nothing magic about this:

(eval '(letrec ((fact (lambda (x) (if (zero? x) 1 (* x (fact (- x 1)))))))
         (fact 5))
      (scheme-report-environment 5))
==> 120

The magic is _here_:

(begin (define a 5) (eval '(set! a (+ a 1)) (interaction-environment)) a)
==> 6

Here (interaction-enviroment) is a run-time representation of the
compile-time environment. It makes possible two-way interaction between the
stages. Essentially, first-class environments are all the magic you need to
implement eval.

So what I'm looking for is adapting first-class environments, as well as
other forms of reflection that are found in lisps, Smalltalk, Java, and
other untyped languages, to static typing. And I want to do it properly with
minimal run-time checking:

eval :: Pi t . String -> Env -> Maybe t

Here "t" is an explicit run-time type parameter, and 'eval t s e' returns
'Just x' if 's' represents a well-formed expression that can be assigned
type 't' in the environment 'e' and reduces to 'x'.

There are lots of other issues, of course. But the point is that I'm not so
much interested in code-generation mechanisms but rather in how to reify
compile-time information on the program as run-time objects.

Optimally, I'd like a system that allows the definition of new types at
runtime and possibly even gradual hot-swapping of the entire codebase of the
program. All with type-safety.

So is there any research on this sort of thing?

(This isn't really Haskell-specific, so this is probably somewhat off-topic
for haskell-cafe. Sorry about that, but I don't really know of a better
place to discuss this. When I tried to query about this on the Types forum,
the moderator rejected my posting as "too rambling", which was of course
perfectly accurate :). I haven't yet managed to write up a more lucid
exposition of the issue...)


Lauri Alanko
la@iki.fi