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 [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell