<div class="gmail_quote">On Tue, Jan 20, 2009 at 1:14 PM, David Menendez <span dir="ltr"><<a href="mailto:dave@zednenem.com">dave@zednenem.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="Ih2E3d">On Tue, Jan 20, 2009 at 2:51 PM, Mauricio <<a href="mailto:briqueabraque@yahoo.com">briqueabraque@yahoo.com</a>> wrote:<br>
>>> But how is this:<br>
>>> data SomeNum = forall a. SN a<br>
>>> different from:<br>
>>> data SomeNum = SN (forall a. a)<br>
><br>
>> At a glance they look the same to me — but only the first is accepted by<br>
>> ghc.<br>
><br>
> Following the link you pointed in the last<br>
> message, I found this at <a href="http://8.8.4.1" target="_blank">8.8.4.1</a>:<br>
><br>
> data T a = T1 (forall b. b -> b -> b) a</div></blockquote><div><br></div><div>The constructor here is irrelevant. The function here can do anything a top-level function of type:</div><div><br></div><div>something :: b -> b -> b </div>
<div><br></div><div>I like to think about quantification in this regard in terms of isomorphisms. Think about what a function of type forall b. b -> b -> b can do. It cannot do anything with its arguments, because it must work on all types, so it only has one choice to make: it can return the first argument, or it can return the second argument.</div>
<div><br></div><div>So, forall b. b -> b -> b is isomorphic to Bool.</div><div><br></div><div>For symmetry, the constructor T1 has type:</div><div><br></div><div>T1 :: (forall b. b -> b -> b) -> a -> T1 a</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="Ih2E3d"><br><br>
> If I understand properly, it can be activated<br>
> with -XPolymorphicComponents. It's different<br>
> from my example, but I would like to know what<br>
> it does that this can't:<br>
> </div></blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="Ih2E3d">
> data T a = forall b. T1 (b->b->b) a</div></blockquote><div><br></div><div>The constructor T1 here has type:</div><div><br></div><div>T1 :: forall b. (b -> b -> b) -> a -> T1 a</div><div><br></div><div>
See the difference?</div><div><br></div><div>You can pass the latter a function of any type you choose, eg. (Int -> Int -> Int) or ((Bool -> Bool) -> (Bool -> Bool) -> (Bool -> Bool)). So when somebody gets a T from you, they have no idea what type the function you gave it was, so they can only use it in limited ways (in this case, nothing useful at all can be done with it).</div>
<div><br></div><div>Here's another existential type:</div><div><br></div><div>data T' a = forall b. T' (b -> a) b</div><div> </div><div>Here, a T' contains a value of some type b -- who knows what it is -- and a function to get from that value to an a. Since we don't know anything about b, all we can do is to apply the function.</div>
<div><br></div><div>T' a is isomorphic to a. But it might have different operational behavior; e.g. maybe a is a huge list which is cheaply generated from some small generator value (of type b). Then if you pass a T' around, it's the same as passing that big list around, except for you <span class="Apple-style-span" style="font-style: italic;">don't</span> cache the results of the list, improving memory performance. It's like inverse memoization.</div>
<div><br></div><div>Not all existential types are for inverse memoization, this is just one case.</div><div><br></div><div>I found it easiest to reason about these with the types of the constructors, and thinking about what non-quantified type they are isomorphic to.</div>
<div><br></div><div>Luke</div></div>