Re: Typesafe MRef with a regular monad
Keith Wansbrough [EMAIL PROTECTED] wrote in article [EMAIL PROTECTED] in gmane.comp.lang.haskell.general: 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. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Typesafe MRef with a regular monad
| 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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
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. 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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
In article [EMAIL PROTECTED], [EMAIL PROTECTED] (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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
In article [EMAIL PROTECTED], [EMAIL PROTECTED] (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-) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
Keith Wansbrough [EMAIL PROTECTED] writes: In article [EMAIL PROTECTED], [EMAIL PROTECTED] (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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
Simon Peyton-Jones [EMAIL PROTECTED] writes: | Conjecture: It's impossible to implement RefMonad directly in Haskell | without making use of built-in ST or IO functionality and without unsafe or | potentially diverging code (such as unsafeCoerce). A more concrete way to formulate a problem that I believe to be equivalent is this. Implement the following interface module TypedFM where data FM k -- Abstract; finite map indexed by keys of type k data Key k a-- Abstract; a key of type k, indexing a value of type a empty :: FM k insert :: Ord k = FM k - k - a - (FM k, Key k a) lookup :: Ord k = FM k - Key k a - Maybe a The point is that the keys are typed, like Refs are. But the finite map FM is only parameterised on k, not a, so it can contain (key,value) pairs of many different types. I don't think this can be implemented in Haskell, even with existentials. But the interface above is completely well typed, and can be used to implement lots of things. What I *don't* like about it is that it embodies the finite-map implementation, and there are too many different kinds of finite maps. There is, I guess, some nice language extension that would enable one to program TypedFM, rather than provide it as primitive; but I don't know what it is. Here's a hand-waving argument that you need either Typeable (or something else that has a run-time concrete representation of types) or ST/STRef (or something else, probably monadic, that can track unique objects) to do this. (Warning: there may be Haskell syntax errors in the following; I haven't written Haskell for a while.) Consider the following: let (m, _) = insert empty key val (_, k1) = insert empty key 'V' (_, k2) = insert empty key val in (lookup m k1, lookup m k2) This gives a value of type (Maybe Char, Maybe String); I think the intended semantics are that the value should be (Nothing, Just val). (Maybe the first lookup should throw an exception instead of returning Nothing? Surely it should not return (Just 'V') or (Just ((unsafeCoerce# 'V') :: String)). (The second lookup must return (Just val); otherwise, you're breaking referential transparency.) Now, imagine what the map looks like in memory. Suppose it is just a standard association list. The key cannot be just the string key, or the pair (key,1) (where 1 means it's the first thing inserted into the map); it must somehow depend on the type of the value. Hence, you need to use Typeable or some other run-time representation of types. The above argument convinces me that you need run-time types to program TypedFM. The problem in the above example is that you can create a key in one map and attempt to use it in another map. If you could prohibit such an attempt (or even detect it), then you wouldn't need Typeable. But what does it mean to use a key in the same map? In let (m1, k) = insert empty key val (m2, _) = insert m1 key2 val2 in lookup m2 k you must allow the lookup of k in m2, even though m1 and m2 are different maps (one has a key key2 and the other doesn't). Somehow, a key must be usable with the map it was created in, and with descendents of that map, but not with siblings of that map. In an impure language, this could be done with some sort of tag on the map, but I don't see how to do so in a pure language. Following the above chain of reasoning, we could create an version of TypedFM that was based in the IO monad. There would be a global variable that you could use to dole out TypedFM tags; each map that you created (in the IO monad, of course) would have a unique tag, and keys of a map would have the same tag. You could only use the maps in a single-threaded fashion (i.e., within the IO monad); otherwise there would be sibling maps and we would be back to needing Typeable. We could try to associate keys with their maps in some other way. For instance, we could use the ST approach, and give keys and their maps a dummy type parameter that would have to match. Even then, we would need something monad-like to single-thread the maps. To summarize, I believe that you need either a run-time representation of types (like Typeable) or some way to single-thread access to your map objects (like the ST monad) to implement something like TypedFM. We've seen an implementation using Typeable/Dynamic. An implementation in the ST monad might be more difficult, depending on the intended semantics of TypedFM (what's supposed to happen if you insert the same key with values of different types?); but for my imagined uses of TypedFM, you could just use the ST monad with STRef's directly. If Typeable is necessary (and Dynamic is sufficient), or the ST monad is necessary (and the ST monad is sufficient), then that doesn't leave a lot of room for nice new language extensions (unless somebody can come up with some way to single-thread objects that's even more clever than
Re: Typesafe MRef with a regular monad
Derek Elkins wrote: | The question (at least to me) is more, 'you can | satisfy the RefMonad interface with STRefs or IORefs, | but those use imperative features under the hood; | can it be satisfied without them?' As I showed in the message that spawned off this discussion, this is indeed possible to do (unless you think any monad by itself is an imperative thing). The only thing one needs to focus on is the typing and not the imperativeness. /Koen. -- Koen Claessen http://www.cs.chalmers.se/~koen Chalmers University, Gothenburg, Sweden. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
Someone asked me: | I don't recall the message you are referring to, and I | can't find it in the archive. Can you point me at it? Sorry, I meant: http://www.haskell.org/pipermail/haskell/2001-September/007922.html /K :-) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
On Wed, 11 Jun 2003 09:19:46 +0200 (MET DST) Koen Claessen [EMAIL PROTECTED] 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 ;). ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
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 () ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
On Tue, 10 Jun 2003 11:44:45 -0700 (PDT) [EMAIL PROTECTED] 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 ;). ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
Ralf Hinze writes: 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-) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Typesafe MRef with a regular monad
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 :-) Cheers, Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
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. 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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Typesafe MRef with a regular monad
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 | -Original Message- | From: Ralf Hinze [mailto:[EMAIL PROTECTED] | Sent: 06 June 2003 14:12 | To: Simon Peyton-Jones; Tim Sweeney; [EMAIL PROTECTED]; Ashley Yakeley | Subject: Re: Typesafe MRef with a regular monad | | 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. | | 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 | ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
Am Freitag, 6. Juni 2003 15:23 schrieb Simon Peyton-Jones: Oh bother, I forgot to add that you can of course insert a new value with an old key (suitably typed) and have it overwrite. Else, as you say, there would not be much point. Maybe it'd be better to have a separate key-construction function newKey :: k - Key k a instead of having insert return a key. S Seriously, isn't this just an application of dynamics? The key type allows us to insert a cast when looking up a data structure of dynamic values? Cheers, Ralf ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Typesafe MRef with a regular monad
Yes, one *could* use dynamic types. But the check would always succeed! That suggests a lack in the static type system. It's not surprising: the soundness depends on the un-forgeability of keys. So it's reasonable that there should be some language extension. I'm just looking for the minimal such extension. Finite maps see a bit of a big hammer. Simon | -Original Message- | From: Ralf Hinze [mailto:[EMAIL PROTECTED] | Sent: 06 June 2003 14:29 | To: Simon Peyton-Jones; Tim Sweeney; [EMAIL PROTECTED]; Ashley Yakeley | Subject: Re: Typesafe MRef with a regular monad | | Am Freitag, 6. Juni 2003 15:23 schrieb Simon Peyton-Jones: | Oh bother, I forgot to add that you can of course insert a new value | with an old key (suitably typed) and have it overwrite. Else, as you | say, there would not be much point. | | Maybe it'd be better to have a separate key-construction function | newKey :: k - Key k a | instead of having insert return a key. | | S | | Seriously, isn't this just an application of dynamics? The key | type allows us to insert a cast when looking up a data structure | of dynamic values? | | Cheers, Ralf | ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
Am Freitag, 6. Juni 2003 15:47 schrieb Simon Peyton-Jones: Yes, one *could* use dynamic types. But the check would always succeed! Why is that? If I overwrite an entry with a value of a different type, then the check fails. I am certainly missing something ... Cheers, Ralf ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Typesafe MRef with a regular monad
You can't overwrite an entry with a value of a different type, because the keys are typed! Any more than you can overwrite an IORef with a value of a different type. S | -Original Message- | From: Ralf Hinze [mailto:[EMAIL PROTECTED] | Sent: 06 June 2003 15:01 | To: Simon Peyton-Jones; Tim Sweeney; [EMAIL PROTECTED]; Ashley Yakeley | Subject: Re: Typesafe MRef with a regular monad | | Am Freitag, 6. Juni 2003 15:47 schrieb Simon Peyton-Jones: | Yes, one *could* use dynamic types. But the check would always succeed! | | Why is that? If I overwrite an entry with a value of a different type, | then the check fails. I am certainly missing something ... | | Cheers, Ralf | ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
Am Freitag, 6. Juni 2003 16:09 schrieb Simon Peyton-Jones: You can't overwrite an entry with a value of a different type, because the keys are typed! Any more than you can overwrite an IORef with a value of a different type. S Why is that? Ok, here is my second implementation. It uses the Dynamic module from our HW2002 paper. A key is a pair consisting of the actual key and a type representation. module TypedFM where import Prelude hiding (lookup) import qualified Prelude import Dynamics data FM k = FM [(k, Dynamic)] data Key k a = Key k (Type a) empty :: FM k empty = FM [] insert:: (Typable a) = FM k - k - a - (FM k, Key k a) insert (FM bs) k a= (FM ((k, Dyn rep a) : bs), Key k rep) lookup:: (Eq k) = FM k - Key k a - Maybe a lookup (FM bs) (Key k rep)= case Prelude.lookup k bs of Nothing - Nothing Just dy - cast dy rep update:: (Typable b) = FM k - Key k a - b - (FM k, Key k b) update (FM bs) (Key k _) b= (FM ((k, Dyn rep b) : bs), Key k rep) Does this fit the bill? Cheers, Ralf ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Typesafe MRef with a regular monad
In fact I think these Typesafe MRef's are exactly equivalent 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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
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 [EMAIL PROTECTED]
To: [EMAIL PROTECTED]
Sent: Wednesday, June 04, 2003 5:19 PM
Subject: Re: Typesafe MRef with a regular monad
In article [EMAIL PROTECTED],
[EMAIL PROTECTED] 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
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
On Wed, 04 Jun 2003 15:19:53 -0700
Ashley Yakeley [EMAIL PROTECTED] wrote:
In article [EMAIL PROTECTED],
[EMAIL PROTECTED] 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
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Typesafe MRef with a regular monad
In article [EMAIL PROTECTED], Derek Elkins [EMAIL PROTECTED] 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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
