[bitc-dev] deeply immutable functions and Haskell's ST

Richard Uhtenwoldt ru at river.org
Thu Aug 25 06:54:30 EDT 2005


Jonathan S. Shapiro writes:
>Some time ago, Mark Miller introduced a notion of "deeply immutable"
>functions. A deeply immutable function is not permitted to close over
>any mutable state. This means that it can only mutate arguments and
>locals, and that it cannot *read* any mutable state from its
>environment. 

Now I realize that you guys are fully capable of writing a type
checker that can impose this deep-immutability constraint all by
yourselves, but I thought you might like to know that GHC's type
system can already express this deep-immutability constraint.  in
fact, this has been the case since 1994.

particularly, in 1994, a paper appeared that described the "ST
monad", which has been available to user of GHC ever since.  this
ST monad, or "ST type" if you prefer, is settled, proven design:
GHC simply implemented the design described in the paper, and
that design has not needed any changes except for the fact that
it turns out that _lazy_ state monads are in fact
difficult/unintuitive for Haskell programmers to reason about
with the result that ST was changed into a _strict_ state monad.
(a strict state monad is what we want anyways because it is the
one that is isomorphic to the corresponding language features in
imperative languages like E, BitC, etc.)

now, I realize that you guys are not planning to embrace monads,
and you are probably a little turned off by the thought that this
solution depends on a monad, so please give me a few paragraphs
to try to set your minds at ease.

monads can be thought of as just another part of the type system
of Haskell.

in fact, according to one (Moggi) of the two researchers
responsible for the introduction of monads into Haskell (the
first language to have monads), the original insight that led to
monads in Haskell was that it might well prove useful for the
type system to distinguish between the type (e.g., Int) of a
value (e.g., 4) and the type (e.g., IO Int) of a computation that
performs some side effects, then yields a value.

now, Haskellers have not up to now been interested in things like
confinement.  (I tend to think that they should _become_
interested.)  the ST monad was introduced into Haskell for a
quite-different reason, and to tell you the truth it is not used
all that much because people do not often need to solve the
programming problem the ST monad solves --or when they do there
are other solutions available (e.g., to put the whole program in
the IO monad).

But it is quite noncontroversial: there are no Haskellers going
around saying things like "the ST monad must die," or, "the ST
monad was a mistake," or such.


>                            Consider something like:
>
>  (deftypeclass (Eql 'a)
>    == : (fn ('a 'a) 'a))
>
>followed by an instantiation:
>
>  (definstance (Eql SomeType)
>    (lambda (x y) (and (isEqual x SomeGlobal)
>                       (isEqual y SomeGlobal))))
>
>where SomeGlobal is mutable.
>
>There is no intrinsic problem in the type system with this
>instantiation, but it has an unpleasant consequence: deeply immutable
>procedures cannot invoke methods because they may later be instantiated
>in a way that violates deep immutability.

== has what we would call in Haskell a pure type.  

"pure" is used by the Haskell community in multiple ways, so let
me define how I use it here.  

it turns out to be easier to define the notion "not pure", as
follows.  if a is any type, then IO a and ST s a are not pure for
any type s.  if i is not pure, so is a -> i for any type a.

Note that according to my definition, [IO ()] is a pure type:
this is a reasonable result because there is no way to activate
those IOs unless the [IO ()] is part of a larger impure type.

if an expression has a pure type, then it cannot sense or mutate
any mutables that are bound to variables that are free in that 
expression.

note that I do not say that an expression of pure type cannot
close over a mutable because indeed it can close over whatever it
likes, but it cannot sense or mutate anything it closes over.

recall that in haskell, if "ref" is a mutable, then to sense
"ref", it does not suffice (as it does not most languages) simply
to write "ref" but rather you have to write "readIORef ref" or
"readSTRef ref".  

and readIORef is simply not available in any pure type, and
readSTRef is restricted to mutables that have been allocated
inside the pure type (inside a runST inside the pure type, to
be precise).

now it is possible in haskell to define

  (deftypeclass (Eql 'a)
    == : (fn ('a 'a) 'a))
  (definstance (Eql SomeType)
    (lambda (x y) "allocate some local mutables and some local arrays
       and then sense and mutate the hell out of them in the 
       process of determining whether x and y are equal" ))

and in fact that is exactly what the ST monad is for.  The 'a is
still considered a pure type.

the type system (in particular, rank-2 polymorphism) ensures that
that last instance definition will sense and mutate only mutables
it itself has allocated.

>There appear to be four solutions:

>4. Make (deeply-immutable T) an explicit part of the type system.
>UNFORTUNATELY THIS APPEARS TO BE A MESS.

well guess what :) this is what Haskell does.

If there are any Haskell experts reading this, I have to point
out a wrinkle: Dr Shapiro and Mark Miller want to apply the
deep-immutability concept to _functions_ whereas the ST type can
express/capture the notion of deep immutability only of
_computations_.  I have a rather simple (but untested) way to
address that wrinkle that involves writing no more than 30 or 40
lines of Haskell code, which I'll be glad to show you as soon as
I write and test it.

the 1994 paper is here:

http://research.microsoft.com/Users/simonpj/Papers/lazy-functional-state-threads.ps.Z

You need to read only the first 6 pages unless you want to learn
how to add an ST monad to a language implementation.

Now a request: can someone please post or send me sample code
that _uses_ a deeply-immutable function?  The object-oriented
nature of E code makes it less than ideal for my purpose because
hard to translate into Haskell, so I'd prefer pseudo-Scheme or
pseudo-BitC code.




More information about the bitc-dev mailing list