On Sun, Oct 26, 2008 at 8:17 AM, Paul L <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
