Fri, 12 May 2000 00:42:52 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> newSTRef :: a -> ST s (STRef s a)
> readSTRef :: STRef s a -> ST s a
> and
>
> f:: STRef s a -> STRef s a
> f v = runST( newSTRef v >= \w -> readSTRef w)
>
> Let's start
>
> v has type STRef s a
...for "s" and "a" coming from the instantiation of a polymorphic
function "f". Yes.
> newSTRef v has type ST s (STRef s (STRef s a))
> (THIS is of the form ST s (STRef s T(s))
No. It has the type
ST s1 (STRef s1 (STRef s a))
where "s1" is free (thus can be later generalized over) and "s" and
"a" come from the environment inside "f" (thus are monomorphic).
It would have the type you wrote if "v" was created in this thread.
> > > Now forall s1. ( ST s1 T(s)) IMPLIES forall s . ( ST s T(s) )
> >
> > It does not. And I have already told why, a few e-mails ago.
>
> IT DOES : that is a well known rule of forall (forall x,y . alpha(x.y) =>
> forall x. alpha(x,x) )
I see no "forall s" in the left type.
> > When you use runST, you don't always know if the type given for "s"
> > will be instantiated to a type variable or not. Being a type variable
> > is not a property of a type.
>
> I can only say here : ???????????????
runST':: ST s Int -> Int
runST' x = ...
Inside the body of runST' "x" has the type "ST s Int", with "s"
taken from the environment.
When runST' will be later applied to a value of the type "ST s Int"
with "s" free, "x" will have the type "ST s Int" with nothing more
known about "s". (If runST was applied to this value directly, it
would be OK.)
When runST' will be applied to a value of the type "ST RealWorld Int",
"x" will have the type "ST RealWorld Int".
But you have to compile runST' _now_, and decide whether the first
argument of ST from the type of "x" is a type variable.
Haskell does not have this problem. It does not ever check if a type
is a type variable, but if it is a _free_ type variable, i.e. one
that can be generalized over.
> > > > runST':: forall s. ST s Int -> Int
> > > > runST' x = runST x
> > > >
> > > > Should it compile with your type of runST?
> function runST are fullfilled . So ("my") runST will work.
Now I write
len :: Int
len = runST' (liftM length (readFile "foo") :: ST RealWorld Int)
which creates a global value of type Int which changes in time. Oops!
--
__("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a23 C+++$ UL++>++++$ P+++ L++>++++$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e>++++ h! r--%>++ y-
