[Haskell-cafe] Moving "forall" over type constructors

[Sean Leather]

Hi,

> 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.


I found these examples interesting, mostly because I don't understand it
very well. So, I simplified Klaus' code a bit and derived the following:

-----
{-# LANGUAGE Rank2Types #-}

-- Wrapper
newtype W a = W { unW :: a }

inside :: ((forall a. W (t a))-> W (forall a. (t a)))
--inside (W x) = W x -- (a) FAILS
--inside = W . unW -- (b) FAILS
inside x = W (unW x) -- (c) WORKS
-----

Can someone comment on the differences between the following in terms of
type-checking or inference? Considering the errors I got, I'm guess the
issue is the same for the pattern-matching (a) and the point-free (b)
versions. Are there any pointers for developing a better understanding or
intuition of this?

Thanks,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080609/28cff892/attachment.htm