o***@pobox.com

2003-06-03 07:22:48 UTC

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

type. As we will see, the value of the second argument of the HeapRef

doesn't actually matter -- only its type does.

HeapRef doesn't actually matter. But its type sure does: if we

uncomment the following line

/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.

values, polymorphic function values and even IO values.

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

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

] 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 desireddata 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)

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 listdata 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.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

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 exampleswhere

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)

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 oftag_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

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-- 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) : []

-- 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 regulardata 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

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 alet 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 ()

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!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

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