[Haskell-cafe] heterogeneous environment

[oleg at okmij.org]

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