> On 26-Apr-2000, Jan Brosius <[EMAIL PROTECTED]> wrote:
> > Hi,
> >
> > First I give the following primitive operations
> >
> > newVar :: a -> ST s (MutVar s a)
> >
> > readVar :: MutVar s a -> ST s a
> >
> > writeVar :: MutVar s a -> a -> ST s ()
> >
> > Next consider the function
> >
> > f :: MutVar s a -> Mut Var s a
> >
> > f v = runST (newVar v `thenST` \w ->
> >
> > readVar w)
> >
> > 1. What is the type given to newVar v by the typechecker?
>
> Let's see... `v' has type `MutVar s a', and after renaming apart
> `newVar' has type `forall a2,s2 . a2 -> ST s2 (MutVar s2 a2)',
> so, substituting `Mutvar s a' for `a2', we see that
> `newVar v' has type `forall s2 . ST s2 (MutVar s2 (MutVar s a))'.
>
> --
Ok, Next recall
runST :: forall s. (ST s a) -> a
and let runST1 give the type signature
runST1 :: ST s a -> a
consider
v = runST1 ( newVar True)
Then newVar True gets the type ST s (MutVar s a)
( I prefer the more sloppy notation without a forall as it gives less
clutter).
In runST1 :: ST s a -> a
Let us substitute a by say MutVar s a
we then get after renaming the s in runST1 by s2
ST s2 ( MutVar s a ) -> MutVar s a )
Have we finished ? One would say no : one needs a substitution for s2 , If
we
don't "cheat" we must now substitute s2 by s and we get
ST s (MutVar s) -> MutVar s a
In principle this is not the type of runST.
Because technically the "domain" of runST is of the form
ST s a where a is never of the form T(s)
Finally consider
runST :: forall s . ( ST s a) -> a
What to do now ? let us first substitute a by MutVar s a as shown above.
After renaming there remains
forall s2 . ( ST s2 (MutVar s a)) -> MutVar s a
What is now the meaning of the forall s2 above? If it means that s2 can be
substituted then we must substitute it by s But that is not what one wants :
one wants s2 to remain non free.
Where I wanted to come is this:
give runST the type signature
runST :: exists s . ( ST s a ) -> a
and technically we have also a bounded variable s. What is the reason for
choosing
forall against exists ? I think there is no reason for it. But I can be
wrong.
Friendly
Jan Brosius
