Log 123009

Various issues: Alpha conversion now in place, trivial. Linker bugs, or rather, failures to provide good errors, when not supplying all the object files. (I use a transform to bind to definitions. If an actual is defined, it becomes a call, otherwise, it becomes a name. I.e. supply the wrong set of modules, and I generate open LC terms.)

It probably wasn't even a substitution bug, but, I feel a lot more comfortable with alpha conversion in place.

First syntax change I'll make when ready: add 'fi.' Just read up on some Ada, I am convinced.

123009: Two flaws: 1) Flattening selects/methods may have an arity bug - not sure. 2) Processing applications to thunks has a bug - confirmed. It's almost the same bug...
123009: Stuck. Did I now do the exception handling wrong... or not?
123009: It's something else...
123009: Looking at the wrong places. Select is ok, exception is ok, it's just the thunk bug - missing 'apply' remove.

Rusty

All operational semantics preserving translations should be easily expressed with the 'thunkification' trick, i.e. 'shuffling' redexes which evaluate first under one strategy to a place where they will evaluate first under another strategy. Wonder why this took me more than fifteen minutes, actually...

Christmas Kōan LCi 1001

Two hands clap and there is a sound. What is the sound of one hand?
— Hakuin Ekaku


"...in the beginning a monk first thinks a kōan is an inert object upon which to focus attention; after a long period of consecutive repetition, one realizes that the kōan is also a dynamic activity, the very activity of seeking an answer to the kōan. The kōan is both the object being sought and the relentless seeking itself. In a kōan, the self sees the self not directly but under the guise of the kōan...When one realizes ("makes real") this identity, then two hands have become one. The practitioner becomes the kōan that he or she is trying to understand. That is the sound of one hand." — G. Victor Sogen Hori, Translating the Zen Phrase Book

Of course, you could try a naive translation of LCi to LC such that the resulting term is a list of calls made.

But under the most naive encoding, some terms might reduce under all rewrite strategies to the same term, i.e. superficially make the same calls in exactly the same order, and you still wouldn't know anything about the exact temporal behaviour. I just need observational equivalence on traces of rewrites of terms under an evaluation strategy.

It always boils down to the same observation: Value doesn't equal behaviour.

Right...

Compiled all sources to object files, and ended up with a substitution bug while linking... In a compiler, you really end up paying for each wrong decision.

As mentioned earlier, I thought I could cheat my way around alpha-conversion for performance reasons. The result: bugs. No way around it, I'll add it. I am rereading all my functions on my intermediate LC and adding comments/replacing them with the standard definitions.

I have the tendency to use blogs as scratch pads for half thoughts. It becomes a mess, I cleaned up some posts.

Boehm-Demers-Weiser = Borg?

Strange, I thought it would be nice if I would add bindings to gc.h. But after thinking it over, what would happen: When garbage collecting the Boehm collector would travel the whole Hi heap looking for references to nodes allocated in the Boehm heap. So it might not be worth to have my own Cheney collector running in parallel with Boehm, even if faster?

Log 122709

I turned off the typechecker in order to get the C bootstrap to compile itself. The OCaml compiler compiles to a term which is evaluated by a simple small-step evaluator on a stack of closures, it can't handle deeply nested evaluations.[1] I need to know whether it's able to compile itself, otherwise I'll need to backport the C back-end to the ML compiler. Guess I'll start on unit tests again. It's actually quite hard to derive unit tests for interfaces. Going to check Haskell on that, my interfaces are essentially type classes on type constructors, so the difference shouldn't be that big.

[1] Not ideal, but OCaml runs out of stack space easily. So, I build an explicit evaluator on a stack. Which is correct, but naive, it allocates 1Gb on some of the bigger files. The rewriter is pretty naive, and uses some unknown fact that the semantics of eager LC can be expressed on just a stack of closures, whereas most publications use some three tuple of a stack and some other stuff.

Two Thoughts

I posted a mail about an impure calculus. Now the question would be: Why would one be interested in that? The answer is rather trivial.

Even pure programming languages, like Haskell and Clean, compile to side-effecting programs, even when they carefully try to hide that. The underlying semantics of a functional program is, without being too pompous about it, therefore best expressed in an impure calculus. Ideally with a corresponding operational semantics, since that is what programs do: They have run-time behaviour.[1][2][3]

Now, the reason why am I interested in lazy calculi: I want mostly eager behaviour -I like predictability,- but at some points I want laziness for it's expressiveness. For example, one really nice thing about Haskell is that equivalence of, say, the contents of two trees may be determined by lazily unfolding them to two lists and checking those lists for equality. This is hard to program in a language with eager semantics. I was wondering if I could `cheat` my way around this problem and settle on a semantics in the middle of lazy and eager behaviour, the language seems to be eager, but, under water, when side-effect free, the language is essentially lazy. I.e., when dealing with pure functions/data, evaluation is lazy.

No idea whether the latter is achievable. Guess not, though Haskell proves otherwise. Rephrasing: Not as easily as I want it - with this semantics I'll end up with an impure Haskell variant. Worst of both worlds.

^[1] Black addendum: And if I read one more paper which thinks it'll contribute anything interesting to compiler technology by chasing arrows, I'll puke, and see it as an outright failure of fundamental CS to get anything right.
^[2]I am referring to compiler/code-generation techniques here, not top-level type-theoretical concerns.
^[3]An ideal compiler for a pure lazy language would compile superficially effect-free programs down to lazy side-effecting terms to eager side-effecting terms to imperative code. Then again, ideals don't work, and it seems it has been investigated anyway. Though this might almost exactly be what GHC does these days.

Rephrasing Thunks

Assume a lambda calculus with side effects/impure function calls:

   M ::= c | v | \v . M | (M M) | call c

An example term: (\x. \y. call (+) x y) 2 3.

The operational semantics of a term is the series of calls made to the system during the evaluation under a certain rewrite strategy. Two terms evaluated under two rewrite strategies are considered operationally equal if they made exactly the same calls in exactly the same order.

The standard naive technique for transforming a call-by-need term to a call-by-value term is called thunkification:

1. An abstraction \x.e translates into \x.T(e);
2. An application (e1 e2) translates into T(e1)(\x.T(e2 )), where x is a fresh variable.
   That is, the evaluation of the argument is suspended (thunkified);
3. A variable x translates into (x d) (where d is a dummy argument)
   Thus, x is bound to a suspension and x must be dethunkified.

I suspect that for this impure calculus, it is sufficient to thunkify lazy terms and optimize the corresponding term according to partial evaluation under a call-by-value semantics. Possibly, arguments to calls can be fully reduced by just supplying them their dummy argument, forcing evaluation. That would make strictness analysis superfluous, I wonder what I missed here?

It seems trivial, but it probably isn't. I have the feeling that there is a generalizing pattern if you would supply operational semantics preserving functions between the two/four mostly known reduction strategies, with the addendum that for impure LC, you might need to 'patch' rewriting such that all calls receive fully reduced terms to mimic behaviour of 'real' down-to-earth programming languages, or assume all calls receive constants as arguments. Of course, translating call-by-need to call-by-value is the most obviously wanted function, but it might be worth it to study and prove correct those other semantic preserving functions in order to gain some better understanding in rewrite semantics for impure LC.

References:

1. Paul Steckler, Mitchell Wand, Selective Thunkification, Proceedings of the 1st International Static Analysis Symposium. 1994.
   ftp://ftp.ccs.neu.edu/pub/people/steck/sas94.ps.
2. Torben Amtoft, Minimal Thunkification, Proceedings of the Third International Workshop on Static Analysis WSA'93, volume 724 of Lecture Notes in Computer Science. 1993.
   http://www.daimi.aau.dk/~tamtoft/Papers/WSA93.ps.Z
   http://www.cis.ksu.edu/~tamtoft/Papers/Amt:MT-1993
3. Alan Mycroft, The theory of transforming call-by-need to call-by-value. International Symposium on Programming, Paris. 1980.

Operational Semantics Preserving Translations

Assume a lambda calculus (LCi) with side effects/impure function calls:

LCi ::= c | v | \v . LCi | (LCi LCi) | call LCi*

Note that * is a sequence of terms.

An example term: (\x. \y. call (+) x y) 2 3.

A call models an impure/non-referentially transparent system call. For simplicity, we assume that if two programs are run, and they have made identical calls, that any two new identical calls will return identical results.

I.e.: if two programs made (precisely) two calls to some function "tick" resulting in values 1 and 2, then the third call to tick will return the same value.

Assume the functions EAGER and LAZY, eager and lazy operational semantics for closed terms in LCi, respectively. They both map an LCi term into a value of type (LCi := call LCi*)* LCi, the collection of made calls in temporal order followed, possibly, by the term in strong normal form - fully reduced. I'll handwave termination concerns away for the time being. EAGER and LAZY are called the operational semantics since it tracks the system calls made and returns the evaluated term, if any. Note that I assume that a call only accepts an LCi term in strong normal form (fully reduced), and returns a term in strong normal form.

Examples:

EAGER((\x. \y. call (+) x y) 2 3) = (5 := call 2 3), 5.
During the evaluation of the term we made one call to +, returned 5, and the whole program reduces to 5.

and

EAGER( (\x . call tick) (call tick) ) = (1 := call tick), (2 := call tick), 2.
Two calls to tick returned constants 1 and 2, the whole program reduces to 2.

moreover

LAZY ( (\x. call (+) 2 3) (call tick) ) = (5 := call 2 3), 5.

whereas

EAGER ( (\x. call (+) 2 3) (call tick) ) = (1 := call tick), (5 := call 2 3), 5.

Two terms are assumed to be operationally equal if they made exactly the same systems calls in temporal order, and possibly reduce to the same term, BUT two identical terms may return a similar result under the two impure operational semantics, but are not equal since they didn't make the same series of system calls.

Needed: two functions e_to_l and l_to_e such that

EAGER(l) = LAZY(e_to_l l),
LAZY(l) = EAGER(l_to_e l), 
EAGER(l) = EAGER(l_to_e(e_to_l l)), and  
LAZY(l) = LAZY(e_to_l (l_to_e l)).

I.e., operational semantics preserving functions between eager and lazily evaluated impure LC terms where = is the alpha equivalence on series of terms.

Rationale: I want to implement some lazy features in Hi, this seems to be one good solution.

Moreover:

1. Say you would like to implement a Haskell compiler but you only have a Lisp compiler. Solution: translate Haskell to a corresponding LCi term l, translate that term to l' = l_to_e l, translate l' to Lisp. Hereby solving the problem once and for all.
2. Say you want to have eager semantics in Haskell. That could be done similarly with the e_to_l function.

I didn't think it through too much, a simple CPS transform probably doesn't do it, but may be a good starting point.

Funny thing is that this is a totally opposing view to normal interpretations of operational semantics of LC since I am only interested in observational equivalence with respect to side effects. Which makes sense for someone who builds compilers since the only interesting quality of a program is what it does to the system and the result is often uninteresting.

Log 122509

Solved all typing problems, typechecker seems to be correct, but slow. Rethinking the instance checks since the code seems to be too complex, hinting at bugs. It also generates errors on the wrong spots, which should be fixable easily. Bootstrap accepts 30% of its own source, after which it stalls for unknown reasons.

12/25/09: Its the quadratic time typechecker. I gather type constraints in a simple bottom up pass over the term. It introduces a large number of variables and equalities where for each equality a linear number of substitutions are made on the sequent. Moreover, instantiation constraints also introduce type unknowns. On large terms, the prover run by an ocaml interpreter just stalls. I discard type equalities, for now, from the antecedents which should, almost, halve the running time.

In the end, I want to decorate variables in the AST with their derived types. The running time should be fixable by the introduction of two type unknowns: those unknowns which should be remembered, and unknowns for intermediates, where the former are stored separately in the sequent. A nice to have for now.

On Generalizations

The bootstrap compiler has a more restrictive typechecker, basically because I implemented some cases better. Parts of the bootstrap compiler are therefore not accepted. Two problems, which basically boil down to generalization errors.

First -yeah I read the papers,- it assumed, mostly, that generalization is 'good' because of the following example:

let f = [x -> x] in (f 3, f 'a')

If we wouldn't generalize the type of f, it must be the identity on int and char, which fails to typecheck. The only problem: The example is not general, it never happens. Functions which are polymorphic are usually written as definitions, and almost never occur in function bodies.

What does happen is that we want to know in local functions what argument types to expect, such that subsequently we can optimize better, i.e.:

let g = [y -> print y] in g 3

If y has type int, then the generic function print may be optimized to print_int.

Moreover, and this seems to be a source of 'features,' it is hard to generalize in the right order. In the example below, it should be derived that z is a printable value.

f z = let x = [x -> x] in let g = [y -> print y] in g (f z)

Which fails, at the moment.

Which leaves me with two choices. After thinking it through, I derived that linear order solving handles almost all cases, so that's no problem. So, get rid of generalizations is one choice, get rid of the bug the other. Guess I'll stick with generalizations, even if problematic. (Can only generalize over local variables, pattern matching and generalization are a hard mix.)

I guess I forgot an equality somewhere, or forgot assigning some variables monomorphic...

12/23/09: A substitution on a set of monomorphic variables is the set of free-variables after substitution.

Towards a Top-Level Interpreter

I am looking at ways to build a top-level interactive interpreter. Best thing I can think of:

1. Compile a series of modules to a shared library.
2. Write an interpreter which compiles (untyped) expressions to thunks using libdl. A simple lambda to SKI to thunks compiler should be enough.
   
3. Evaluate thunks with the runtime.
   

Should do it. Needed: bindings of the runtime into the Hi language.

Log 122009

After a number of changes, some small, some large, the to ml compiled compiler accepts its own system file again. It also cleanly compiles simple programs to C (fac, list manipulations). Various thoughts:

1. I simplified the type checker to a prover using solely antecedents and consequents. Both are stored in a list, giving quadratic behavior. It should become O(n x log(n)) here.
2. In order to avoid quadratic, or worse, behavior I tried to avoid alpha conversion on lambda terms during substitution. There have been/are too many bugs because of that. Should solve this.
3. I don't inline yet. I should do this at some point.
   
4. The method invocations are compiled down to combinators. Case statements are a linear collection of tests, that means linear behavior on lookups. Not sure this is a problem actually.
5. Everything not essential graph rewriting is done through FFI (libffi) where all functions are loaded from dynamic libraries (libdl). Every FFI call is evaluated each time. FFI is slow already, I could/should add memoization here.
6. FFI calls are dynamic in nature leading to runtime failures when types are not matched. Should look into swig to automate the glue.
7. I should allow unary arguments to FFI, now it is assumed all FFI symbols refer to functions.
   
8. I wonder how combinators will work out long-time. There might be just too much copying - should think over how spurious copying can be avoided.
   
9. I need serialization. This should be simple and obvious if all data is treated as trees.
10. I started on a simple ReST parser for documentation which I intend to be part of the compiler.
11. I should prove the type system correct?

Explanation in order why I use FFI even for simple addition: This is probably the reverse of what one would expect since tradional compilers often optimize heavily on native types. But, to me, the order of requirements was: 1) fast graph rewriting, 2) good simple interfacing with C, and 3) reasonably fast compiler. Hence, I considered thinking about integers a waste of time, or, a nice to have.

Writing a compiler is

like pushing a giant wedding cake through a keyhole in the hope you end up with a camel.

Cheney

There's a bug in the garbage collector, somewhere I probably forget to decrease/increase a pointer. (I use a drop-in replacement for Boehm, so I do some pointer arithmetic to get to the meta-field of an allocated structure.)

It is unbelievable how much time it takes to debug one C routine of 50 lines.

[Fixed: returned wrong variable after copying.]