On Sat, Oct 25, 2008 at 11:55 PM, Paul L wrote:

Tnaks for the clarification, please see my further questions below

On 10/25/08, Daniel Fischer wrote:

...

Sure, (g (flip readArray 0)) :: ST s Int, or, explicitly, forall s. ST s Int, there's nothing to restrict the s, so it's legitimate to pass it to runST.

..[snipped]..

...

What would be a generic mapST, which type should it have?

I tried this type for mapST, it doesn't work:

mapST :: (a -> ST s b) -> [a] -> [b] mapST f (x:xs) = runST (f x) : mapST f xs mapST f [] = []

By your reasoning, (f x) should have type forall s . ST s b, and should match what runST expects, but apparently GHC complains about it. Why?

From the perspective of code inside the definition of mapST, f is not

The problem is that the type variable s is determined by the caller of mapST. If you write the type with explicit foralls, you get: mapST :: forall a b s. (a -> ST s b) -> [a] -> [b] polymorphic, because a, b, and s have already been determined. The type you need is, mapST :: forall a b. (forall s. a -> ST s b) -> [a] -> [b] Now runST is able to pass an arbitrary type for s to f. (GHC can silently convert between "forall s. a -> ST s b" and "a -> forall s. ST s b".) It may be helpful to rewrite the types with a more explicit notation. For example, runST :: (a :: *) -> ((s :: *) -> ST s a) -> a mapST_wrong :: (a :: *) -> (b :: *) -> (s :: *) -> (f :: a -> ST s b) -> [a] -> [b] mapST_right :: (a :: *) -> (b :: *) -> (f :: (s :: *) -> a -> ST s b) -> [a] -> [b] -- Dave Menendez http://www.eyrie.org/~zednenem/

On Sun, Oct 26, 2008 at 8:17 AM, Paul L wrote:

Thanks very much for the explanation, I now have a better understanding.

I'm glad I could help.

On 10/26/08, David Menendez wrote: ..[snipped]..

...

It may be helpful to rewrite the types with a more explicit notation. For example,

runST :: (a :: *) -> ((s :: *) -> ST s a) -> a

mapST_wrong :: (a :: *) -> (b :: *) -> (s :: *) -> (f :: a -> ST s b) -> [a] -> [b] mapST_right :: (a :: *) -> (b :: *) -> (f :: (s :: *) -> a -> ST s b) -> [a] -> [b]

Is this the kind syntax? Very cool indeed!

If you're referring to the kind signatures feature in GHC, then no, although the use of * is related. It's actually a way of writing dependent products, which generalize foralls and the function arrow. This particular syntax is used by Agda, but I've also seen it in some proposals to add limited dependent types to Haskell. I've found it very helpful in understanding how universal and existential quantification behave, because it treats the type and value parameters uniformly. -- Dave Menendez http://www.eyrie.org/~zednenem/