On Sun, Oct 26, 2008 at 8:17 AM, Paul L
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