Hello everyone, I recently found myself attempting to use ST at the base of a stack of transformers, ala: type Test t r = ErrorT String (ST t) r I imagined, given the type of ST, that I would need a run function along the lines of: runTest :: (forall t. Test t r) -> Either String r (which was, in fact, exactly what I wanted). Unfortunately, even with that type signature, I can't find a way to convince the compiler that the state thread is properly universal in the call to runST. Is it possible to write this function, or is ST (and other monads that use its style of threading) not transformable? Thanks, /g -- It is myself I have never met, whose face is pasted on the underside of my mind.
Hi J Garrett, I don't see any problem in GHC 6.6. with:
runTest c = runST (runErrorT c)
*Main> runTest (return True) Loading package mtl-1.0 ... linking ... done. Right True *Main> On the other hand, I try to define it firstly as below and got the following error.
runTest = runST . runErrorT
Couldn't match expected type `forall t. Test t r' against inferred type `ErrorT e m a' Expected type: (forall t. Test t r) -> forall s. ST s a1 Inferred type: ErrorT e m a -> m (Either e a) In the second argument of `(.)', namely `runErrorT' In the expression: runST . runErrorT Rank-2 types seem to interact badly with (.) and ($), but my type theory educated neuron doesn't know why. I think this is folklore knowledge? Cheers pepe On 22/12/2006, at 18:26, J. Garrett Morris wrote:
Hello everyone,
I recently found myself attempting to use ST at the base of a stack of transformers, ala:
type Test t r = ErrorT String (ST t) r
I imagined, given the type of ST, that I would need a run function along the lines of:
runTest :: (forall t. Test t r) -> Either String r
(which was, in fact, exactly what I wanted). Unfortunately, even with that type signature, I can't find a way to convince the compiler that the state thread is properly universal in the call to runST. Is it possible to write this function, or is ST (and other monads that use its style of threading) not transformable?
Thanks, /g
-- It is myself I have never met, whose face is pasted on the underside of my mind. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Fri, Dec 22, 2006 at 06:44:54PM +0100, Pepe Iborra wrote:
Rank-2 types seem to interact badly with (.) and ($), but my type theory educated neuron doesn't know why. I think this is folklore knowledge?
You say:
runErrSt = (.) runST runErrorT
runErrorT has type ErrorT e m a -> m (Either e a) runST has type (forall s. ST s a) -> a (.) has type (b -> c) -> (a -> b) -> (a -> c) since runST is the first argument to (.), we must unify (forall s. ST s a) with b Quoting the GHC Manual:
There is one place you cannot put a forall: you cannot instantiate a type variable with a forall-type. So you cannot make a forall-type the argument of a type constructor. So these types are illegal:
I am not aware of why this restriction exists, but it is a consequence of a documented restriction. (I hear rumors about limited support for "left-to-right impredicative instantiation" in GHC HEAD, but it's way over my head :( )
Hmm, that was simpler than I had imagined. Thank you both!
/g
On 12/22/06, Stefan O'Rear
On Fri, Dec 22, 2006 at 06:44:54PM +0100, Pepe Iborra wrote:
Rank-2 types seem to interact badly with (.) and ($), but my type theory educated neuron doesn't know why. I think this is folklore knowledge?
You say:
runErrSt = (.) runST runErrorT
runErrorT has type ErrorT e m a -> m (Either e a) runST has type (forall s. ST s a) -> a (.) has type (b -> c) -> (a -> b) -> (a -> c)
since runST is the first argument to (.), we must unify (forall s. ST s a) with b
Quoting the GHC Manual:
There is one place you cannot put a forall: you cannot instantiate a type variable with a forall-type. So you cannot make a forall-type the argument of a type constructor. So these types are illegal:
I am not aware of why this restriction exists, but it is a consequence of a documented restriction. (I hear rumors about limited support for "left-to-right impredicative instantiation" in GHC HEAD, but it's way over my head :( )
-- It is myself I have never met, whose face is pasted on the underside of my mind.
participants (3)
-
J. Garrett Morris -
Pepe Iborra -
Stefan O'Rear