cdiggins.com

Well I’m going to drop off the radar for about 10 days, because I’m driving across America, moving from Seattle to Montreal. It doesn’t look like I am going to be able to make any release before I leave. In general though things are looking very promising, I am now achieving pretty good test coverage with the most recent type system. I still have some problems identifying bound variables in edge cases, though I think I know what I am doing wrong. The current development version of the type reconstructor and constraint solver are accesible online at http://cat-language.googlecode.com/svn/trunk/ in the files http://cat-language.googlecode.com/svn/trunk/CatTypeReconstructor.cs and http://cat-language.googlecode.com/svn/trunk/ConstraintSolver.cs .

 I have had some big help from Luca Cardelli’s paper Basic Polymorphic Typechecking ( http://research.microsoft.com/Users/luca/Papers/BasicTypechecking.pdf ). For those of you implementing type systems I strongly recommend that paper. I could never explain things more eloquently than he does. However, let me point out that Luca calls bound type variables “generic” variable and free type variables “non-generic” variables. This is a little non-standard, but to be honest I think it is easier to grasp. I am torn between the two different names in my code, and I keep oscillating between the two (though in the end I think I will end up using “free” and “bound”).

What I find a little mysterious about the type checking literature I have read is that no one has really stated the obvious thing: implementing a type system is very similar to writing a Prolog interpreter. Manfred von Thun was the only person I’ve heard make that connection, and it has proven to be an immensely helpful observation.

P.S.

Luca Cardelli is one of my heroes in the field of computer science. He has an uncanny ability for adding clarity to advanced concepts while maintaining precision and technical accuracy. I can’t recommend his papers enough, too bad all computer scientists didn’t write like he does.

I knew for a while that the problems I was having with the Cat type system were related to the identification of free and bound type variables, but for some reason the solution eluded me. I created several different just slightly broken versions of the type inference engine, but for type inference close is just not good enough (when I say close, I was literally passing over 99% of over 200 unit tests).

Well I finally realize that the problem could be easily avoided by using a lambda lifting algorithm (I regret having to link to Wikipedia, but in this case it is one of the most lucid explanations I could find). Essentially you convert all function types so that all type and type vector variables are bound. This simplifies everything greatly. Afterward whenever you copy a function type (say because it is equal to a type variable which has been duplicated), you then have to make sure you create new names for all variables, and add those new names as constraints to the constraint list.

After that everything should be easy as pie, assuming you know how to write a type inference engine. ;-)

If you are interested in learning how to write a type-inference engine (a.k.a type reconstruction algorithm), I suggest getting Benjamin Pierce’s book: Types and Programming Languages.

When Simon Peyton Jones said that he bowed down to Butler Lampson in a recent Channel-9 interview ( http://channel9.msdn.com/Showpost.aspx?postid=326762 ) it piqued my curiosity because I wasn’t familiar with him. When I found a link to a list of systems he worked on ( http://research.microsoft.com/lampson/Systems.html ) I was shocked I hadn’t heard of him before, this fellow’s credentials are unbelievable!

I also read a very interesting and insightful little slide-deck on his site at http://research.microsoft.com/lampson/Slides/GoldAndFoolsGoldAbstract.htm , amongst many others which I have yet had a chance to peruse. What intrigued me about thos slides is how some of his ideas ran contrary to today’s popular thinking about programming (not that I place any real value on popular ideas).  

Butler’s slides are simple and to-the-point observations of the reality of the last 50 years of software development, from a true software engineer’s perspective.

Now that I am writing more serious code using Cat (I started work on a parsing library), I am confronted with the desperate need for code management tools. I’ve started work on visual code manipulation tools which will be integrated into the next version of Cat. Here is a screen shot of a colorized Code Viewer:

The plan is to provide not a full IDE but instead a set of tools integrated with the interpeter for editing and manipulating code visually. The code viewer will provide access to some dialog based editing of functions (currently under development), but itself is not an editor. I’ll be able to offer more features in a shorter time frame this way. I’m hoping that when people get access to the source code, they will be inspired to implement more sophisticated tools themselves.

The upcoming version of Cat also has built-in support for unit-testing. Notice the tests in the meta-comments for “bury”, they can be run from the interpreter by simply writing ”[bury] #test”. You can automatically test every command loaded using “#testall”.

I’ll have a release of this version this week which I’ll call 0.17, but it won’t have all of the features that I promised for the end of August. In short what is still missing is homogeneous types, and full object types. At least the new type system can finally handle “[1] dup” properly! Now if I only I could figure out why the classical combinators were failing (SKK, etc.) :-(

I am hard at work on version 0.17, but because of some subtle but particularly nasty bugs in the type system requiring a full rewrite, and an impending move across North America from Redmond, Washington to Montreal, Quebec, I don’t expect to release version 0.17 until late August. I’m also writing a introductory programming textbook which is horribly time consuming.

Amongst a hopefully fully functioning type system, the major new features expected in the 0.17 release include object types, and statically typed homogeneous lists.

Another small but important feature is the new meta-comment system. Technically it is a kind of a cross between meta-data and comments. This will slow down the release because I have to complete a meta-comment parser and move all of my documentation and tests to the new system. 

Here is a sneak-peak at the new format for meta-comments expected in version 0.17

define repeat : (’A (’A -> ‘A) int -> ‘A)
{{
  desc:
    Executes a loop a fixed number of times
  semantics
    $A [$B] $c repeat == $A $c eqz [] [$B $c dec] if
}}
{
  swap            // ‘A int [body]
  [dip dec] bind  // ‘A int [[body] dip dec]
  [neqz] while pop
}

define whilen : (’A (’A -> ‘A bool) (’A bool -> ‘A) -> ‘A)
{{
  desc:
    Executes a while loop, while a condition is not true
  semantics:
    $A [$B] [$C] whilen == $A $C not [$B [$B][$C] whilen] [] if
}}
{ [not] compose while }

define whilene : (’A list (’A list -> ‘A list) -> ‘A)
{{
  desc:
    Executes a function while the list on the top of the stack is not empty
  semantics:
    $A $b [$C] whilene == $A $b empty not [$C [$C] whilene] [pop] if
}}
{ [empty] whilen pop }

define whilenz : (’A int (’A int -> ‘A int) -> ‘A)
{{
  desc:
    Executes a function while the value on the top of the stack is not equal to zero.
  semantics:
    $A $b [$C] whilenz == $A $b neqz [$C [$C] whilenz] [pop] if
}}
{ [neqz] while pop }

define for_each : (’A list (’A list any -> ‘A list) -> ‘A)
{{
  desc:
    executes function with each item in the list
  semantics:
    $A $b [$C] for_each == $A $b empty not [uncons pop [$C] for_each] [pop] if }
}}
{ [dip] bind [uncons swap] rcompose whilene pop } 

Notice that there are now five indicies of the meaning of each function:

• the name
• a type signature
• a description
• a semantics
• the implementation

Now hopefully this is sufficient information for readers to figure out precisely what each function does, and how it does it (and identify bugs). I’d appreciate some feedback on this new documentation approach to the library.

At the moment am testing Cat on some real-world problems by building a parsing and tree library from scratch. I am trying to get prepared for the ICFP contest, though I am feeling somewhat pessimistic. Mind you, I do have the luxury of hacking the language as I go! :-)

From the Wikipedia entry on lambda calculus.

“Lambda calculus can be called the smallest universal programming language.”.

You could call it that I suppose, but then you would be wrong. Languages such as Iota and Jot by Chris Barker are universal programming languages and are by any measures far simpler than the Lambda calculus.

I just thought I’d set the record straight.

The following is from a new proposal for the format of metadata in Cat that I posted recently to the Cat mailing list:

define dip : ('A 'b ('A -> 'C) -> 'C 'b)
{{
  summary pops an item
  semantics [$B] $a dip == $B $a
  test
    usage 1 [2] dip
    expected 2 1
    result 2 1
  test
    usage 1 2 [[3] dip] dip
    expected 3 1 2
    result 3 1 2
  history
    created
      by Christoper
      on 7/13/2006
    modified
      by Christopher
      on 7/13/2006
{
  swap quote compose apply
}

I would really appreciate hearing people’s comments and suggestions.

I might as well let the Cat out of the bag, Frank Krueger and I plan on entering the 2007 ICFP contest, using Cat of course. Our team is known as the “Cat’s Meow”.

I was very confused by the Johan Jeuring’s July 6th blog post titled “Feyeneyete Loop” until it dawned on me to drop the e’s. This leaves us with ”fynyt loop”, which prounced phonetically is “finite loop”. I doubt that this is simple coincidence. The “8″ is still a bit mysterious to me, but I suspect it is a symbolic representation of some kind of “loop” construct.

I know that historically the ICFP loves turing machines, automatons, and languages, so I suspect our little alien friend speaks some kind of turing language.

Very interesting stuff!

I have had to rewrite the entire Cat type reconstruction algorithm (i.e. inference engine) from scratch. The problem I encountered was surprisingly subtle, and was uncovered by Colin Hirsch. When I write: [[1] dup] the type is mistakenly reported as:

( -> (’A -> ‘A int) (’A -> ‘A int)

At first this looks right, but the problem is that ‘A is a free variable in each child function. This leads the type checker  is lead to believe that both instances of ‘A are the same, when in fact they are different. The solution is to rename instances of free variables. The unfortunate problem is that identifying and tracking free variables during the unification process is tricky.

I have come up with many incomplete hacks to try and address the problem, and the current version of Cat (0.16) comes close to doing the right thing. However, since I was not properly tracking which variables are bound and which ones are free, it still can’t handle a couple of classical combinators correctly. This is unfortunately not good enough, so I’m in the middle of a rewrite of the type reconstruction algorithm. It is hopefully going to allow me in version 0.17 handle the entire SK calculus without a hitch.

 The advantage of doing the rewrite is that the new code is more compact, easier to understand, and more efficient. Hopefully the finished type inference engine will be useful as a blueprint for others interested in implementing type reconstruction in their languages.

I believe the Scsh Reference Manual has possibly the best acknowledgements section ever written.