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 S nat) slist -> int end structure SList :> SLIST = struct (* encode integer types *) type 'a nat = int type Z = unit type 'a S = unit fun S i = i+1; fun P i = i-1; fun Z () = 0 fun zerop 0 = true | zerop _ = false fun toInt d = d type ('elt, 'n) slist = 'elt list * 'n fun snil () = ([],0) fun scons elt sl = let val (l,i) = sl in ((elt::l),S i) end infixr :+: fun x :+: y = scons x y fun shd sl = let val (h::t,i) = sl in h end fun stl sl = let val (h::t,i) = sl in (t,P i) end fun slen sl = let val (_,i) = sl in i end end open SList infixr :+: val mylist = 1 :+: 2 :+: 3 :+: snil(); val the_head = shd mylist; val the_tail = stl mylist; val the_next_head = shd the_tail; (* This doesn't even compile! val head_of_nil = shd (snil()) *)

## Comments

## Post a Comment