Jay Cox wrote:
I'm trying to learn more about Explicit Universal Quantification so I decide to run the following supposedly correct code from the ghc user guide:
module Dummy where
import ST
newtype TIM s a = TIM (ST s (Maybe a))
runTIM :: (forall s. TIM s a) -> Maybe a runTIM t = case t of {TIM l -> runST l} <...> so, is this a bug?
No, it is correct and expected behaviour, as I will explain below.
I noticed also the following code compiles fine. (slightly modified from a message on this list titled "Re: Type problem with ST monad" dating April 23, 1999
module Dummy where
import ST
newtype TIM s a = TIM (ST s (Maybe a))
runTIM :: (forall s. TIM s a) -> Maybe a runTIM t = runST (deTIM t)
deTIM (TIM t) = t
Perfect example for explanation of the problem. The difference is between
runTIM t = case t of {TIM l -> runST l} and runTIM t = runST (deTIM t) deTIM (TIM t) = t
In the last one, after the type checker has verified that deTIM is type-correct, it can safely generalize the type of deTIM, because it is a top-level function. This means that if we have f :: a -> String f x = "Hello, world" we are allowed to apply f to an Int in one place, and to an Char in another place: g :: (String, String) g = (f 3, f 'a') This is common and well-known behaviour, and it's possible to prove that this never gives problems. However, in
runTIM t = case t of {TIM l -> runST l} the argument 't' is non-generic. If we have the function g :: (a -> String) -> (String, String) g f = (f 3, f 'a') a problem appears. 'f' is used in a generic way, being applied to arguments of different types, which is not allowed because if we have h = f (\x -> show (x + 1)) the second part of the tupel is undefined, though this would be type-correct. This is clearly undesirable. So we have to restrict f to be non-generic.
Consequently, types of variables which are derived from it must be non-generic as well. In particular this applies to 'l'. Thus, 'l' can't be generalized to fit in the type of runST. With this burden of information about generic and non-generic, we can say in short:
runTIM t = case t of {TIM l -> runST l} is wrong because l CANNOT be generalized to fit the type of runST. runTIM t = runST (deTIM t) deTIM (TIM t) = t is correct because deTIM CAN be generalized, so it fits the type of runST
Rijk-Jan van Haaften