Safe and sound STRef [Was Implementing RefMonads in Haskell without ST,IO]
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
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-)
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...
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.
In article <200306042005.h54K5mG0014203@adric.fnmoc.navy.mil>, oleg@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
On Wed, 04 Jun 2003 15:19:53 -0700 Ashley Yakeley <ashley@semantic.org> wrote:
In article <200306042005.h54K5mG0014203@adric.fnmoc.navy.mil>, oleg@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
In article <20030604200734.00006d9e.ddarius@hotpop.com>, Derek Elkins <ddarius@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
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" <ashley@semantic.org> To: <haskell@haskell.org> Sent: Wednesday, June 04, 2003 5:19 PM Subject: Re: Typesafe MRef with a regular monad
In article <200306042005.h54K5mG0014203@adric.fnmoc.navy.mil>, oleg@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
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
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
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
participants (5)
-
Ashley Yakeley -
Derek Elkins -
Keith Wansbrough -
oleg＠pobox.com -
Tim Sweeney