On Wed, Sep 16, 2009 at 11:58 AM, Cristiano Paris <span dir="ltr"><<a href="mailto:frodo@theshire.org">frodo@theshire.org</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="im">On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>> wrote:<br>
> Here's the difference between these two types:<br>
><br>
> test1 :: forall a. a -> Int<br>
> -- The caller of test1 determines the type for test1<br>
> test2 :: (forall a. a) -> Int<br>
> -- The internals of test2 determines what type, or types, to instantiate the<br>
> argument at<br>
<br>
</div>I can easily understand your explanation for test2: the type var a is<br>
closed under existential (?) quantification. I can't do the same for<br>
test1, even if it seems that a is closed under universal (?)<br>
quantification as well.<br></blockquote><div><br>Both are universally quantified, but at a different level. To look at it in System F-land, you have two levels of types that can get passed in lambdas. Explicitly:<br><br>
Haskell:<br>> test1 :: forall a. a -> Int<br>> test1 _ = 1<br>> test2 :: (forall a. a) -> Int<br>> test2 x = x<br><br>explicitly in System F:<br><br>test1 = /\a \(x :: a). 1<br>test2 = \(x :: forall a. a). x @Int<br>
<br>/\ is type-level lambda, and @ is type-level application.<br><br>In test1, the caller specifies "a" and then passes in an object of that type.<br>In test2, the caller must pass in an object which is of all types, and test2 asks for that object to be instantiated at the type "Int"<br>
<br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="im">> Or, to put it another way, since there are no non-bottom objects of type<br>
> (forall a. a):<br>
<br>
</div>Why?<br></blockquote><div><br>Informally, because you can't create something that can be any type. For example, what could the result of<br><br>test3 :: (forall a. a) -> Int<br>test3 x = length (x `asTypeOf` [()])<br>
<br>be? How could you call it?<br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="im">> test1 converts *anything* to an Int.<br>
<br>
</div>Is the only possible implementation of test1 the one ignoring its<br>
argument (apart from bottom of course)?<br></blockquote><div><br>There's one way that doesn't entirely ignore its argument.<br><br>test4 x = seq x 1<br><br>But I don't like to talk about that one :)<br><br> -- ryan<br>
</div></div><br>