On Thu, Sep 17, 2009 at 6:59 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;">
On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram <<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>> wrote:<br>
> ...<br>
<div class="im">> 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>
</div>Ok. But let me be pedantic: where is the universal quantification in<br>
test1? It seems to me the a is a free variable in test1 while being<br>
closed under universal quantification in test2.<br></blockquote><div class="im"><br>The universal quantification is right in the extra lambda: it works for all types "a".<br><br>Just like this works on all lists [a]:<br>
<br>length = /\a. \(xs :: [a]). case xs of { [] -> 0 ; (x:ys) -> 1 + length @a ys }<br><br>Here are some uses of test1:<br><br>v1 = test1 @Int 0<br>v2 = test1 @[Char] "hello"<br>v3 = test1 @() ()<br><br>Here's a use of test2:<br>
<br>v4 = test2 (/\a. error @a "broken")<br><br>given error :: forall a. String -> a<br><br> -- ryan<br></div></div><br>