Moving "forall" over type constructors
At first I'd like to thank Claus, Ryan, Edsko, Luke and Derek for their quite helpful replies to my previous thread. In the course of following their advice I encountered the problem of moving a "forall" quantifier over a wrapper type constructor. If I have
newtype Wrapper a = Wrapper a
and I instantiate Wrapper with a polymorphic type, then it is possible to move the quantifier outside:
outside :: Wrapper (forall a. (t a)) -> (forall a. Wrapper (t a)) outside(Wrapper x) = Wrapper x
(surprisingly the code does not work with the implementation 'outside x = x'; I guess this is a ghc bug) However, the other way around does not work:
inside :: (forall a. Wrapper (t a))-> Wrapper (forall a. (t a)) inside x= x
results in the following error: Couldn't match expected type `forall a. t a' against inferred type `t a' Expected type: Wrapper (forall a1. t a1) Inferred type: Wrapper (t a) In the expression: x In the definition of `inside': inside x = x Any ideas on how to make this work? Klaus
On Mon, Jun 09, 2008 at 03:20:33PM +0200, Klaus Ostermann wrote:
At first I'd like to thank Claus, Ryan, Edsko, Luke and Derek for their quite helpful replies to my previous thread.
In the course of following their advice I encountered the problem of moving a "forall" quantifier over a wrapper type constructor.
If I have
newtype Wrapper a = Wrapper a
and I instantiate Wrapper with a polymorphic type, then it is possible to move the quantifier outside:
outside :: Wrapper (forall a. (t a)) -> (forall a. Wrapper (t a)) outside(Wrapper x) = Wrapper x
(surprisingly the code does not work with the implementation 'outside x = x'; I guess this is a ghc bug)
Not a bug; those two types are not the same. In the code you've given, ghc needs to find evidence that it can create a element of type (Wrapper (t a)) for any any; fortunately, it can do so because it has 'x', which can create a 't a' for any 'a'.
inside :: (forall a. Wrapper (t a))-> Wrapper (forall a. (t a)) inside x= x
results in the following error:
But here we have an argument that can return a Wrapper (t a) for any 'a'; that does *not* mean it can return a wrapper of a polymorphic type. If you think about 'a' as an actual argument, then you could pass 'Int' to get a Wrapper (t Int), Bool to get a wrapper (t Bool), or even (forall a. a -> a) to get a Wrapper (t (forall a. a -> a)), but no argument at all could make a Wrapper (forall a. t a). Edsko
But here we have an argument that can return a Wrapper (t a) for any 'a'; that does *not* mean it can return a wrapper of a polymorphic type. If you think about 'a' as an actual argument, then you could pass 'Int' to get a Wrapper (t Int), Bool to get a wrapper (t Bool), or even (forall a. a -> a) to get a Wrapper (t (forall a. a -> a)), but no argument at all could make a Wrapper (forall a. t a).
I just found out that it *is* possible to implement the inside function, namely as follows:
inside :: forall t. ((forall a. Wrapper (t a))-> Wrapper (forall a. (t a))) inside x = Wrapper f where f :: forall a. (t a) f = unwrap x unwrap (Wrapper z) = z
I guess this solves my problem. Sorry for bothering you with this question. I still find it a bit weird to write all these obfuscated identity functions to make the type checker happy, though. Klaus -- View this message in context: http://www.nabble.com/Moving-%22forall%22-over-type-constructors-tp17732668p... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
On Mon, Jun 09, 2008 at 06:55:20AM -0700, Klaus Ostermann wrote:
But here we have an argument that can return a Wrapper (t a) for any 'a'; that does *not* mean it can return a wrapper of a polymorphic type. If you think about 'a' as an actual argument, then you could pass 'Int' to get a Wrapper (t Int), Bool to get a wrapper (t Bool), or even (forall a. a -> a) to get a Wrapper (t (forall a. a -> a)), but no argument at all could make a Wrapper (forall a. t a).
I just found out that it *is* possible to implement the inside function, namely as follows:
inside :: forall t. ((forall a. Wrapper (t a))-> Wrapper (forall a. (t a))) inside x = Wrapper f where f :: forall a. (t a) f = unwrap x unwrap (Wrapper z) = z
I guess this solves my problem. Sorry for bothering you with this question. I still find it a bit weird to write all these obfuscated identity functions to make the type checker happy, though.
As I said, the types are not isomorphic -- it you think of type parameters as arguments you will see why. Edsko
participants (2)
-
Edsko de Vries -
Klaus Ostermann