more detailed explanation about forall in Haskell

[Jan Brosius]

Hi,   According to the reactions that I have received I feel the need to explain in more detail my email in mime type entitled : about the abuse of forall in Haskell. The easiest thing for me would be to send an attachment in pdf to the Haskell - mailing list. But I guess this is impossible.     1. Let ' s rehearse some things w.r.t. my first email. As you know I used the following notation for substitution : if  x  is a variable ,  T  a term (say type or say set) and  alpha  is a formula, that is a logical phrase , a logical assertion then I define by :           (T | x ) alpha   the (new) formula beta obtained by substituting in alpha every free occurrence of the variable x by  T . For example   let        Alpha == [forall x. (A x )] x   then  ( T | x ) alpha becomes         [forall x. ( A x) ]  T   This example shows at the same time that it is best to rename before substitution  of x by T , every  bound occurrence of x in alpha by a (new) variable(s)   that is (are) neither a free variable of alpha nor a free variable of T .   Of course it is (better for reading) to have different names for all different bound variables ocurring in alpha and in T.   An example might explain better the above tactic:   E.g. suppose T == [forall x. ST x [forall x. STRef x a]] x   Then first change T to the equivalent form      T==[forall u. ST u [ forall s. STRef s a]] x   Next let aplha be of the form     alpha==[forall x. forall s in Free ( x ) . (x =/s ) ] x =/ x   Then before the substitution ( T | x ) alpha   rename eventually all bound variables in T and alpha   e.g.      T == [forall u. ST u [forall s. STRef s a]] x   and     alpha == [forall v. [forall w in Free ( v ). ( v =/w )]] x =/ x   Then  ( T | x ) alpha becomes   (T|x)alpha == [forall v. [forall w in Free (v ). (v=/w)]] T=/ T     (I hope that in the above no typo's got in).     2. Next let me point out once and for all that logical quantifiers are used only in logical formula's . The disobedience of this rule means necessarily a departure from the logical meaning of a quantifier . PERIOD .   3.Next look at some Haskell functions and the use of the forall's there.   a. good use:              id :: forall a . a -> a                      id x = x             id2 :: forall s,a . (s,a) -> (s.a)                     id2 (x, y ) = (x,y)    readSTRef :: forall s,a . STRef s a -> ST s a    b.  bad use :     newSTRef:: forall s.a . a -> ST s STRef s a   This type signature MUST be replaced by   newSTRef:: forall a. [forall s ni Free ( a ) .  a -> ST s STRef s a] where  Forall s ni Free(a)  means " forall s not being a free variable (occurring in ) of a "   c. illigitimate use :   runST :: forall a. ( forall s. ST s a ) -> a     3. The why   b. This is because in reality the function newSTRef is meant to be used only in cases where s is not a free variable of a.   b1. e.g.  we KNOW that the following code will "work"    f :: forall s, a . STRef s a -> STRef s a    f v = runST( newSTRef v >=  \w -> readSTRef w )     let the type of v be STRef s a  ,  then the type of newSTRef v is not meant to be something of the form   ST s (STRef s (STRef s a))   because then the type of readSTRef w would become   ST s STRef s a   and we KNOW that this should not be a good argument of the function runST.   Because  f v is supposed to WORK we can hope that the type of readSTRef given above is correct.(to be honest I don't know) I deduced this from another working little program  "swap" in the paper entitled "lazy functional state threads"     So the correct type signature of newSTRef must be:   newSTRef :: forall a . [forall s ni Free(a) . a -> ST s (STRef s a)]   Let's see what happens when type of v = STRef s a. Then the type of newSTRef v becomes: after renaming bound variables first and after substituting a in newSTRef by STRef s a : and after the following steps:   first newSTRef "becomes" (admitted this is a bit loose)   forall s1 ni Free( STRef s a) .  [STRef s a  -> ST s1 (STRef s1 (STRef s a))]   and since s is a free variable in STRef s a the type of newSTRef v becomes   ST s1 (STRef s1 (STRef s a))    WITH the additional information given to the  typechecker (?) that now s1 is a variable that will never be allowed to get instantiated to s , i.e. s1 =/ s.   This remark is important, indeed suppose that forall x,y . alpha(x,y) is a true formula then alpha(x,y) is a true formula and also alpha(x,x) is a true formula !!!   Next  the type of w becomes STRef s1 (STRef s a) and the type of readSTRef w becomes   ST s1 (STRef s a)  WITH  s1 =/ s   and this is an acceptable type for the argument of runST (VERY loosely indicated by forall s . ST s a )     That is runST will deliver something of the type STRef s a     Finally remark that , if we would have given for id2 the type signature   id2 :: forall a . [forall s ni Free ( a )  .(s,a) -> (s,a)]   we would have excluded the possibility that the image of id2 could become of type  (s.s).   c.  forall s. ST s a   is illigitimate since you can not form a logical phrase with it (It is not supposed to be known that ST s a   is in reality implemented as a function.).   There are 2 ways to circumvent this problem.   c1. Use a new free variable binder ,e.g. `b ,for types to mean the following:     `b s. ST s a   is the type of  ALL ST s a  with the EXCEPTION of all types of the form  ST s T(s)   and then give runST the type signature   runST :: forall a. (`b s . ST s a) -> a   c2. Use the following type signature for runST   runST :: forall a. [forall s ni Free( a ) . ST s a -> a]     If we are supposed to know that IO a = ST World a then use the signature   runST :: forall a. [forall Variable ( s ) ni Free ( a ) . ST s a -> a ]   where Variable (s) means " s is a type variable".   Since Variable (World) is not true , the above type signature will not allow that runST accepts  types of the form IO a as argument.     4. If it were possible to interrogate the typechecker in the following way :     typeOf (x) = typeOf (y)   then it would be possible to give a direct definition of runST.   5. Using `b as defined above we could give now the following type signature for newSTRef   newSTRef :: forall a . a -> (`b s. ST s (STRef s a))   Here  `b s. ST s (STRef s a)  will mean the type of ALL ST s (STRef s a)  with the EXCEPTION of any type of the form ST s (STRef s T(s))     As we can see  `b  appears as a type restrictor.     Thanks for reading , sorry for the typo's.   Very Friendly, Jan Brosius     PS: I have the impression that no notice is taken of the remarks given in my first email. I hope the Haskell committee will take notice of these remarks after reading these more detailed explanation. It is a bit sad that I cannot send a pdf form as an attachment . This would allow better  reading and better checking for typo's .