Ben wrote:
- use Data.Unique to identify Refs, and use existential quantification or Data.Dynamic to create a heterogenous Map from uid to log. for example, to represent a log of compare-and-swaps we might do something like
data Ref a = Ref (IORef a) Unique data OpaqueCAS = forall a . OpaqueCAS { casRef :: Ref a, oldVal :: a, newVal :: a } type CASLog = Map Unique OpaqueCAS logCAS r@(Ref _ uid) o n log = insert uid (OpaqueCAS r o n) log...
but what if the transaction wants to perform a second CAS on a reference we've already CAS'd? then we should create a combined OpaqueCAS record which expects t he first oldVal and swaps in the second newVal. unfortunately the type checker balks at this, as it can't prove that the type variable 'a from the first record is the same as the 'a in the new record; i suppose there might be some fancy type shenanigans which might solve this...
It seems you actually prefer this solution, if it worked. This solution will entail some run-time check one way or another, because we `erase' types when we store them in the log and we have to recover them later. If the problem is of merging two CASLog entries into one, your code above already solves it. There are no type shenanigans are necessary. I will make slight modification though by introducing an extra IORef for `ephemeral' communication. Values written to that IORef almost immediately retrieved. It is not strictly necessary since your Ref already has one IORef; I assume that it can't be garbled, even for a brief moment. The complete code is enclosed at the end of the message. If one wants to live a bit dangerously but efficiently, one may wish to create a module of reference cells indexed by unique numbers, like your Ref. The data constructor Ref is not exported. If the only way to create Refs is to use the function newRef of the module, and that function assuredly creates a Ref with a unique label, one is justified in writing the function cast :: Ref a -> Ref b -> Maybe (Ref b) cast r1@(Ref _ u1) (Ref _ u2) | u1 == u2 -> Just (unsafeCoerce r1) cast _ _ = Nothing because the same labels correspond to references of the same type. The _safe_ solution, similar to that in the enclosed code below, was used in HANSEI, which is the embedded DSL for probabilistic programming. Here is the relevant code describing first-class memory (it is OCaml). (* We often use mutable variables as `communication channel', to appease the type-checker. The variable stores the `option' value -- most of the time, None. One function writes a Some x value, and another function almost immediately reads the value -- exactly once. The protocol of using such a variable is a sequence of one write almost immediately followed by one read. We use the following helpers to access our `communication channel'. *) let from_option = function Some x -> x | None -> failwith "fromoption";; let read_answer r = let v = from_option !r in r := None; v (* for safety *) (* First-class storage: for the implementation of `thread-local' memory *) module Memory = struct type 'a loc = int * 'a option ref type cell = unit -> unit module M = Map.Make(struct type t = int let compare x y = x - y end) type mem = cell M.t let newm = M.empty let genid : unit -> int = (* generating fresh locations *) let counter = ref 0 in fun () -> let v = !counter in counter := succ v; v let new_loc () = (genid (), ref None) let new_cell (_,chan) x = fun () -> chan := Some x let mref (id,chan) m = let cell = M.find id m in cell (); read_answer chan let mset ((id,chan) as loc) x m = M.add id (new_cell loc x) m end;; Enclosed Haskell code: {-# LANGUAGE ExistentialQuantification #-} module Ref where import Data.IORef import Data.Unique import Data.Map as M data Ref a = Ref (IORef a) (IORef a) Unique data OpaqueCAS = forall a . OpaqueCAS { casRef :: Ref a, oldVal :: a, newVal :: a } type CASLog = M.Map Unique OpaqueCAS logCAS r@(Ref _ _ uid) o n log = M.insert uid (OpaqueCAS r o n) log -- If one is bothered with undefined below, use Nothing newRef :: a -> IO (Ref a) newRef x = do r1 <- newIORef x r2 <- newIORef undefined -- auxiliary u <- newUnique return (Ref r1 r2 u) writeOld :: OpaqueCAS -> IO () writeOld (OpaqueCAS (Ref _ ra _) o n) = writeIORef ra o readOld :: OpaqueCAS -> IO OpaqueCAS readOld (OpaqueCAS r@(Ref _ ra _) _ n) = do o <- readIORef ra -- guard against errors and memory leaks writeIORef ra undefined return (OpaqueCAS r o n) writeNew :: OpaqueCAS -> IO () writeNew (OpaqueCAS (Ref _ ra _) o n) = writeIORef ra n readNew :: OpaqueCAS -> IO OpaqueCAS readNew (OpaqueCAS r@(Ref _ ra _) o _) = do n <- readIORef ra -- guard against errors and memory leaks writeIORef ra undefined return (OpaqueCAS r o n) -- Create CAS record with the old value from the first CAS and -- the new value from the new CAS. -- First we assume that the two OpaqueCAS correspond to the same -- variable. A run-time error occurs otherwise. -- Second, we make no checks for the relation between the new -- value of the first CAS and the old value of the new CAS. Probably -- they are meant to be the same. Anyway, we don't even look at them. combineCAS:: OpaqueCAS -> OpaqueCAS -> IO OpaqueCAS combineCAS cas1 cas2 = do writeNew cas2 readNew cas1