[Cap-Talk] immutable data

[Richard Uhtenwoldt]

Norman Hardy writes:

>I do not [know] the specific differences between Scheme 48 and the standard
>Scheme but

Just that some care has gone into Scheme 48's runtime to keep it from leaking
secrets.


>I have some notes at <http://ccap-lore.com/CapTheory/SKBLC.html> 
>Referring to a paper by Jonathan Rees in which Scheme is used in a 
>strong capability sense.

I've been browsing eros-os.org et al for years but did not become
enthusiastic about strong capabilities till I read Rees's paper.  (Rees's
paper requires a knowledge of Scheme and is at
href="http://mumble.net/jar/pubs/secureos/".

The paper show how a programmer can exploit the principle that if a
programmer cannot name an authority, she cannot exercise that authority.
of course, the e-lang and eros-os and cap-lore.com web sites say the same
thing, but because they are complex artifacts requiring mastering many
details (pages, nodes, segments, etc), I never mastered enough detail
about Eros or E or KeyKOS to see for myself how capabilities result in
programs more secure than those produced today without more work on the
programmer's part (once the capability concepts have been learned).

Rees's paper shows with a minimum of extraneous detail how strong
capabilities give an elegant (low cost in program complexity) solution to
a bunch of problems that have annoyed me about software.  for me
personally the annoying problem whose solution via capabilities most
impressed me is the vexing situation where the install program of one web
browser overwrites without asking the user the hard-won config settings
of a competing web browser that is already installed.


Reading http://cap-lore.com/CapTheory/sensoryScm.html, I think I can
clear up a point about Scheme for you:

> I don't see a clear stance as to
> whether environments are mutable

They are.  In Scheme, a variable is always bound to a location.  a
location is always mutable and contains a value.

At least two people on the e-lang list, Rees being one of them, have
asserted that this is a design flaw of Scheme (I can point you at the
messages if you like--it was like 6 months ago), and I agree.

The reason it is a flaw is that it is sometimes valuable to name a chunk
of immutable data (of arbitrary type, integer, list of integer, etc).
exactly that --modulo concerns about being able to verify compiled code
whereas type systems are usually applied to source code-- is what you
need to do in sensoryScm.html.

ML lets you do that with minimal fuss.  in particular, ML's variables are
by default bound to (immutable) values; to get mutability, you bind the
variable not to an ordinary value like an (immutable) integer but rather
to what called a ref (although "loc" would have been a more apt term,
IMO).  refs and mutable arrays are probably the only mutable data types
in ML.

I.e., in ML, immutable data is the default kind of data, even for
composite data types like lists and tuples (collections of heterogenous
things like records in Cobol or Pascal); 80 to 90% of variables in ML
programs are bound to immutable data; programmers strive to minimize
reliance on mutable data.  when you need mutable data, you explicitly use
a ref.  Specifically, noting that ML is a statically typed language,
instead of declaring

  i : integer

one would declare

  ri : ref integer         ("ri is of type ref containing an integer")

and then one would write !ri (pronounced "deref ri" I suggest) to fetch
from the ref and ri:=53 to store into the ref.  i:=53 is a type error.
so is

  ri * 3 

--one has to write

  !ri * 3

Here is roughly how one would translate your notation into ML.
the ML is probably not well formed but close enough to convey the idea.

(let ((i 4)) (see i)) <---> let i=4 in i
(let ((i 4)) i)       <---> let ri=ref 4 in !ri   
    (note how ML makes the programmer distinguish between i and ri)
(let ((pi (cons 3 4))) (set-cdr! pi 42) pi) <---> 
    let pi=Pair !3 !4 in {(cdr pi):=42; pi}
(see (cons 3 4)) <---> Pair 3 4

Everything I said about ML applies modulo syntax to the other functional
programming languages (FPLs) I know about.  I mention ML because ML is
the FPL closest to Scheme, differing from Scheme mainly by being
statically typed.

The folks on the e-lang list seem to prefer dynamically typed languages.
There is no reason why a dynamically typed language could not use its
type system to distinguish between mutable and immutable data the way
FPLs do, but I do not know of one with a currently maintained
implementation.  certainly no language used by more than 100 programmers
at any give time.  well, that too strong: Dylan is certainly dynamically
typed but I do not know if it lets the programmer distinguish immutable
from mutable data.  Kind of doubt it.  And I know nothing about Smalltalk
or Ruby.  Prolog might do it but Prolog is unsuitable for cap programming
for other reasons.

Finally, it is a treat to correspond with such an accomplished person,
and I hope my exposition on mutability wasnt too long and tedious.