Safe and sound STRef [Was Implementing RefMonads in Haskell without ST,IO]
ol...@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
The following is the statically typed polymorphic heap itself:
> 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.
More tests:
> 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
Testing alternation:
> 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
_______________________________________________
Haskell mailing list
Has...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Keith Wansbrough
> 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-)
ol...@pobox.com
> 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...
ol...@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]
A pre-allocated heap of 5 cells:
> 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
A Heap monad:
> 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
We can run our monad:
> 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
ol...@pobox.com wrote:
> 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.
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;};
});
--
Ashley Yakeley, Seattle WA
Tim Sweeney
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
Derek Elkins
Ashley Yakeley <ash...@semantic.org> wrote:
> In article <200306042005....@adric.fnmoc.navy.mil>,
> ol...@pobox.com wrote:
>
> > 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.
>
> 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.
> 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.
> 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;};
> });
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
Derek Elkins <dda...@hotpop.com> wrote:
> 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).
--
Ashley Yakeley, Seattle WA
_______________________________________________
Tim Sweeney
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
we get an error:
More tests:
Testing alternation:
_______________________________________________
Simon Peyton-Jones
| 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.
Simon
Ralf Hinze
> 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.
Here is a Haskell 98 implementation:
> 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
Simon Peyton-Jones
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
| -----Original Message-----
| From: Ralf Hinze [mailto:ra...@informatik.uni-bonn.de]
| Sent: 06 June 2003 14:12
| To: Simon Peyton-Jones; Tim Sweeney; has...@haskell.org; Ashley
Yakeley
| Subject: Re: Typesafe MRef with a regular monad
|
Ralf Hinze
> 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?
Simon Peyton-Jones
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:ra...@informatik.uni-bonn.de]
| Sent: 06 June 2003 14:29
| To: Simon Peyton-Jones; Tim Sweeney; has...@haskell.org; Ashley
Yakeley
| Subject: Re: Typesafe MRef with a regular monad
|
Ralf Hinze
> 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 ...
Simon Peyton-Jones
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:ra...@informatik.uni-bonn.de]
| Sent: 06 June 2003 15:01
| To: Simon Peyton-Jones; Tim Sweeney; has...@haskell.org; Ashley
Yakeley
| Subject: Re: Typesafe MRef with a regular monad
|
Ralf Hinze
> 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.
> 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?
George Russell
to dynamic types. In other words, if you've got one,
you've got the other. Ralf Hinze has just shown that
if you have dynamic types you can implement Typesafe MRef.
The reverse implementation would be something like
> data Dynamic = FM ()
>
> toDyn :: a -> Dynamic
> toDyn a = insert empty () a
>
> fromDynamic :: Dynamic -> Maybe a
> fromDynamic fm =
> let
> bogus :: Key () a
> (_,bogus) = insert empty () undefined
> in
> lookup fm bogus
Keith Wansbrough
> 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.
[..]
> > 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-)
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 :-)
Cheers,
Simon
Lennart Augustsson
>Simon P.J. writes:
>
>
>
>>... 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
ol...@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
ol...@pobox.com wrote:
>
> > 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
| 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.
Koen Claessen
| 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 :-)
Derek Elkins
Koen Claessen <ko...@cs.chalmers.se> wrote:
> 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.
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 ;)."
_______________________________________________
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. (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
cwi...@newtonlabs.com (Carl R. Witty) wrote:
> 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.
--
Ashley Yakeley, Seattle WA
_______________________________________________
Keith Wansbrough
> cwi...@newtonlabs.com (Carl R. Witty) wrote:
>
> > 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
> > In article <v4j7k7q...@newtonlabs.com>,
> > cwi...@newtonlabs.com (Carl R. Witty) wrote:
> >
> > > 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
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,
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".
Simon
Ralf Hinze
> 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
Ken Shan
> 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
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
* "Harry Potter is a sexist neo-conservative autocrat."
-- Pierre Bruno, Liberation (cf. ISBN 1-85984-666-1)
* Return junk mail in the postage-paid response envelope included.
* Insert spanners randomly in unjust capitalist machines.