Safe and sound STRef [Was Implementing RefMonads in Haskell without ST,IO]

[o***@pobox.com]

Back in September 2001, Koen Claessen wrote:
] 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.... I conjecture this functionality cannot be implemented
] in Haskell 98, nor in any of the known safe extensions of Haskell.

Recently, Tim Sweeney wrote
] Is it possible to actually implement a working instance of RefMonad in
] Haskell, without making use of a built-in monad like IO or ST?

The following code shows a safe and sound implementation of a
polymorphic heap with references and updates. The heap is capable of
storing of polymorphic, functional and IO values. All operations are
*statically* checked. An attempt to alter a heap reference with a
value of a mismatched type leads to a _compile-time_ error. Everything
is implemented in Haskell98 + multiparameter classes with functional
dependencies + overlapping instances. I suspect that the latter isn't
strictly needed, but it's almost midnight. Most importantly, no IO or
ST monad, no unsafePerformIO or unsafeCoerce, no existential types and
no Dynamics are needed. It seems that the polymorphic updateable heap
can be implemented safely. Although the code looks like a monadic
code, the Monad class doesn't seem to be polymorphic enough to wrap
our heap. Perhaps arrows will help.

I'd like to remark first that the ST monad with polymorphic STRef can
be implemented in Haskell98 + safe extensions _provided_ all the
values question are in the class Show/Read. When we store values,
we store their external representation. When we retrieve a value, we
read it. Similarly for values in the Binary class. All such values are
_safely_ coercible. The following code however does not make this
assumption. In our heap below, we can even store polymorphic
functions and IO values!


First, the tags for values in our heap

data Zero
data Succ a
class HeapTag a where
tag_value:: a -> Int
instance HeapTag Zero where
tag_value _ = 0
-- I just can't avoid the undefined arithmetics
instance (HeapTag t) => HeapTag (Succ t) where
tag_value _ = 1 + tag_value (undefined::t)

The heap reference is the combination of the tag and the desired
type. As we will see, the value of the second argument of the HeapRef
doesn't actually matter -- only its type does.

data HeapRef t a = HeapRef t a

Our heap is implemented as a polymorphic associative list

data Nil t v r = Nil
data Cons t v r = Cons t v r
class PList ntype ttype vtype cdrtype where
cdr:: ntype ttype vtype cdrtype -> cdrtype
empty:: ntype ttype vtype cdrtype -> Bool
value:: ntype ttype vtype cdrtype -> vtype
tag:: ntype ttype vtype cdrtype -> ttype
instance PList Nil ttype vtype cdrtype where
empty = const True
instance (PList n t v r,HeapTag tag) => PList Cons tag vtype (n t v r) where
empty = const False
value (Cons t v r) = v
tag (Cons t v r) = t
cdr (Cons t v r) = r
class Heap t v h | t h -> v where
fetch:: (HeapRef t v) -> h -> v
alter:: (HeapRef t v) -> v -> h -> h
instance (HeapTag t,PList Cons t v r) => Heap t v (Cons t v r) where
fetch _ p = value p
alter _ vnew (Cons t v r) = (Cons t vnew r)
instance (HeapTag t,Heap t v r,PList Cons t' v' r) =>
Heap t v (Cons t' v' r) where
fetch ref p = fetch ref $ cdr p
alter ref vnew (Cons t v r) = Cons t v $ alter ref vnew r

Let's make our heap instances of a class Show, so we have something to show.

instance (PList Nil ttype vtype cdrtype) => Show (Nil ttype vtype cdrtype)
where
show _ = "[]"
instance (Show vtype, HeapTag ttype, PList Cons ttype vtype cdrtype,
Show cdrtype) =>
Show (Cons ttype vtype cdrtype)
where
show x = (show $ (tag_value $ tag x, value x)) ++ " : " ++ (show $ cdr x)

Let's take a few simple examples

tinc (x::t) = undefined::(Succ t)
tag_one = (undefined::(Succ Zero))
acons = Cons
lst1 = acons tag_one 'a' $ Nil
lst2 = acons (tinc tag_one) 'a' $ acons tag_one True $ Nil
test1 = fetch (HeapRef tag_one 'z') lst1

The result is 'a'. We see that the value of the second argument of
HeapRef doesn't actually matter. But its type sure does: if we
uncomment the following line

-- test1' = fetch (HeapRef tag_one (1::Int)) lst1

we get an error:

/tmp/o1.lhs:127:
Couldn't match `Char' against `Int'
Expected type: Char
Inferred type: Int
When using functional dependencies to combine
Heap t v (Cons t v r),
arising from the instance declaration at /tmp/o1.lhs:91
Heap (Succ Zero) Int (Cons (Succ Zero) Char (Nil t v r)),
arising from use of `fetch' at /tmp/o1.lhs:127
When generalising the type(s) for `test1''

Indeed, the stored value is of type Char and we try to read it as an
Int.

test21 = fetch (HeapRef tag_one False) lst2
-- the latter test again makes sure that fetching is type safe
--test22' = fetch (HeapRef (tinc tag_one) False) lst2
test22 = fetch (HeapRef (tinc tag_one) (undefined::Char)) lst2
testa1 = alter (HeapRef tag_one (undefined::Bool)) False lst2
--gives: (2,'a') : (1,False) : []
testa2 = alter (HeapRef (tinc tag_one) (undefined::Char)) 'y' lst2
--gives: (2,'y') : (1,True) : []

Now we can bundle our heap with an allocation pointer

-- p is the heap, t is the next tag to allocate in p
data GHeap t p = GHeap t p
instance (HeapTag t,Show p) => Show (GHeap t p) where
show (GHeap t p) = "Global heap: alloc ptr " ++ (show$tag_value t) ++
"\n" ++ (show p)
init_gh = GHeap (undefined::Zero) Nil
fetch_gh ref (GHeap _ p) = fetch ref p
alloc_gh x (GHeap t p) = (HeapRef t x,GHeap (tinc t) (Cons t x p))
alter_gh ref newval (GHeap t p) = GHeap t $ alter ref newval p

And finally the big test. The test shows storing and altering regular
values, polymorphic function values and even IO values.

test3 = do
let heap = init_gh
let (xref,heap1) = alloc_gh 'a' heap
let (yref,heap2) = alloc_gh [(1::Int),2,3] heap1
let (zref,heap3) = alloc_gh (Just False) heap2
putStrLn "\nAfter allocations"
print heap3
putStr "x is "; print $ fetch_gh xref heap3
putStr "y is "; print $ fetch_gh yref heap3
putStr "z is "; print $ fetch_gh zref heap3
let heap31 = alter_gh xref 'z' heap3
let heap32 = alter_gh yref [] heap31
let heap33 = alter_gh zref (Just True) heap32
putStrLn "\nAfter updates"
print heap33
putStr "x is "; print $ fetch_gh xref heap33
putStr "y is "; print $ fetch_gh yref heap33
putStr "z is "; print $ fetch_gh zref heap33
putStrLn "\nPolymorphic and IO values"
let (gref,heap4) = alloc_gh (\x->x+1) heap33
let (href,heap5) = alloc_gh id heap4
let (mref,heap7) = alloc_gh (putStrLn "Monad!") heap5
putStr "g 1 is "; print $ (fetch_gh gref heap4) (1::Int)
putStr "h True is "; print $ (fetch_gh href heap5) True
putStr "h 'a' is "; print $ (fetch_gh href heap5) 'a'
putStr "m is "; (fetch_gh mref heap7)
let heap71 = alter_gh mref (putStrLn "New Monad") heap7
let heap72 = alter_gh gref (\x->x+5) heap71
putStrLn "\nAfter updates to polymorphic and IO values"
putStr "g 1 is "; print $ (fetch_gh gref heap72) (1::Int)
putStr "m is "; (fetch_gh mref heap72)
return ()

I had many occasions to see that an attempt to retrieve the value of a
wrong type or change the value with that of a wrong type result in a
compiler error! Although we are "altering" polymorphic values, the type
safeness seems to be preserved

test4 = do let heap = init_gh
let (xref,heap1) = alloc_gh [] heap
let (yref,heap2) = alloc_gh [(1::Int)] heap
let (zref,heap3) = alloc_gh [True] heap
let heap11 = alter_gh xref [(1::Int)] heap1
--let z = fetch_gh zref heap11
let z = fetch_gh zref heap1
print z

If we uncomment the commented line, we will get a type error!

The lines like
*> let (yref,heap2) = alloc_gh [(1::Int),2,3] heap1
*> let (zref,heap3) = alloc_gh (Just False) heap2

almost suggest a monad. Alas, the Monad class doesn't seem to be
polymorphic enough. The type of the >>= is
forall m b a. (Monad m) => m a -> (a -> m b) -> m b
although 'b' at the end doesn't have to be the same as 'a' at the
beginning, 'm' must be the same in the argument of >>= and in its
result. However, in our example, heap2 has a type different from that
of heap1.


ghci -fglasgow-exts -fallow-undecidable-instances
-fallow-overlapping-instances /tmp/o1.lhs

[Keith Wansbrough]

Post by o***@pobox.com
The following code shows a safe and sound implementation of a
polymorphic heap with references and updates. The heap is capable of
storing of polymorphic, functional and IO values. All operations are
*statically* checked. An attempt to alter a heap reference with a
value of a mismatched type leads to a _compile-time_ error. Everything
is implemented in Haskell98 + multiparameter classes with functional
dependencies + overlapping instances.

The problem you mention later, that the type of the heap returned is
different from the type of the heap passed, is fatal. The following
expression is untypeable:

let heap = init_gh in
let (mr,heap1) = if 1<2 then
let (xr,h) = alloc_gh 42 heap in (Just xr,h)
else
(Nothing,heap) in
case mr of
Nothing -> ""
Just r -> show (fetch_gh r heap1)

Heaps should be more dynamic than this; the (type of the) *reference*
should encode the type it points to, but the (type of the) *heap*
should not.

The question is still open...

--KW 8-)

[o***@pobox.com]

It seems it is possible to implement polymorphic references using the
regular (not IO and not ST) monad and without resorting to any unsafe
extension. Furthermore, that monad has a run function, which does not
compromise the type safety.

When I claimed in the previous message that the polytypic nature of
the heap precludes its encapsulation in a monad, I was fortunately
mistaken. I was confused: I thought that a function signature a->a
meant that the type of the argument must be identical to the type of
the result. That is clearly not true: the type of the argument should
merely be specializable to the type of the result. If we pre-allocate
a heap with, say, 5 cells of the undefined value, we can store values
of any type in these cells. Of course, after we wrote something in a
cell, we can overwrite it with the value of the same or a more
specialized type. Therefore, we can seek the fixpoint heap without
offending the typechecker. This gives us a desired monad.


[Continuing the code from the original message]

t1 = tag_one
t2 = (tinc t1)
t3 = (tinc t2)
t4 = (tinc t3)
t5 = (tinc t4)
heap5 = Cons t5 undefined $ Cons t4 undefined $ Cons t3 undefined $
Cons t2 undefined $ Cons t1 undefined $ Nil
newtype HeapM h a = HeapM (h->(a,h))
instance Monad (HeapM h) where
return x = HeapM $ \h -> (x, h)
HeapM m >>= f = HeapM $ \h -> let (x, h') = m h; HeapM m' = f x in m' h'

The argument of hget and hput functions below must be a heap of 5
cells, with arbitrary values. heap5 is the most general heap of that
sort

hget tag = HeapM $ \(h::t) -> (fetch (HeapRef tag undefined) h,h)
where x::t = heap5
hput tag newval = HeapM $
\(h::t) -> ((),alter (HeapRef tag undefined) newval h)
where x::t = heap5
runHOF (HeapM hf) = fst $ hf heap5

The test. We test storing and altering polymorphic values, including
polymorphic functional values!

test7 = do
let l1 = tag_one
hput l1 'a'
v1 <- hget l1
let l2 = tinc l1 -- our allocator is somewhat primitive at the moment
hput l2 Nothing -- storing a polymorphic value of type Maybe a
v2 <- hget l2
let l3 = tinc l2
hput l3 (\x->x+1) -- storing a polymorphic function over Num a
v3 <- hget l3
-- Update the cells and retrieve the updated values
hput l1 'b'
v11 <- hget l1
hput l2 $ Just True -- overwrite with a more specialized value
v21 <- hget l2
hput l3 (\x->x+5)
v31 <- hget l3
return $ [[show v1, show v2, show $ v3 1],
[show v11, show v21, show $ v31 1]]

The result is

*Main> runHOF test7
[["'a'","Nothing","2"],["'b'","Just True","6"]]


Ashley Yakeley wrote:
] ] Is it possible to actually implement a working instance of RefMonad in
] ] Haskell, without making use of a built-in monad like IO or ST?

] You certainly wouldn't be able to do this for any monad M which had:

] performM :: forall a. M a -> a;

] ...because it wouldn't be type-safe: you'd be able to construct coerce
] :: a -> b just as you can with unsafePerformIO.

Fortunately, that doesn't seem to be the case. Here's an example that is
roughly equivalent to the unsafe example in the documentation for
unsafePerformIO. Note that t1 is equivalent to readIORef [a] (actually,
t1 points out to a reference cell Ref a, which can accept values of
any type whatsoever).


--> test9 = do
--> hput t1 []
--> hput t1 [42]
--> bang <- hget t1
--> return $ (bang ::[Char])

If we uncomment the above code, we get a compiler error:

/tmp/o1.lhs:327:
No instance for (Num Char)
arising from the literal `42' at /tmp/o1.lhs:327
In the list element: 42
In the second argument of `hput', namely `[42]'


A nicer implementation of newRef (an allocator) is left for the future
work. I think that the pre-allocation trick makes it possible.

The pre-allocation scheme isn't such a limitation: clearly we can not
invoke newSTRef or newIORef arbitrary number of times (while keeping
the references). Sooner or later something unpleasant happens. We can
think therefore of newSTRef as indexing in a some pre-allocated array.
With the template Haskell, we can easily pre-allocate a heap of 640K
cells, and that should be enough for everybody.

[Ashley Yakeley]

Post by o***@pobox.com
] ] Is it possible to actually implement a working instance of RefMonad in
] ] Haskell, without making use of a built-in monad like IO or ST?
] performM :: forall a. M a -> a;
] ...because it wouldn't be type-safe: you'd be able to construct coerce
] :: a -> b just as you can with unsafePerformIO.
Fortunately, that doesn't seem to be the case.

That's only because you've failed to do the difficult part: implement
newRef. Your monadic solution has a statically typed/sized store: I'd
say it doesn't properly count as a "heap" since you can't heap new stuff
on it.

The original problem was to create an instance of

class Monad m => RefMonad m r | m -> r where
newRef :: a -> m (r a)
readRef :: r a -> m a
writeRef :: r a -> a -> m ()

without making use of IO or ST. Given some M and R that have

instance RefMonad M R
performM :: forall a. M a -> a

one can write this:

coerce :: forall a b. a -> b;
coerce a = let
{
ref = performM (newRef Nothing);
} in performM (do
{
writeRef ref (Just a);
mb <- readRef ref;
case mb of {Just b -> return b;};
});

[Tim Sweeney]

Conjecture: It's impossible to implement RefMonad directly in Haskell
without making use of built-in ST or IO functionality and without unsafe or
potentially diverging code (such as unsafeCoerce).

Any takers?

If this is true or suspected to be true, any thoughts on whether a structure
besides Monad could encapsulate safe references in Haskell without core
language changes? My intuition is that no such structure exists in Haskell
with power and flexibility equivalant to RefMonad (support for references of
arbitrary types not limited by their context.)

If this is generally thought to be impossible in Haskell, what sort of
language extensions would be needed to make this work safely, meaning
without unsafe coercions? This seems like a hairy problem. Yet it gets to
the core question of whether Haskell's monads can really implement
imperative features (such as references) in a purely functional way, or are
just a means of sequentializing those imperative constructs that are built
into the runtime.

Any solutions I can think of require a dependent-typed heap structure, and
that all references be parameterized by the heap in which they exist.

-Tim

----- Original Message -----
From: "Ashley Yakeley" <***@semantic.org>
To: <***@haskell.org>
Sent: Wednesday, June 04, 2003 5:19 PM
Subject: Re: Typesafe MRef with a regular monad

Post by Ashley Yakeley

Post by o***@pobox.com
] ] Is it possible to actually implement a working instance of RefMonad in
] ] Haskell, without making use of a built-in monad like IO or ST?
] performM :: forall a. M a -> a;
] ...because it wouldn't be type-safe: you'd be able to construct coerce
] :: a -> b just as you can with unsafePerformIO.
Fortunately, that doesn't seem to be the case.

That's only because you've failed to do the difficult part: implement
newRef. Your monadic solution has a statically typed/sized store: I'd
say it doesn't properly count as a "heap" since you can't heap new stuff
on it.
The original problem was to create an instance of
class Monad m => RefMonad m r | m -> r where
newRef :: a -> m (r a)
readRef :: r a -> m a
writeRef :: r a -> a -> m ()
without making use of IO or ST. Given some M and R that have
instance RefMonad M R
performM :: forall a. M a -> a
coerce :: forall a b. a -> b;
coerce a = let
{
ref = performM (newRef Nothing);
} in performM (do
{
writeRef ref (Just a);
mb <- readRef ref;
case mb of {Just b -> return b;};
});
--
Ashley Yakeley, Seattle WA
_______________________________________________
Haskell mailing list
http://www.haskell.org/mailman/listinfo/haskell

[Derek Elkins]

On Wed, 04 Jun 2003 15:19:53 -0700

Post by Ashley Yakeley

Post by o***@pobox.com
] ] Is it possible to actually implement a working instance of
RefMonad in ] ] Haskell, without making use of a built-in monad like
IO or ST?
] performM :: forall a. M a -> a;
] ...because it wouldn't be type-safe: you'd be able to construct
coerce ] :: a -> b just as you can with unsafePerformIO.
Fortunately, that doesn't seem to be the case.

That's only because you've failed to do the difficult part: implement
newRef. Your monadic solution has a statically typed/sized store: I'd
say it doesn't properly count as a "heap" since you can't heap new
stuff on it.

I agree, if I knew I'd have 5 components before I could just use a 5
tuple and a State monad. I'd have to look back over the other heap
stuff to see what it provides type-wise, but (at least the "new" monad
version) seems to miss the point.

Post by Ashley Yakeley
The original problem was to create an instance of
class Monad m => RefMonad m r | m -> r where
newRef :: a -> m (r a)
readRef :: r a -> m a
writeRef :: r a -> a -> m ()
without making use of IO or ST. Given some M and R that have
instance RefMonad M R
performM :: forall a. M a -> a

M = (forall s.ST s)
R = STRef s

e.g. runST :: (forall s.ST s a) -> a

you can use the same trick for your own RefMonad. I'm not sure if this
will work with RefMonad exactly. If ST/STRef can be made an instance of
RefMonad without any trouble though, then I believe it should work.

Post by Ashley Yakeley
coerce :: forall a b. a -> b;
coerce a = let
{
ref = performM (newRef Nothing);
} in performM (do
{
writeRef ref (Just a);
mb <- readRef ref;
case mb of {Just b -> return b;};
});

I was having fun with
coerce :: a -> b
coerce x = unsafePerformIO (writeIORef ref x >> readIORef ref)
where ref = unsafePerformIO (newIORef undefined)

last night, some fun examples (using GHCi 5.04.3),
data Foo a = Bar | Baz a (Foo a)

coerce 5 :: Maybe Int ==> Nothing
coerce 'a' :: Int ==> 97
coerce [1..3] :: Foo Integer ==> (Baz 1 (Baz 2 (Baz 3 Bar)))
coerce [4] :: Maybe Integer ==> Just 4

I need to reread the GHC internals paper, I want to see if I can get one
like
(coerce something :: (sometype -> someothertype)) someotherthing

[Ashley Yakeley]

Post by Derek Elkins
M = (forall s.ST s)
R = STRef s
e.g. runST :: (forall s.ST s a) -> a
you can use the same trick for your own RefMonad. I'm not sure if this
will work with RefMonad exactly. If ST/STRef can be made an instance of
RefMonad without any trouble though, then I believe it should work.

No, it won't work, fortunately ST is safe this way:

newSTRef Nothing :: forall a s. ST s (STRef s (Maybe a))

runST (newSTRef Nothing) :: -- type error, s escapes.

The type error occurs because "forall s. ST s a" cannot be matched with
"forall s. ST s E" (for some type-expression E) if E contains s (which
it does in this case).

[Tim Sweeney]

Oleg,

This is a very neat solution to providing coercion-free references in a
local environment.

I'm trying to generalize this to some sort of Monad-like typeclass, where
there is a nice mapping from Monad's to this new and more powerful
typeclass, so that one can combine typed references, IO, etc., into a single
framework.

It seems to me that your approach couldn't be generalized in this way in
Haskell, because the type of the resulting reference-using "computation"
depends on the precise set of heap operations performed there. So, for
example, you couldn't do something like:

..
a <- newRef Int 123
b <- if (some conditional) then (newRef Int) else (a)
..

Because the heap types propagated out of the conditional's two branches
differ.

The only way I can see generalizing your technique to support this sort of
thing requires a type system supporting both dependent types and subtyping.
Think the reference monad as looking somewhat like the state monad; instead
of a single piece of state, it propagates a dependent-typed pair of
(heapTypeFunc,heapValueFunc) similar in spirit to your PList construct, with
the type guaranteeing that any heap operation returns an output heapTypeFunc
that's a contravariant extension of its input heapTypeFunc.

Conjecture: Implementing type-safe (coercion-free), composable computations
over typed references isn't possible in Haskell. By composable I mean that
some operator similar in spirit to >>= on Monads can be implemented and that
computations with differing effects can occur in if-branches.

But then again, I had not thought the problem you solved using PList to be
solveable in Haskell, and am very eager to be proven wrong!

-Tim

----- Original Message -----
Back in September 2001, Koen Claessen wrote:
] 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.... I conjecture this functionality cannot be implemented
] in Haskell 98, nor in any of the known safe extensions of Haskell.

Recently, Tim Sweeney wrote
] Is it possible to actually implement a working instance of RefMonad in
] Haskell, without making use of a built-in monad like IO or ST?

The following code shows a safe and sound implementation of a
polymorphic heap with references and updates. The heap is capable of
storing of polymorphic, functional and IO values. All operations are
*statically* checked. An attempt to alter a heap reference with a
value of a mismatched type leads to a _compile-time_ error. Everything
is implemented in Haskell98 + multiparameter classes with functional
dependencies + overlapping instances. I suspect that the latter isn't
strictly needed, but it's almost midnight. Most importantly, no IO or
ST monad, no unsafePerformIO or unsafeCoerce, no existential types and
no Dynamics are needed. It seems that the polymorphic updateable heap
can be implemented safely. Although the code looks like a monadic
code, the Monad class doesn't seem to be polymorphic enough to wrap
our heap. Perhaps arrows will help.

I'd like to remark first that the ST monad with polymorphic STRef can
be implemented in Haskell98 + safe extensions _provided_ all the
values question are in the class Show/Read. When we store values,
we store their external representation. When we retrieve a value, we
read it. Similarly for values in the Binary class. All such values are
_safely_ coercible. The following code however does not make this
assumption. In our heap below, we can even store polymorphic
functions and IO values!


First, the tags for values in our heap

data Zero
data Succ a
class HeapTag a where
tag_value:: a -> Int
instance HeapTag Zero where
tag_value _ = 0
-- I just can't avoid the undefined arithmetics
instance (HeapTag t) => HeapTag (Succ t) where
tag_value _ = 1 + tag_value (undefined::t)

The heap reference is the combination of the tag and the desired
type. As we will see, the value of the second argument of the HeapRef
doesn't actually matter -- only its type does.

data HeapRef t a = HeapRef t a

Our heap is implemented as a polymorphic associative list

data Nil t v r = Nil
data Cons t v r = Cons t v r
class PList ntype ttype vtype cdrtype where
cdr:: ntype ttype vtype cdrtype -> cdrtype
empty:: ntype ttype vtype cdrtype -> Bool
value:: ntype ttype vtype cdrtype -> vtype
tag:: ntype ttype vtype cdrtype -> ttype
instance PList Nil ttype vtype cdrtype where
empty = const True
instance (PList n t v r,HeapTag tag) => PList Cons tag vtype (n t v r)

where

empty = const False
value (Cons t v r) = v
tag (Cons t v r) = t
cdr (Cons t v r) = r
class Heap t v h | t h -> v where
fetch:: (HeapRef t v) -> h -> v
alter:: (HeapRef t v) -> v -> h -> h
instance (HeapTag t,PList Cons t v r) => Heap t v (Cons t v r) where
fetch _ p = value p
alter _ vnew (Cons t v r) = (Cons t vnew r)
instance (HeapTag t,Heap t v r,PList Cons t' v' r) =>
Heap t v (Cons t' v' r) where
fetch ref p = fetch ref $ cdr p
alter ref vnew (Cons t v r) = Cons t v $ alter ref vnew r

Let's make our heap instances of a class Show, so we have something to show.

instance (PList Nil ttype vtype cdrtype) => Show (Nil ttype vtype cdrtype)
where
show _ = "[]"
instance (Show vtype, HeapTag ttype, PList Cons ttype vtype cdrtype,
Show cdrtype) =>
Show (Cons ttype vtype cdrtype)
where
show x = (show $ (tag_value $ tag x, value x)) ++ " : " ++ (show $ cdr

x)


Let's take a few simple examples

tinc (x::t) = undefined::(Succ t)
tag_one = (undefined::(Succ Zero))
acons = Cons
lst1 = acons tag_one 'a' $ Nil
lst2 = acons (tinc tag_one) 'a' $ acons tag_one True $ Nil
test1 = fetch (HeapRef tag_one 'z') lst1

The result is 'a'. We see that the value of the second argument of
HeapRef doesn't actually matter. But its type sure does: if we
uncomment the following line

-- test1' = fetch (HeapRef tag_one (1::Int)) lst1

we get an error:

/tmp/o1.lhs:127:
Couldn't match `Char' against `Int'
Expected type: Char
Inferred type: Int
When using functional dependencies to combine
Heap t v (Cons t v r),
arising from the instance declaration at /tmp/o1.lhs:91
Heap (Succ Zero) Int (Cons (Succ Zero) Char (Nil t v r)),
arising from use of `fetch' at /tmp/o1.lhs:127
When generalising the type(s) for `test1''

Indeed, the stored value is of type Char and we try to read it as an
Int.

test21 = fetch (HeapRef tag_one False) lst2
-- the latter test again makes sure that fetching is type safe
--test22' = fetch (HeapRef (tinc tag_one) False) lst2
test22 = fetch (HeapRef (tinc tag_one) (undefined::Char)) lst2
testa1 = alter (HeapRef tag_one (undefined::Bool)) False lst2
--gives: (2,'a') : (1,False) : []
testa2 = alter (HeapRef (tinc tag_one) (undefined::Char)) 'y' lst2
--gives: (2,'y') : (1,True) : []

Now we can bundle our heap with an allocation pointer

-- p is the heap, t is the next tag to allocate in p
data GHeap t p = GHeap t p
instance (HeapTag t,Show p) => Show (GHeap t p) where
show (GHeap t p) = "Global heap: alloc ptr " ++ (show$tag_value t) ++
"\n" ++ (show p)
init_gh = GHeap (undefined::Zero) Nil
fetch_gh ref (GHeap _ p) = fetch ref p
alloc_gh x (GHeap t p) = (HeapRef t x,GHeap (tinc t) (Cons t x p))
alter_gh ref newval (GHeap t p) = GHeap t $ alter ref newval p

And finally the big test. The test shows storing and altering regular
values, polymorphic function values and even IO values.

test3 = do
let heap = init_gh
let (xref,heap1) = alloc_gh 'a' heap
let (yref,heap2) = alloc_gh [(1::Int),2,3] heap1
let (zref,heap3) = alloc_gh (Just False) heap2
putStrLn "\nAfter allocations"
print heap3
putStr "x is "; print $ fetch_gh xref heap3
putStr "y is "; print $ fetch_gh yref heap3
putStr "z is "; print $ fetch_gh zref heap3
let heap31 = alter_gh xref 'z' heap3
let heap32 = alter_gh yref [] heap31
let heap33 = alter_gh zref (Just True) heap32
putStrLn "\nAfter updates"
print heap33
putStr "x is "; print $ fetch_gh xref heap33
putStr "y is "; print $ fetch_gh yref heap33
putStr "z is "; print $ fetch_gh zref heap33
putStrLn "\nPolymorphic and IO values"
let (gref,heap4) = alloc_gh (\x->x+1) heap33
let (href,heap5) = alloc_gh id heap4
let (mref,heap7) = alloc_gh (putStrLn "Monad!") heap5
putStr "g 1 is "; print $ (fetch_gh gref heap4) (1::Int)
putStr "h True is "; print $ (fetch_gh href heap5) True
putStr "h 'a' is "; print $ (fetch_gh href heap5) 'a'
putStr "m is "; (fetch_gh mref heap7)
let heap71 = alter_gh mref (putStrLn "New Monad") heap7
let heap72 = alter_gh gref (\x->x+5) heap71
putStrLn "\nAfter updates to polymorphic and IO values"
putStr "g 1 is "; print $ (fetch_gh gref heap72) (1::Int)
putStr "m is "; (fetch_gh mref heap72)
return ()

I had many occasions to see that an attempt to retrieve the value of a
wrong type or change the value with that of a wrong type result in a
compiler error! Although we are "altering" polymorphic values, the type
safeness seems to be preserved

test4 = do let heap = init_gh
let (xref,heap1) = alloc_gh [] heap
let (yref,heap2) = alloc_gh [(1::Int)] heap
let (zref,heap3) = alloc_gh [True] heap
let heap11 = alter_gh xref [(1::Int)] heap1
--let z = fetch_gh zref heap11
let z = fetch_gh zref heap1
print z

If we uncomment the commented line, we will get a type error!

The lines like
*> let (yref,heap2) = alloc_gh [(1::Int),2,3] heap1
*> let (zref,heap3) = alloc_gh (Just False) heap2

almost suggest a monad. Alas, the Monad class doesn't seem to be
polymorphic enough. The type of the >>= is
forall m b a. (Monad m) => m a -> (a -> m b) -> m b
although 'b' at the end doesn't have to be the same as 'a' at the
beginning, 'm' must be the same in the argument of >>= and in its
result. However, in our example, heap2 has a type different from that
of heap1.


ghci -fglasgow-exts -fallow-undecidable-instances
-fallow-overlapping-instances /tmp/o1.lhs

[o***@pobox.com]

Post by Keith Wansbrough
Heaps should be more dynamic than this; the (type of the) *reference*
should encode the type it points to, but the (type of the) *heap*
should not.

However, the heap can store polymorphic values. Therefore, we can use
a heap to store the polymorphic heap... Your example, slightly
re-written as follows, types

test5 = do
let heapi = init_gh
let (href,heap2) = alloc_gh undefined heapi
let (mr,heap1) =
if 1<2 then
let (xr,h) = alloc_gh 42 heapi
heap2' = alter_gh href h heap2
in (Just xr,heap2')
else
(Nothing,heap2)
print $
case mr of
Nothing -> ""
Just r -> show (fetch_gh r (fetch_gh href heap1))

and even prints the answer to everything...

[Simon Peyton-Jones]

| Conjecture: It's impossible to implement RefMonad directly in Haskell
| without making use of built-in ST or IO functionality and without
unsafe or
| potentially diverging code (such as unsafeCoerce).

A more concrete way to formulate a problem that I believe to be
equivalent is this. Implement the following interface

module TypedFM where
data FM k -- Abstract; finite map indexed by keys
of type k
data Key k a -- Abstract; a key of type k, indexing a
value of type a
=20
empty :: FM k
insert :: Ord k =3D> FM k -> k -> a -> (FM k, Key k a)
lookup :: Ord k =3D> FM k -> Key k a -> Maybe a

The point is that the keys are typed, like Refs are. But the finite map
FM is only parameterised on k, not a, so it can contain (key,value)
pairs of many different types.

I don't think this can be implemented in Haskell, even with
existentials. But the interface above is completely well typed, and can
be used to implement lots of things. What I *don't* like about it is
that it embodies the finite-map implementation, and there are too many
different kinds of finite maps.

There is, I guess, some nice language extension that would enable one to
program TypedFM, rather than provide it as primitive; but I don't know
what it is.

Simon

[Ralf Hinze]

Post by Simon Peyton-Jones
A more concrete way to formulate a problem that I believe to be
equivalent is this. Implement the following interface
module TypedFM where
data FM k -- Abstract; finite map indexed by keys
of type k
data Key k a -- Abstract; a key of type k, indexing a
value of type a
empty :: FM k
insert :: Ord k => FM k -> k -> a -> (FM k, Key k a)
lookup :: Ord k => FM k -> Key k a -> Maybe a
The point is that the keys are typed, like Refs are. But the finite map
FM is only parameterised on k, not a, so it can contain (key,value)
pairs of many different types.
I don't think this can be implemented in Haskell, even with
existentials. But the interface above is completely well typed, and can
be used to implement lots of things. What I *don't* like about it is
that it embodies the finite-map implementation, and there are too many
different kinds of finite maps.
module TypedFM
where
data FM k = FM
data Key k a = Key k a
empty = FM
insert FM k a = (FM, Key k a)
lookup FM (Key k a) = Just a

Cheers, Ralf

[Carl R. Witty]

Post by Simon Peyton-Jones
| Conjecture: It's impossible to implement RefMonad directly in Haskell
| without making use of built-in ST or IO functionality and without
unsafe or
| potentially diverging code (such as unsafeCoerce).
A more concrete way to formulate a problem that I believe to be
equivalent is this. Implement the following interface
module TypedFM where
data FM k -- Abstract; finite map indexed by keys
of type k
data Key k a -- Abstract; a key of type k, indexing a
value of type a
empty :: FM k
insert :: Ord k => FM k -> k -> a -> (FM k, Key k a)
lookup :: Ord k => FM k -> Key k a -> Maybe a
The point is that the keys are typed, like Refs are. But the finite map
FM is only parameterised on k, not a, so it can contain (key,value)
pairs of many different types.
I don't think this can be implemented in Haskell, even with
existentials. But the interface above is completely well typed, and can
be used to implement lots of things. What I *don't* like about it is
that it embodies the finite-map implementation, and there are too many
different kinds of finite maps.
There is, I guess, some nice language extension that would enable one to
program TypedFM, rather than provide it as primitive; but I don't know
what it is.

Here's a hand-waving argument that you need either Typeable (or
something else that has a run-time concrete representation of types)
or ST/STRef (or something else, probably monadic, that can track
unique objects) to do this. (Warning: there may be Haskell syntax
errors in the following; I haven't written Haskell for a while.)

Consider the following:

let (m, _) = insert empty "key" "val"
(_, k1) = insert empty "key" 'V'
(_, k2) = insert empty "key" "val"
in (lookup m k1, lookup m k2)

This gives a value of type (Maybe Char, Maybe String); I think the
intended semantics are that the value should be (Nothing, Just "val").
(Maybe the first lookup should throw an exception instead of returning
Nothing? Surely it should not return (Just 'V') or
(Just ((unsafeCoerce# 'V') :: String)). (The second lookup must
return (Just "val"); otherwise, you're breaking referential
transparency.)

Now, imagine what the map looks like in memory. Suppose it is just a
standard association list. The key cannot be just the string "key",
or the pair ("key",1) (where 1 means it's the first thing inserted
into the map); it must somehow depend on the type of the value.
Hence, you need to use Typeable or some other run-time representation
of types.

The above argument convinces me that you need run-time types to
program TypedFM. The problem in the above example is that you can
create a key in one map and attempt to use it in another map. If you
could prohibit such an attempt (or even detect it), then you wouldn't
need Typeable.

But what does it mean to use a key in "the same map"? In

let (m1, k) = insert empty "key" "val"
(m2, _) = insert m1 "key2" "val2"
in lookup m2 k

you must allow the lookup of k in m2, even though m1 and m2 are
different maps (one has a key "key2" and the other doesn't). Somehow,
a key must be usable with the map it was created in, and with
"descendents" of that map, but not with siblings of that map. In an
impure language, this could be done with some sort of tag on the map,
but I don't see how to do so in a pure language.

Following the above chain of reasoning, we could create an version of
TypedFM that was based in the IO monad. There would be a global
variable that you could use to dole out TypedFM tags; each map that
you created (in the IO monad, of course) would have a unique tag, and
keys of a map would have the same tag. You could only use the maps in
a single-threaded fashion (i.e., within the IO monad); otherwise there
would be "sibling" maps and we would be back to needing Typeable.

We could try to associate keys with their maps in some other way. For
instance, we could use the "ST" approach, and give keys and their maps
a dummy type parameter that would have to match. Even then, we would
need something monad-like to single-thread the maps.

To summarize, I believe that you need either a run-time representation
of types (like Typeable) or some way to single-thread access to your
map objects (like the ST monad) to implement something like TypedFM.
We've seen an implementation using Typeable/Dynamic. An
implementation in the ST monad might be more difficult, depending on
the intended semantics of TypedFM (what's supposed to happen if you
insert the same key with values of different types?); but for my
imagined uses of TypedFM, you could just use the ST monad with STRef's
directly.

If Typeable is necessary (and Dynamic is sufficient), or the ST monad
is necessary (and the ST monad is sufficient), then that doesn't leave
a lot of room for nice new language extensions (unless somebody can
come up with some way to single-thread objects that's even more clever
than the ST monad).

Carl Witty

[Ashley Yakeley]

Post by Carl R. Witty
Here's a hand-waving argument that you need either Typeable (or
something else that has a run-time concrete representation of types)
or ST/STRef (or something else, probably monadic, that can track
unique objects) to do this.

George Russell already showed this, didn't he? You can implement
Typeable given type-safe MRefs, and you can implement type-safe MRefs
given Typeable.

[Simon Peyton-Jones]

Oh bother, I forgot to add that you can of course insert a new value
with an old key (suitably typed) and have it overwrite. Else, as you
say, there would not be much point.

Maybe it'd be better to have a separate key-construction function=09
newKey :: k -> Key k a
instead of having insert return a key. =20

S
| -----Original Message-----
| From: Ralf Hinze [mailto:***@informatik.uni-bonn.de]
| Sent: 06 June 2003 14:12
| To: Simon Peyton-Jones; Tim Sweeney; ***@haskell.org; Ashley
Yakeley
| Subject: Re: Typesafe MRef with a regular monad
|=20
| > A more concrete way to formulate a problem that I believe to be
| > equivalent is this. Implement the following interface
| >
| > module TypedFM where
| > data FM k -- Abstract; finite map indexed by keys
| > of type k
| > data Key k a -- Abstract; a key of type k, indexing a
| > value of type a
| >
| > empty :: FM k
| > insert :: Ord k =3D> FM k -> k -> a -> (FM k, Key k a)
| > lookup :: Ord k =3D> FM k -> Key k a -> Maybe a
| >
| > The point is that the keys are typed, like Refs are. But the finite
map
| > FM is only parameterised on k, not a, so it can contain (key,value)
| > pairs of many different types.
| >
| > I don't think this can be implemented in Haskell, even with
| > existentials. But the interface above is completely well typed, and
can
| > be used to implement lots of things. What I *don't* like about it
is
| > that it embodies the finite-map implementation, and there are too
many
| > different kinds of finite maps.
|=20
| Here is a Haskell 98 implementation:
|=20
| > module TypedFM
| > where
|=20
| > data FM k =3D FM
| > data Key k a =3D Key k a
|=20
| > empty =3D FM
| > insert FM k a =3D (FM, Key k a)
| > lookup FM (Key k a) =3D Just a
|=20
| Cheers, Ralf
|=20

[Ralf Hinze]

Post by Simon Peyton-Jones
Oh bother, I forgot to add that you can of course insert a new value
with an old key (suitably typed) and have it overwrite. Else, as you
say, there would not be much point.
Maybe it'd be better to have a separate key-construction function
newKey :: k -> Key k a
instead of having insert return a key.
S

Seriously, isn't this just an application of dynamics? The key
type allows us to insert a cast when looking up a data structure
of dynamic values?

Cheers, Ralf

[Simon Peyton-Jones]

Yes, one *could* use dynamic types. But the check would always succeed!
That suggests a lack in the static type system. It's not surprising:
the soundness depends on the un-forgeability of keys. So it's
reasonable that there should be some language extension. I'm just
looking for the minimal such extension. Finite maps see a bit of a big
hammer.

Simon

| -----Original Message-----
| From: Ralf Hinze [mailto:***@informatik.uni-bonn.de]
| Sent: 06 June 2003 14:29
| To: Simon Peyton-Jones; Tim Sweeney; ***@haskell.org; Ashley
Yakeley
| Subject: Re: Typesafe MRef with a regular monad
|=20
| Am Freitag, 6. Juni 2003 15:23 schrieb Simon Peyton-Jones:
| > Oh bother, I forgot to add that you can of course insert a new value
| > with an old key (suitably typed) and have it overwrite. Else, as
you
| > say, there would not be much point.
| >
| > Maybe it'd be better to have a separate key-construction function
| > newKey :: k -> Key k a
| > instead of having insert return a key.
| >
| > S
|=20
| Seriously, isn't this just an application of dynamics? The key
| type allows us to insert a cast when looking up a data structure
| of dynamic values?
|=20
| Cheers, Ralf
|=20

[Ralf Hinze]

Post by Simon Peyton-Jones
Yes, one *could* use dynamic types. But the check would always succeed!

Why is that? If I overwrite an entry with a value of a different type,
then the check fails. I am certainly missing something ...

Cheers, Ralf

[Simon Peyton-Jones]

You can't overwrite an entry with a value of a different type, because
the keys are typed! Any more than you can overwrite an IORef with a
value of a different type.
S

| -----Original Message-----
| From: Ralf Hinze [mailto:***@informatik.uni-bonn.de]
| Sent: 06 June 2003 15:01
| To: Simon Peyton-Jones; Tim Sweeney; ***@haskell.org; Ashley
Yakeley
| Subject: Re: Typesafe MRef with a regular monad
|=20
| Am Freitag, 6. Juni 2003 15:47 schrieb Simon Peyton-Jones:
| > Yes, one *could* use dynamic types. But the check would always
succeed!
|=20
| Why is that? If I overwrite an entry with a value of a different type,
| then the check fails. I am certainly missing something ...
|=20
| Cheers, Ralf
|=20

[Ralf Hinze]

Post by Simon Peyton-Jones
You can't overwrite an entry with a value of a different type, because
the keys are typed! Any more than you can overwrite an IORef with a
value of a different type.
S

Why is that? Ok, here is my second implementation. It uses the
Dynamic module from our HW2002 paper. A key is a pair consisting
of the actual key and a type representation.

Post by Simon Peyton-Jones
module TypedFM
where
import Prelude hiding (lookup)
import qualified Prelude
import Dynamics
data FM k = FM [(k, Dynamic)]
data Key k a = Key k (Type a)
empty :: FM k
empty = FM []
insert :: (Typable a) => FM k -> k -> a -> (FM k, Key k a)
insert (FM bs) k a = (FM ((k, Dyn rep a) : bs), Key k rep)
lookup :: (Eq k) => FM k -> Key k a -> Maybe a
lookup (FM bs) (Key k rep) = case Prelude.lookup k bs of
Nothing -> Nothing
Just dy -> cast dy rep
update :: (Typable b) => FM k -> Key k a -> b -> (FM k, Key k b)
update (FM bs) (Key k _) b = (FM ((k, Dyn rep b) : bs), Key k rep)

Does this fit the bill?

Cheers, Ralf

[Keith Wansbrough]

Post by Ralf Hinze
Why is that? Ok, here is my second implementation. It uses the
Dynamic module from our HW2002 paper. A key is a pair consisting
of the actual key and a type representation.

[..]

Post by Ralf Hinze

Post by Simon Peyton-Jones
update :: (Typable b) => FM k -> Key k a -> b -> (FM k, Key k b)
update (FM bs) (Key k _) b = (FM ((k, Dyn rep b) : bs), Key k rep)

Does this fit the bill?

No, because update shouldn't return a new key, it should allow reuse
of the same key. Restating Simon PJ's original signature, and adding
update:

module TypedFM where
data FM k -- Abstract; finite map indexed bykeys of type k
data Key k a -- Abstract; a key of type k, indexing a value of type a

empty :: FM k
insert :: Ord k => FM k -> k -> a -> (FM k, Key k a)
lookup :: Ord k => FM k -> Key k a -> Maybe a
update :: Ord k => FM k -> Key k a -> a -> FM k

If updating gives you a new key, then you might as well just store the
value in the key. Instead, you keep the same key; and so you'd better
remain type-compatible.

--KW 8-)

[Ken Shan]

Post by Simon Peyton-Jones
module TypedFM where
data FM k -- Abstract; finite map indexed bykeys of type k
data Key k a -- Abstract; a key of type k, indexing a value of type a
empty :: FM k
insert :: Ord k => FM k -> k -> a -> (FM k, Key k a)
lookup :: Ord k => FM k -> Key k a -> Maybe a
update :: Ord k => FM k -> Key k a -> a -> FM k
If updating gives you a new key, then you might as well just store the
value in the key. Instead, you keep the same key; and so you'd better
remain type-compatible.

Discussing this with Oleg, I realized that this signature is not sound.

(fm1, key) = insert empty 42 undefined
value_in = 1 :: Int
fm2 = update fm1 key value_in
Just value_out = lookup fm2 key :: Char

[Simon Marlow]

... So it's reasonable that there should be some language extension.=20
I'm just looking for the minimal such extension.

unsafeCoerce# is quite a minimal extension :-)

Cheers,
Simon

[Lennart Augustsson]

Post by Simon Marlow

... So it's reasonable that there should be some language extension.
I'm just looking for the minimal such extension.

unsafeCoerce# is quite a minimal extension :-)

It's a minimal extension, but it's not an extension that provides any
insight. :)

-- Lennart

[o***@pobox.com]

update :: (Typable b) => FM k -> Key k a -> b -> (FM ...)

I didn't know constraints on values are allowed... Given below is the
implementation of the required interface, in Haskell98

module TypedFM where
data FM k -- Abstract; finite map indexed bykeys of type k
data Key k a -- Abstract; a key of type k, indexing a value of type a

empty :: FM k
insert :: Ord k => FM k -> k -> a -> (FM k, Key k a)
lookup :: Ord k => FM k -> Key k a -> Maybe a
update :: Ord k => FM k -> Key k a -> a -> FM k


Implementation:

import Monad

data U = LBool Bool
| LChar Char
| LInt Int
| LL [U] -- Lists of any kind
| LA (U->U) -- monomorophic functions of any kind


class UNIV a where
inj:: a -> U
prj:: U -> Maybe a


instance UNIV Bool where
inj = LBool
prj (LBool a) = Just a
prj _ = Nothing

instance UNIV Char where
inj = LChar
prj (LChar a) = Just a
prj _ = Nothing

instance UNIV Int where
inj = LInt
prj (LInt a) = Just a
prj _ = Nothing

instance (UNIV a) => UNIV [a] where
inj = LL . map inj
prj (LL as) = foldr f (Just []) as
where f e (Just s) = case prj e of
Just x -> Just $ x:s
_ -> Nothing
f _ _ = Nothing
prj _ = Nothing

instance (UNIV a,UNIV b) => UNIV (a->b) where
inj f = LA $ \ua -> let (Just x) = prj ua in inj $ f x
prj (LA f) = Just $ \x -> let Just y = prj$f$inj x in y
prj _ = Nothing

data FM k = FM [U]

data Key k a = Key Int a

empty = FM []

insert (FM l) _ a = (FM $(inj a):l, Key (length l) a)

lookp:: (UNIV a) => FM k -> Key k a -> Maybe a
lookp (FM l) (Key i a) = prj $ (reverse l)!!i

update:: (UNIV a) => FM k -> Key k a -> a -> FM k
update (FM l) (Key i _) a = FM $ reverse (lb ++ ((inj a):(tail lafter)))
where (lb,lafter) = splitAt i (reverse l)


test1 = do
let heap = empty
let (heap1,xref) = insert heap () 'a'
let (heap2,yref) = insert heap1 () [(1::Int),2,3]
let (heap3,zref) = insert heap2 () "abcd"
putStrLn "\nAfter allocations"
-- print heap3

putStr "x is "; print $ lookp heap3 xref
putStr "y is "; print $ lookp heap3 yref
putStr "z is "; print $ lookp heap3 zref

let heap31 = update heap3 xref 'z'
let heap32 = update heap31 yref []
let heap33 = update heap32 zref "new string"
putStrLn "\nAfter updates"

putStr "x is "; print $ lookp heap33 xref
putStr "y is "; print $ lookp heap33 yref
putStr "z is "; print $ lookp heap33 zref

putStrLn "\nFunctional values"
let (heap4,gref) = insert heap33 () (\x->x+(1::Int))
putStr "g 1 is "; print $ liftM2 ($) (lookp heap4 gref) $ Just (1::Int)
return ()

[Derek Elkins]

On Tue, 10 Jun 2003 11:44:45 -0700 (PDT)

Post by o***@pobox.com

update :: (Typable b) => FM k -> Key k a -> b -> (FM ...)

I didn't know constraints on values are allowed... Given below is the
implementation of the required interface, in Haskell98

They aren't presumably as that would (as you and another have shown)
make the implementation more or less trivial. With constraints
you can have a type a -> b (the type of unsafeCoerce) only it's
meaningful and safe as the values are constrained (as opposed to saying
'give me anything and I'll give you whatever you want') The question
(at least to me) is more, 'you can satisfy the RefMonad interface with
STRefs or IORefs, but those use "imperative" features under the hood;
can it be satisfied without them?' Personally, I think Tim Sweeney is
focusing on the wrong aspect. The problem here has nothing to do with
monads, it's purely a typing issue, you can have monads in Scheme and
you could definitely satisfy that interface (in the pure subset) as
implicitly everything is in class Typeable. Simon PJ pointed this out
best by changing the question to how to make a "polymorphic" finite map.
That's not to say that arrows, comonads, or monads, or something else
don't have a place (they might not though) as STRefs/IORefs are only
type safe because they are in a monad, or perhaps you can look at it
another way and they aren't safe at all but monads simply make it
impossible to abuse them, in which case unsafeCoerce is likely the
minimal extension, again this just shows that this is purely a type
issue, unsafeCoerce has nothing to do with monads and I don't think most
would consider it an imperative feature (though a common feature in
imperative languages ;).

[Koen Claessen]

Derek Elkins wrote:

| The question (at least to me) is more, 'you can
| satisfy the RefMonad interface with STRefs or IORefs,
| but those use "imperative" features under the hood;
| can it be satisfied without them?'

As I showed in the message that spawned off this discussion,
this is indeed possible to do (unless you think any monad by
itself is an imperative thing). The only thing one needs to
focus on is the typing and not the imperativeness.

/Koen.

--
Koen Claessen
http://www.cs.chalmers.se/~koen
Chalmers University, Gothenburg, Sweden.

[Derek Elkins]

On Wed, 11 Jun 2003 09:19:46 +0200 (MET DST)

Post by Koen Claessen
| The question (at least to me) is more, 'you can
| satisfy the RefMonad interface with STRefs or IORefs,
| but those use "imperative" features under the hood;
| can it be satisfied without them?'
As I showed in the message that spawned off this discussion,
this is indeed possible to do (unless you think any monad by
itself is an imperative thing). The only thing one needs to
focus on is the typing and not the imperativeness.
/Koen.

Hence the very next sentence,
"Personally, I think Tim Sweeney is
focusing on the wrong aspect. The problem here has nothing to do with
monads, it's purely a typing issue,"

and the last sentence,

"[...]STRefs/IORefs are only
type safe because they are in a monad, or perhaps you can look at it
another way and they aren't safe at all but monads simply make it
impossible to abuse them, in which case unsafeCoerce is likely the
minimal extension, again this just shows that this is purely a type
issue, unsafeCoerce has nothing to do with monads and I don't think most
would consider it an imperative feature (though a common feature in
imperative languages ;)."

[Koen Claessen]

Someone asked me:

| I don't recall the message you are referring to, and I
| can't find it in the archive. Can you point me at it?

Sorry, I meant:

http://www.haskell.org/pipermail/haskell/2001-September/007922.html

/K :-)

[Keith Wansbrough]

Post by Ashley Yakeley

Post by Carl R. Witty
Here's a hand-waving argument that you need either Typeable (or
something else that has a run-time concrete representation of types)
or ST/STRef (or something else, probably monadic, that can track
unique objects) to do this.

George Russell already showed this, didn't he? You can implement
Typeable given type-safe MRefs, and you can implement type-safe MRefs
given Typeable.

But George Russell's implementation relied on looking up something in
one map with a key obtained from another map. I thought type-safe
MRefs should disallow this.

--KW 8-)

[Carl R. Witty]

Post by Keith Wansbrough

Post by Ashley Yakeley

Post by Carl R. Witty
Here's a hand-waving argument that you need either Typeable (or
something else that has a run-time concrete representation of types)
or ST/STRef (or something else, probably monadic, that can track
unique objects) to do this.

George Russell already showed this, didn't he? You can implement
Typeable given type-safe MRefs, and you can implement type-safe MRefs
given Typeable.

But George Russell's implementation relied on looking up something in
one map with a key obtained from another map. I thought type-safe
MRefs should disallow this.

If you use Simon PJ's type signatures, you can't really disallow using
a key from one map with another map.

Carl Witty

[Simon Peyton-Jones]

| If you use Simon PJ's type signatures, you can't really disallow using
| a key from one map with another map.

Yes, that's a good point. So there are really three issues:
a) single-threaded-ness=20
b) making sure you look up in the right map
c) making sure the thing you find has the right type

Even if you have typed keys, (Key a), then if you look them up in the
wrong map, any guarantee that it maps to a value of type 'a' is out of
the window. I can think of two solutions
i) Guarantee that keys are unique across all maps,=20
so that a key from one map is never in the domain of another.

ii) Use the (ST s) and (STRef s) trick, to connect the key with
the map.
This seems cleaner, but demands more of the programmer.

But my main point remains: that some form of typed finite map ought to
exist that does no dynamic type checks, because none are necessary.
This must be a terribly old problem; and unsafeCoerce seems like a
rather brutal "solution". =20

Simon

[Ralf Hinze]

Post by Simon Peyton-Jones
a) single-threaded-ness
b) making sure you look up in the right map
c) making sure the thing you find has the right type
Even if you have typed keys, (Key a), then if you look them up in the
wrong map, any guarantee that it maps to a value of type 'a' is out of
the window.

Not true, if you use the finite map implementation based on dynamics.
Here, the story is: with single-threaded-ness you can omit the dynamic
type checks (they are guaranteed to succeed); if you use finite maps
in a persistent manner, this is no longer true.

Cheers, Ralf