Skip to main content


Showing posts from February, 2007

Protected access using lightweight capabilities

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, 'n…

Automated Deduction and Functional Programming

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
two, though …