Hi all,
Here is a little experiment I did a while ago. I was trying
to isolate the capability of the ST monad to deal with
different types at the same time. (Following up on a
discussion at the Haskell Workshop in 2000, where we
discussed that the ST monad is really a combination of
different features that should be separated.)
The idea is that one has a monad, "O s", in which one can
create objects with identity, of type "Object s a":
type O s a -- abstract, Monad
type Object s a -- abstract
newObject :: O s (Object s a)
The idea is now that, we want to be able to compare these
objects for equality. But not only that! Given two objects
of possibly different types, say "Object s a" and "Object s
b", if they are equal, then so must their types be!
So, instead of making "Object s a" an instance of "Eq", we
provide the following function:
compareObject :: Object s a -> Object s b -> Maybe (a -> b)
If the objects are not equal, we get "Nothing". But, if the
objects are equal, we also get a "proof" of that you can
cast between their types.
This monad is safe, and can be used as a basis for monads in
which one wants to implement something like "STRef"s. I
provide an implementation of an (inefficient, but complete)
ST monad, only using the O monad.
I conjecture this functionality cannot be implemented in
Haskell 98, nor in any of the known safe extensions of
Haskell. Here, I provide an implementation that works with
Hugs.
Any comments?
One thing I would like to propose for GHC and Hugs is to
provide a function like "compareObject" for "STRef"s and
"IORef"s.
Regards,
/Koen.
=====
module Object
( O -- :: * -> * -> *; Monad
, Object -- :: * -> * -> *
, newObject -- :: O s (Object s a)
, compareObject -- :: Object s a -> Object s b -> Maybe (a -> b)
, runO -- :: (forall s . O s a) -> a
)
where
-------------------------------------------------------------------
-- This module is an attempt to isolate the capability of the ST
-- monad of dealing with several types at the same time.
--
-- The idea is that objects of type "Object s a" represent `objects
-- with identity', that are associated with a type a. There exists
-- a comparison function that checks if two objects have the same
-- identity. If this is the case, the associated types should be
-- the same too, and a witness function is provided.
--
-- To ensure that objects with the same identity really are the
-- same object, and also to avoid polymorphically typed objects,
-- we have to create the objects in a monad. We also have to use the
-- "trick with the s", also used in the realization of the ST
-- monad in Haskell. This trick also ensures we can never compare
-- two "Object"s from two different "O"-threads.
--
-- I conjecture that it is impossible to implement this module in
-- pure Haskell with any of the known safe extensions. (So it is
-- even impossible if you are allowed to use the ST monad.)
--
-- Koen Claessen, 19 November 2000
-------------------------------------------------------------------
-------------------------------------------------------------------
-- type O, type Object:
-- "O" is a state monad keeping track of unique tags. "Object"
-- only contains a tag for checking equality.
newtype O s a = MkO (Int -> (a, Int))
newtype Object s a = MkObject Int
instance Monad (O s) where
return x = MkO (\n -> (x, n))
MkO m >>= f = MkO (\n -> let (a, n') = m n ; MkO m' = f a in m' n')
-------------------------------------------------------------------
-- newObject:
-- creating a new object is creating a new tag.
newObject :: O s (Object s a)
newObject = MkO (\n -> (MkObject n, n+1))
-------------------------------------------------------------------
-- compareObject:
-- We check if the objects are equal. If so, we know we can safely
-- cast.
compareObject :: Object s a -> Object s b -> Maybe (a -> b)
compareObject (MkObject tag1) (MkObject tag2)
| tag1 == tag2 = Just unsafeCoerce
| otherwise = Nothing
-- boo!
primitive unsafeCoerce "primUnsafeCoerce" :: a -> b
-------------------------------------------------------------------
-- runO:
-- Executing the state monad.
runO :: (forall s . O s a) -> a
runO m = let MkO f = m ; (a, _) = f 0 in a
-------------------------------------------------------------------
-- the end.
=====
module MyST
( ST -- :: * -> * -> *; Monad
, STRef -- :: * -> * -> *; Eq
, newSTRef -- :: a -> ST s (STRef s a)
, writeSTRef -- :: STRef s a -> a -> ST s ()
, readSTRef -- :: STRef s a -> ST s a
, runST -- :: (forall s . ST s a) -> a
)
where
-------------------------------------------------------------------
-- This module implements an inefficient version of the ST
-- monad in "normal" Haskell; the only extensions we use are
-- existential and universal quantification, and the "Object" module.
--
-- The implementation is inefficient because it uses lists as
-- lookup tables.
--
-- Koen Claessen, 19 November 2000
-------------------------------------------------------------------
import Object
( O
, Object
, newObject
, compareObject
, runO
)
-------------------------------------------------------------------
-- type ST, type State, type Entry, type STRef:
-- the implementation is straightforward: "ST" is a state monad
-- in a type "State", which is a lookup table of existentially
-- quantified "Entry"s. We also implement a weaker form of
-- equality on "STRef"s.
newtype ST s a = MkST (State s -> O s (a, State s))
type State s = [Entry s]
data Entry s = forall a . Object s a := a
newtype STRef s a = MkSTRef (Object s a)
instance Monad (ST s) where
return x = MkST (\n -> do return (x, n))
MkST m >>= f = MkST (\n -> do (a, n') <- m n ; let MkST m' = f a in m' n')
instance Eq (STRef s a) where
MkSTRef tp1 == MkSTRef tp2 =
case tp1 `compareObject` tp2 of
Just _ -> True
Nothing -> False
-------------------------------------------------------------------
-- newSTRef, readSTRef, writeSTRef, runST:
-- the only interesting things happening here are the safe casts
-- by "readSTRef" and "writeSTRef" (note that they are done in
-- different directions).
newSTRef :: a -> ST s (STRef s a)
newSTRef a = MkST $ \st ->
do tp <- newObject
return (MkSTRef tp, (tp := a) : st)
readSTRef :: STRef s a -> ST s a
readSTRef (MkSTRef tp) = MkST $ \st ->
do return (find st tp, st)
where
find ((tp1 := a) : st) tp2 =
case tp1 `compareObject` tp2 of
Just cast -> cast a
Nothing -> find st tp2
writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef (MkSTRef tp) a = MkST $ \st ->
do return ((), update st tp a)
where
update (ent@(tp1 := a) : st) tp2 a' =
case tp2 `compareObject` tp1 of
Just cast -> (tp1 := cast a') : st
Nothing -> ent : update st tp2 a'
runST :: (forall s . ST s a) -> a
runST m = let MkST f = m in runO (do (a,_) <- f []; return a)
-------------------------------------------------------------------
-- the end.
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
