<div><span class="gmail_quote">It seems you've already figured this out, but here's a quick counterexample:</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">> {-# LANGUAGE ExistentialQuantification, RankNTypes #-}</span></div>
<div><span class="gmail_quote">> module Box where</span></div>
<div><span class="gmail_quote">> data Box = forall a. B a</span></div>
<div><span class="gmail_quote">></span></div>
<div><span class="gmail_quote">> --mapBox :: forall a b. (a -> b) -> Box -> Box -- incorrect type</span></div>
<div><span class="gmail_quote">> mapBox f (B x) = B (f x)</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">then:</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">> boxedInt :: Box</span></div>
<div><span class="gmail_quote">> boxedInt = B (1 :: Int)</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">> f :: [Int] -> Int</span></div>
<div><span class="gmail_quote">> f = sum</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">mf :: Box -> Box</span></div>
<div><span class="gmail_quote">mapBox f -- this is well-typed according to the specified type of "mapBox"</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">But,</span></div>
<div><span class="gmail_quote"></span><span class="gmail_quote">mf boxedInt :: Box</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">mf boxedInt</span></div>
<div><span class="gmail_quote">= mapBox f boxedInt</span></div>
<div><span class="gmail_quote">= mapBox sum (B (1 :: Int))</span></div>
<div><span class="gmail_quote">= B (sum (1 :: Int))</span></div>
<div><span class="gmail_quote">which is not well-typed.</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">The least specific type for MapBox is</span></div>
<div><span class="gmail_quote">
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">> mapBox :: forall b. (forall a. (a -> b)) -> Box -> Box</span></div></span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">There are non-bottom functions of this type, for example:</span></div>
<div><span class="gmail_quote"> const (1 :: Int) :: forall a. a -> Int</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">With this type,</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">> ok :: Box</span></div>
<div><span class="gmail_quote">> ok = mapBox (const 1) (B "hello")</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">is well-typed.</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote"> -- ryan</span></div>
<div><span class="gmail_quote"></span> </div>
<div><span class="gmail_quote">On 11/30/07, <b class="gmail_sendername">Pablo Nogueira</b> <<a href="mailto:pirelo@googlemail.com">pirelo@googlemail.com</a>> wrote:</span></div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">A question about existential quantification:<br><br>Given the existential type:<br><br>data Box = forall a. B a
<br><br>in other words:<br><br>-- data Box = B (exists a.a)<br>-- B :: (exists a.a) -> Box<br><br>I cannot type-check the function:<br><br>mapBox :: forall a b. (a -> b) -> Box -> Box<br>-- :: forall a b. (a -> b) -> (exists
a.a) -> (exists a.a)<br>mapBox f (B x) = B (f x)<br><br>Nor can I type check:<br><br>mapBox :: forall a. (a -> a) -> Box -> Box<br>-- :: forall a. (a -> a) -> (exists a.a) -> (exists a.a)<br>
mapBox f (B x) = B (f x)<br><br>The compiler tells me that in both functions, when it encounters the<br>expression |B (f x)|, it cannot unify the universally quantified |a|<br>(which generates a rigid type var) with the existentially quatified
<br>|a| (which generates a different rigid type var) -- or so I interpret<br>the error message.<br><br>However, at first sight |f| is polymorphic so it could be applied to<br>any value, included the value hidden in |Box|.
<br><br>Of course, this works:<br><br>mapBox :: (forall a b. a -> b) -> Box -> Box<br>mapBox f (B x) = B (f x)<br><br>Because it's a tautology: given a proof of a -> b for any a or b I can<br>prove Box -> Box. However the only value of type forall a b. a -> b is
<br>bottom.<br><br>This also type-checks:<br><br>mapBox :: (forall a. a -> a) -> Box -> Box<br>mapBox f (B x) = B (f x)<br><br>When trying to give an explanation about why one works and the other<br>doesn't, I see that, logically, we have:
<br><br>forall a. P(a) => Q implies (forall a. P(a)) => Q when a does not<br>occur in Q.<br><br>The proof in our scenario is trivial:<br><br>p :: (forall a. (a -> a) -> (Box -> Box)) -> (forall a. a -> a) -> Box -> Box
<br>p mapBox f b = mapBox f b<br><br>However, the converse is not true.<br><br>Yet, could somebody tell me the logical reason for the type-checking<br>error? In other words, how does the unification failure translate<br>logically. Should the first mapBox actually type-check?
<br><br>Isn't the code for mapBox :: forall a. (a -> a) -> Box -> Box<br>encoding the proof:<br><br>Assume forall a. a -> a<br>Assume exists a.a<br>unpack the existential, x :: a = T for some T<br>apply f to x, we get (f x) :: a
<br>pack into existential, B (f x) :: exists a.a<br>Discharge first assumption<br>Discharge second assumption<br><br>The error must be in step 3. Sorry if this is obvious, it's not to me right now.<br>_______________________________________________
<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe
</a><br></blockquote><br>