A monad for type casting

[Koen Claessen]

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.