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...