Again, the statement of the problem. >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. The first restriction is outward confinement. The second >restriction is inward confinement.
Again, Here is some E code that demonstrates the use of E's deep-frozen guard. Since I don't quite yet understand E, MarkM graciously translated it into Scheme where of course the guard :deep-frozen is not really Scheme. >(define (cassie max) > (define x 0) ; x is mutable. > (define y 0) ; y is mutable > (define (accept-product calc-factory:deep-frozen) > (let ((diode 0)) ; diode is mutable > (define (diode-write val:deep-frozen) (set! diode val)) > (define (diode-read) diode) > (let ((q (calc-factory diode-write #f)) > (bond (calc-factory #f diode-read)) ) > (q 33) > (set! y (bond 44)) ; y may depend on both 33 and 44 > (set! x (q 55)))) ; Cassie knows that x cannot depend on > ; the 44 she passed to Bond. > #f) ; Since Max calls accept-product, we need to prevent it > ; from leaking an unintended result value back to Max. > (max accept-product) > (display x) ; Depends on at most 33 & 55 according to some algorithm > ; determined by Max. The inability for x to be influenced by > ; Cassie's choice to pass 44 to Bond demonstrates the > ; *-properties. > (newline) > (display y) ; Depends on at most 33 & 44 according to some algorithm > ; determined by Max. (Though its lack of dependence on 55 > ; is based on reasoning about sequential time rather > ; than confinement.) > (newline) ) >(define (max accept-product) > (define (calc-factory optWriter optReader) > (define accum 0) ; accum is mutable. > (define (calc num) > (if optReader > (set! accum (+ accum (optReader)))) > (set! accum (+ accum num)) > (if optWriter > (optWriter accum)) > accum) > calc) > (accept-product calc-factory) > #f) >(cassie max) I have worked out how to do that in Haskell, using only idioms widely-used in the Haskell community. namely, Cassie renames the IO type C; she then lifts into C only "safe" operations and requires Max to write his code to that type C. Deep-frozenness depends among other things on Max's code _not_ refering to the data constructors MakeC and MakeCRef, a condition not enforced by Haskell. (So, someone would have to eyeball that.) >import Prelude hiding (max) >import Data.IORef >data C a = MakeC (IO a) >data CRef a = MakeCRef (IORef a) >instance Monad C where > MakeC p >>= k = MakeC (p >>= \a -> case k a of MakeC p2 -> p2) > return = MakeC . return >runC :: C a -> IO a >runC (MakeC body) = body >newCRef :: a -> C (CRef a) >readCRef :: CRef a -> C a >writeCRef :: CRef a -> a -> C () >modifyCRef :: CRef a -> (a -> a) -> C () >newCRef a = MakeC (newIORef a >>= return . MakeCRef) >readCRef (MakeCRef ref) = MakeC (readIORef ref) >writeCRef (MakeCRef ref) a = MakeC (writeIORef ref a) >modifyCRef (MakeCRef ref) f = MakeC (modifyIORef ref f) >cassie max = do > xref <- newIORef (0 :: Integer) > yref <- newIORef (0 :: Integer) > let acceptProduct calcFactory = runC (do > diodeRef <- newCRef (0 :: Integer) > let > writeDiode n = writeCRef diodeRef n > readDiode = readCRef diodeRef > bond <- calcFactory Nothing (Just readDiode) > q <- calcFactory (Just writeDiode) Nothing > q (33 :: Integer) > y <- bond (44 :: Integer) > MakeC (writeIORef yref y) > x <- q (55 :: Integer) > MakeC (writeIORef xref x) > return () ) > max acceptProduct > x <- readIORef xref > print x > y <- readIORef yref > print y >max acceptProduct = do > let calcFactory optWriter optReader = do > accum <- newCRef (0 :: Integer) > return (\num -> do > case optReader of > Nothing -> return () > Just reader -> do > temp <- reader > modifyCRef accum (+ temp) > modifyCRef accum (+ num) > case optWriter of > Nothing -> return () > Just writer -> do > temp <- readCRef accum > writer temp > readCRef accum ) > acceptProduct calcFactory > return () >main = cassie max Now these data constructors, MakeC and MakeCRef, can--for present purposes--be viewed as (seal,unseal) pairs, which suggests a way to translate the above code back into Scheme this time without the :deep-frozen guard. (i.e., it would be Scheme, not Scheme plus this guard that a Scheme implementation won't understand.) But I'm too tired to work on that tonight. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
