cdiggins.com

Ben Chambers has shared a new implementation of Cat written in Scheme at http://groups.google.com/group/catlanguage/files .

I was looking over the XACC IDE web site the other day thinking how that because it was written in C# that it would be easy to extend to support Cat, when much to my surprise after downloading it I found it already supported Cat! That made my day. The XACC IDE is very clean and elegant, and I think is an IDE with a lot of promise.

In other Cat IDE news I have been in discussions with Guillaume Cartier, the developer of Jazz Scheme about adding support for Cat into JEDI - the Jazz Scheme IDE. He showed me how to do it, I just have to hack a bunch of configuration files (and rebuild the “catalog” and a few other steps). JEDI is very special, because it is largely dynamically configurable and everything is written from the ground up in Jazz Scheme. Eventually it will be fully cross platform, because they don’t rely on Windows common controls (despite having a Windows look and feel). JEDI is one of the most powerful IDEs I have ever seen, because all of the code is exposed.

Finally I am still hoping Adrian Savage will make some bug fixees to his Eclipse plugin, the discussion and link can be found in this thread.

I’m looking at papers on compositional type systems. Here are some interesting papers:

A Typed, Compositional Logic for a Stack-Based Abstract Machine
by Nick Benton
June 2005
29 p.

PDF 226 Kb

We define a compositional program logic in the style of Floyd and Hoare for a simple, typed, stack-based abstract machine with unstructured control flow, global variables and mutually recursive procedure calls. Notable features of the logic include a careful treatment of auxiliary variables and quantification and the use of substructural typing to permit local, modular reasoning about program fragments. Semantic soundness is established using an interpretation of types and assertions defined by orthogonality with respect to sets of contexts.

Keywords: Hoare logic, bytecode

Link: http://research.microsoft.com/research/pubs/view.aspx?type=technical%20report&id=938

Discussion: http://lambda-the-ultimate.org/node/814  

The following paper seems to be independant:

Compositional type systems for stack-based low-level languages
by Ando Saabas and Tarmo Uustalu, appearing in Proceedings of the 12th Computing: The Australasian Theroy Symposium - 2006.

It is widely believed that low-level languages with jumps must be difficult to reason about by being inherently non-modular. We have recently argued that this in untrue and proposed a novel method for developing compositional natural semantics and Hoare logics for low-level languages and demonstrated its viability on the example of a simple low-level language with expressions (Saabas & Uustalu 2005). The central idea is to use the implicit structure of finite disjoint unions present in low-level code as an (ambiguous) phrase structure. Here we apply our method to a stack-based language and develop it further. We define a compositional natural semantics and Hoare logic for this language and go then on to show that, in addition to Hoare logics, one can also derive compositional type systems as weaker specification languages with the same method. We describe type systems for stack-error freedom and secure information flow.

Link: http://www.cs.ioc.ee/~ando/publications/cats06.pdf
Discussion: http://lambda-the-ultimate.org/node/2450#comment

Surprisingly a lot of people don’t realize that an imperative statement such as “a[i] = x” can be treated like pure functional code, if our array “a” is not shared.  It is simply a question of constructing a new array from the old one. This becomes very interesting, because then we can trivially translate imperative code into functional code:

tmp = a[i]; a[i] = a[j]; a[j] = tmp;

Of course, sometime in your language you are probably going to want to share objects. As soon as you explicitly share an object, you lose the property of functional purity because you introduce side-effects (changing an object in one expressions affects other expressions). So the question is, can we reduce or eliminate sharing? The answer is that to a certain degree we can, and more than most people realize.

The first thing to realize is that many assignments to or from local variable and arguments can actually be replaced with swaps or moves. This is not so obvious if you are looking at traditional assembly or bytecode, where everything is treated extremely imperatively. But consider the following byte-code:

 ldloc1; lodconst1; add; stloc1;

This is really common code, but it can be trivially replaced with a purely functional successor function: “[succ]” that is called on the right place on the stack, using “dipN”.

Another important idea is that most copy instructions can be replaced with move instructions. A copy implies either sharing or an actual copy (which can be quite expensive). Many copy instructions result from accessing elements in an array or other collection. One technique to reduce sharing is to replace array getters and setters with a “swap_at” instruction, that swaps an item on the stack, with an item in an array. This causes objects to be moved rather than copied. This way all copy instructions occur on the stack and are explicit, using “dup”. Now our goal simply becomes to reduce the number of “dup” instructions in the code. The “dup” instruction makes an explicit copy, and is going to be expensive. Some languages desire “share” instructions which copy a handle (or pointer) to an object. In such a case we have no choice but to replace the pure object with two impure handles. All functions that operate on these objects then get polluted: the impurity propagates.

So what I plan on doing is to use “dup” to make an explicit copy of an object, and to use “share” to replace an object with two handles. e.g.

   dup : (’a -> ‘a ‘a)
   share : (’a -> handle(’a) handle(’a))

Any function that we call that uses a handle then becomes impure, but at that point what can you do. The programmer has really forced your hand and is insistent on relying on side effects.  

I completely forgot I had written this profiler library in C++ which I had planned on submitting to Boost, at least until I got annoyed with the group, and of C++ programming in general. I hope someone finds it useful.

Things that have caught my eye and triggered my neurons this morning:

• Uniqueness Types - An elegant way to allow destructive semantics in a pure functional manner without the nastiness of monads
• Squeak on a Cell Phone - I am going to have to take a close look the Squeak VM. Related VMs I should also consider are the Slate VM and the Strongtalk VM.
• Bootstrapping Forth - I am going to have to look into bootstrapping Cat in a similar manner. It will help reveal cracks in the language, and the geek factor is pretty high as well.

Fellow language geeks, I found another blog that I like:”Thing that Amuse Me” which is Lennart Augustsson’s blog. Lennart’s home page is here, and he even has a wikipedia page.

This is the basis for a combinator based recursive descent parsing library in Scheme. It seems to work well so far but it disturbs me how few lines of code it is:

; parse rule r repeatedly until it fails
; always return true
(define (star r)
  (lambda () (if (r) ((star r)) #t)))  

; parse rule r repeated until it fails
; return true only if you parse successfully at least once
(define (plus r)
  (lambda () (if (r) ((star r)) #f)))  

; try to parse rule r once
; return true
(define (opt r)
  (lambda () (if (r) #t #t)))  

; parse rule r1, but if it fails try r2
; return false only if both rules fail
(define (choose r1 r2)
  (lambda () (if (not r1) (r2) #t)))  

; parse rule r1 then r2
; return true only if both rules succeed
(define (seq r1 r2)
   (backtracker (lambda () (if (r1) (r2) #f))))  

; returns true if rule parsing fails
; backtrack if successful
(define (not-at r)
  (lambda () (if ((backtracker r)) #f #t)))  

; Used to ... wait for it .... backtrack
(define (backtracker f)
  (lambda ()
    (let ((tmp input))
      (if (f) #t (begin (set! input tmp) #f)))))  

; sample input
; sorry to use global variables, but it too ugly otherwise
(define input '(0 0 1 0))  

; match something specific in the input
; eventually we will want to match ranges of things
(define (match x) (lambda () (if (null? input) #f
  (if (eq? (car input) x)
     (begin (set! input (cdr input)) #t) #f))))  

; This shows how rules can be combined to parse some stuff
(define (test) (seq (seq (star (match 0)) (match 2))
   (opt (match 0))))

There is another embedding of Cat in Haskell which I have posted to the Cat mailing list.

The mysterious Pied has posted an implementation of Cat in Haskell!