[Haskell-cafe] problem using ST monad

David Menendez dave at zednenem.com
Sun Oct 26 13:30:59 EDT 2008


On Sun, Oct 26, 2008 at 8:17 AM, Paul L <ninegua at gmail.com> 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 <dave at zednenem.com> 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>


More information about the Haskell-Cafe mailing list