Rubrication

The following is some SML code that implements the natural numbers using peano arithmetic in the SML type system. These numbers can be used to protect access to list functions. I haven't yet figured out if addition is possible, but I'm hoping that it is. It could be really handy! signature SLIST = sig type 'a nat type Z type 'a S val S : 'a nat -> 'a S nat val P : 'a S nat -> 'a nat val Z : unit -> Z nat val zerop : 'a nat -> bool val toInt : 'a nat -> int type ('elt,'n) slist val snil : unit -> ('elt, Z nat) slist val scons : 'elt -> ('elt, 'n nat) slist -> ('elt, 'n S nat) slist val :+: : 'elt * ('elt, 'n nat) slist -> ('elt, 'n S nat) slist val shd : ('elt, 'n S nat) slist -> 'elt val stl : ('elt, 'n S nat) slist -> ('elt, 'n nat) slist val slen : ('elt, '...

I just got "ML for the working programmer" in the mail a few days ago, and worked through it at a breakneck pace since receiving it. It turns out that a lot of the stuff from the "Total Functional Programming" book is also in this one. Paulson goes through the use of structural recursion and extends the results by showing techniques for proving a large class of programs to be terminating. Work with co-algebras and bi-simulation didn't quite make it in, except for a brief mention about co-variant types leading to the possibility of a type: D := D → D which is the type of programs in the untyped lambda calculus, and hence liable to lead one into trouble. I have to say that having finished the book, this is the single most interesting programming book that I've read since "Paradigms of Artificial Intelligence Programming" and "Structure and Interpretation of Computer Programs". In fact, I would rate this one above the other...

Recently on Lambda the Ultimate there was a post called "Total Functional Programming".  The title didn't catch my eye particularly, but I tend to read the abstract of any paper that is posted there that doesn't sound terribly boring.  I've found that this is a fairly good strategy since I tend to get very few false positives this way and I'm too busy for false negatives. The paper touches directly and indirectly on subjects I've posted about here before.  The idea is basically to eschew the current dogma that programming languages should be Turing-complete, and run with the alternative to the end of supplying "Total Functional Programming" .  At first glance this might seem to be a paper aimed at "hair-shirt" wearing functional programming weenies.  My reading was somewhat different. Most hobbiest mathematicians have some passing familiarity with "Turing's Halting Problem" and the related "Goedel's Inco...

I just spent a couple of very cold weeks in Anchorage Alaska.  I went out with a bunch of friends to a bar on the night prior to leaving, where I met up with an old friend (and listened to two other friends play music).  I started describing the lambda calculus to him since it is related to my work and he was curious what I was up to.  In any case I found myself unable to produce addition of the church numerals off the top of my head, which I found pretty disturbing since it shows that I probably didn't quite understand it in the first place.  Therefor I sat down this morning to see if I couldn't reconstruct it from first principles.  It turns out that it is relatively easy. First, let us start with a bit of notation, and a description of the lambda calculus .  Since wikipedia describes the lambda calculus in detail, I'll just show how one procedes with calculations.  As examples let us start with the church numerals .  1 = (λf x.f x) 2 = (λf...

Probably one of the best papers I've read on the relationship between CBN, CBV and the Curry-Howard correspondance is the paper Call-by-value is dual to call-by-name by Wadler. The calculus he develops for describing the relationship shows an obvious schematic duality that is very visually appealing. After reading the paper that I mentioned earlier on Socially Responsive, Environmentally Friendly Logic (which shall henceforth be called SREF Logic), it struck me that it would be interesting to see what a CPS ( Continuation-passing Style ) like construction looks like in SREF logic, so I went back to the Wadler paper to see if I could figure out how to mimic the technique for multi-player logic. It looks like the formulation by Wadler comes out directly by thinking about logic as a two player game! I'm excited to see what happens with n-player logic. This has been a big diversion from what I'm actually suppose to be working on but I didn't want to forget about i...

Once again the internet comes to the rescue with a Systematic Search for Lambda Expressions .  This is the answer to yesterdays question of whether we can iterate over isomorphic proofs exhaustively in order to extract all programs of a specification which in this case is realised as a "type".  Hooray for computer science!

I have a bunch of ideas that I don't have time to follow up on but I'd like to retain in some fashion so here goes. 1. A long time ago I had a question about the shortest assembly program (parameterised by the instruction set of course!) that could encode the generators of the quaternions under multiplication. It is a very easy thing to program this, but as I was doing it, I found myself being highly doubtful that I was choosing the "right" encoding. In fact I almost certainly wasn't. Would there not be some very tight encoding in terms of "normal" assembly language operators? This has been a persistent question in my mind that comes up frequently in different and often more general forms. If you want to make a fast compiler, how do you know what instructions to output? If you have a highlevel specification, how can you avoid the ridiculously high overhead usually associated with extremely high level languages? Today I found this fabulous pap...