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

[Edsko de Vries]

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