About the abuse of forall in Haskell

[Jan Brosius]

Hi,   1. First I think , even if it is a bit boring, to rehearse some basic logical notions. I have based my logic course on the logic of N. Bourbaki : Theory of Sets. In this completely formal logic the quantifiers  "exists" and "forall"  are constructed as follows:   One introduces in the logic an operator called   Tau  ( the Greek letter t) that I shall represent as  " `t " . Let now alpha be a formula that contains the variable x, then   `t x (alpha)  represents an object  written as follows:                    `t x (alpha) is written like  `t (alpha) where every occurrence of x in alpha is replaced by a small square tied with a line                                      to `t  ; e.g. let alpha be  x  `elem y  then `t x (alpha) is  `t  ( `sq `elem  y ) where `sq denotes the small square symbol.                                                                       tied to (imagine it) the symbol `t .   Next  let us define                   (exists x) alpha  by : [ `t x (alpha)  |  x ] (alpha)  where  ( T | x ) (alpha) is by definition the formal string of symbols obtained by substituting                                                                                             in alpha every occurrence of x by T.   Next  forall is defined formally by:                  (forall x) alpha  ==  `not (exists x) ( `not alpha )     2. Then recall that if e.g. alpha is a formula containing two variables  x  and  y then :                     ( forall x  ) (forall y ) alpha(x,y)  is equivalent with (forall y) ( forall x ) apha(x,y)  is equivalent with  alpha(x,y)   i.e. if ( forall x ) (forall y) alpha(x,y) is true then alpha(x,y) is true  and reversely, and as a consequence alpha(x.x) and (forall x) [alpha(x,x)] is true .   3. The foregoing was boring enough so let us come to the point.      As we know       f :: a -> b   is the type signature of a function with a variable domain a  and a variable image y .   If we write  forall a,b f :: a -> b the we get a logical sentence that one can read as follows : " forall a and b f is a function of a into b "   We see immediately that this can never be a true sentence. Indeed what we really have defined is a family  of functions f(a.b) indexed by a and b and then the sentence becomes : " forall a and b, f(a.b) is a function of a into b ". However given this remark we can all live with the less cluttered version  forall a,b f :: a -> b. Further Haskell prefers to put the forall 's at the left of the sign  :: . We then write  f  ::  forall a,b . a -> b     We can all live with that. And since even this version gives too much clutter  I even prefer the notation   f  ::  a -> b   4. Finally , let us consider the point that intrigued me most, the typing of runST,    runST :: (forall s . ST s a ) -> a   What sort of sentence could be meant by this?  I had to look at the type rules and at the examples in the corresponding paper to conclude that technically the meaning of   forall s . ST s a     was to  define the domain of  runST   as follows :  runST  excepts  as argument  everything of the form   ST s a with the sole restriction  of anything having the type   ST s T(s)  . Indeed suppose that a has type say T(s) then the type of  of the argument  of runST  should  be written  as  (forall s1 . ST s1 T(s) ). I admit that I have been a bit loose in the foregoing phrase, but I hope to explain this better in the example that will follow . First I want to end this with the following observation : if  the  forall  in  ( forall s1 . ST s1 T(s) )  really had the meaning of  the logical  forall  , that is  if "  forall s1 . ST s1 T(s) is  true  then  the case ST s T(s)   i.e.  the case for s1 = s is also true. This is certainly not what we want.   I then thought maybe another non symbol than forall should be used here. So, I thought of something like                                                                                   `t s . ST s a   The inconvenience was that `t is allready used solely for formula's. Then I thought to replace it   by  `b s . ST s a  where `b  stand for the Greek letter b and where  `b s . ST s a   formally   gives   `b ( ST `sq a ) where one imagines that  `sq  is tied with a line to `b  . This new type should then be interpreted by  "  all of ST s a  with the sole exception  of everything of the form  ST s T(s) .   However after considering the example:                                  f  ::  STRef s a  -> STRef s a    ( in the paper MutVar s a  is replaced by STRef s a)                                f v = runST ( newSTRef v >>= \w -> readSTRef w )  (in the paper runST ( newVar v `thenST` \w -> readVar w )  )   OK, let us look at the type of   newSTRef v . Recall that                                newSTRef :: forall s,a . a -> ST s STRef s a   First remark   s  doesn't range over all types but only over the types of State (see paper ) , thus actually we  should write  forall State s .  forall a but since State is not a variable " set " we have commutativity of the bounded quantifier  forall State s and the (unbounded) quantifier forall a . Ok let us drop State and go on ( we can live with that).   Since  v  has  the type  STRef s a   then  newSTRef v shall have the type   forall s1 . ST s1 STRef s a. Now we really have a problem , if a logical  forall was meant  then why should the case  s1 = s  i.e.  ST s STRef s a   not be acceptable, but if we accept this case then runST will have the wrong argument . Since the f v will run  I suppose the typechecker gives something of the form   ST s1 STRef s a   for the type of  newSTRef v. So, we are in a real mess, and we have to conclude that in fact the type signature of newSTRef  was wrongly written down. However there is an acceptable solution.  first define a new logical " term "   FreeV (a) " that means the ( finite ) set  of " free variables in a " , and define  ni  in                              s  ni FreeV (a )   by  " s is not in FreeV(a) "  Then rewrite the type signature of newSTRef as follows                           newSTRef :: forall a . forall s ni FreeV( a ) . a -> ST s STRef s a   Next note that the 2 forall 's cannot commute anymore . Now the type of newSTRef v becomes                                             forall s1 ni FreeV ( ST s STRef s a)   and now the typechecker is forced to choose a new variable say  s1  so that the type of newSTRef v  becomes  ST s1 STRef s a  as we want to have it.   If we accept this we can now give the following type signature for runST   runST :: forall a . forall s ni FreeV( a ) .  ST s a -> a   and there is no need anymore for something as "  runST :: ( `b s . ST s a )  -> a   even  as defining new types with  `b looks mathematically appealing.   Oof .  Thanks for reading  and sorry for the typo's   Friendly Jan Brosius