Hi,<br><br><div class="gmail_quote"><div class="gmail_quote"><div class="Ih2E3d"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div>> I just found out that it *is* possible to implement the inside function,<br>
> namely as follows:<br>
><br>
> > inside :: forall t. ((forall a. Wrapper (t a))-> Wrapper (forall a. (t<br>
> > a)))<br>
> > inside x = Wrapper f<br>
> > where f :: forall a. (t a)<br>
> > f = unwrap x<br>
> > unwrap (Wrapper z) = z<br>
><br>
> I guess this solves my problem. Sorry for bothering you with this question.<br>
> I still find it a bit weird to write all these obfuscated identity functions<br>
> to make the type checker happy, though.<br>
<br>
</div>As I said, the types are not isomorphic -- it you think of type<br>
parameters as arguments you will see why.</blockquote></div><div><br>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:<br>
<br>-----<br>{-# LANGUAGE Rank2Types #-}<br><br>-- Wrapper<br>newtype W a = W { unW :: a }<br><br>inside :: ((forall a. W (t a))-> W (forall a. (t a)))<br>--inside (W x) = W x -- (a) FAILS<br>--inside = W . unW -- (b) FAILS<br>
inside x = W (unW x) -- (c) WORKS<br>-----<br><br>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?<br>
<br>Thanks,<br>Sean<br></div></div>
</div>